On 11.02.21 12:52, Isaac DeFrain wrote:
> I vaguely recall that TLC provides graphviz diagrams of "counterexample"
> behaviors, i.e. a minimal sequence of states which invalidates an
> invariant. (It's entirely possible that I'm making this up...
> confirmation would be great, but isn't necessary.)
>
> Either way, I have a finite model which I've checked exhaustively with
> TLC. I'd like to generate a diagram of this model to help myself and
> others better understand the behaviors. Are there any tools for
> achieving this goal? Granted there are 5491776 distinct states so I
> don't know how helpful it would really be, but I wanted to ask anyway.
Hi Isaac,
running TLC with "-dump dot /path/to/a/file.dot" will dump all states in
dot/graphviz notation to /path/to/a/file.dot. For large state spaces,
Gephi or Cytoscape seem to be the most capable viewers. For smaller
ones, xdot gets the job done.
Markus
--
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/15cee859-d66b-e3e4-a780-1e61b55e93d5%40lemmster.de.