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,