[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.

Markus

[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.