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