[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Finite state machine diagrams

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.


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.