[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Finite state machine diagrams
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Thu, 11 Feb 2021 16:08:50 -0800
- References: <CAM3xQxFcajFxFa6zx=HJ4KJ+37oimt6+B8Q0HNZ0SJNpzwG8cw@mail.gmail.com>
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.