[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Simulation mode

On 8/5/21 9:23 AM, A. Jesse Jiryu Davis wrote:
Brilliant, thank you! The format is fine for me, my only goal is to read some random traces to check my understanding of my spec.

Is there a way to import one of these files into the Toolbox's trace viewer?

The Toolbox can open the generated file, but SANY won't parse it.

Perhaps, a more useful approach to studying your spec with trace exploration is to simulate your spec checking an "artificial" invariant such as `TLCGet("level") < N`. You get a trace if you choose N less than the diameter shown on the model's result page. Additionally, formulate action- and state-constraints to direct the simulator towards more interesting areas of the state space. This requires a recent TLC nightly build, though.


[1] https://github.com/tlaplus/tlaplus/commit/e7b17ad43db6e277c502840e2b0d1be8effea41b

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/18a70444-91e4-ca26-df1b-79888216d91d%40lemmster.de.