[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Is it possible to print only the result of one step in simulation mode
On 13.09.2017 18:44, Christian Spann wrote:
> Hi Markus,
> thanks for the hint, works like a charm.
> Best regards,
>> Hi Christian,
>> you can try the Generator  which writes N randomly chosen traces of
>> length D into N output files. You run it with "java -cp tla2tools.jar
>> tlc2.Generator -n N -d D MC" where MC is the name of your spec.
>> Notice that the released version of the Generator does not correctly
>> terminate. You will have to manually kill it after it has created D
>> output files. The next release will contain a bug fix .
>> Hope this helps,
for small state spaces you might also be interested in the new state
graph visualization which is included in recent nightly builds . Just
tick the corresponding check-box in the "TLC Options" section of the
"Advanced Options" model editor page and run TLC.