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.