Re: [tlaplus] Finite state machine diagrams

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.