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