Re: [tlaplus] Is it possible to print only the result of one step in simulation mode

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 13.09.2017 18:44, Christian Spann wrote:
> Hi Markus,
> 
> thanks for the hint, works like a charm.
> 
> Best regards,
> 
> Christian
> 
>> Hi Christian,
>>
>> you can try the Generator [1] 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 [2].
>>
>> Hope this helps,
>>
>> Markus
Hi Christian,

for small state spaces you might also be interested in the new state
graph visualization which is included in recent nightly builds [1]. Just
tick the corresponding check-box in the "TLC Options" section of the
"Advanced Options" model editor page and run TLC.

Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/