Is it possible to print only the result of one step in simulation mode

[Christian Spann <cspanns....@xxxxxxxxx>]

Dear tla+ users,

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.

Best regards,

Ch0istian