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

[tlaplus] Finite state machine diagrams

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!


Isaac DeFrain

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/CAM3xQxFcajFxFa6zx%3DHJ4KJ%2B37oimt6%2BB8Q0HNZ0SJNpzwG8cw%40mail.gmail.com.