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

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

On 04.09.2017 18:33, Christian Spann wrote:
> I am wondering if it is possible to have TLC execute an arbitrary path
> in a model checking process (simulation mode) of some predefined depth
> and print only the output of the chosen steps instead of printing the
> output of all inspected options before randomly choosing one. Or is
> there another way to achieve such behaviour by using the depth-first
> inspection? I experienced the latter (depth first) to print less and
> less with ongoing exploration, I guess there is some optimization in
> place to skip already computed states which makes it faster but again
> hinders readability if one wants to see how the algorithm evolves
> along its path. Leslie Lamport correctly stated somewhere that TLC is
> obviously not designed for "programming language like" behaviours but
> optimized for model checking but at least we have a strong need for
> this to be able to quickly identify if our spec is defined roughly as
> what we want it to be. 


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


[1]
https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/Generator.java

[2]
https://github.com/tlaplus/tlaplus/commit/1f794340bc194dc54624392ea191c1010c307ba0