Re: [tlaplus] Simulation mode

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.