Finite state machine diagrams

[Isaac DeFrain]

Hello TLA+ community,

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.

Thanks in advance!

Best,

Isaac DeFrain

[Markus Kuppe]

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

[Isaac DeFrain]

Thanks, 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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/15cee859-d66b-e3e4-a780-1e61b55e93d5%40lemmster.de.