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

*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 aninvariant. (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 withTLC. I'd like to generate a diagram of this model to help myself andothers better understand the behaviors. Are there any tools forachieving this goal? Granted there are 5491776 distinct states so Idon't know how helpful it would really be, but I wanted to ask anyway.

Hi Isaac,

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.

**Follow-Ups**:**Re: [tlaplus] Finite state machine diagrams***From:*Isaac DeFrain

**References**:**[tlaplus] Finite state machine diagrams***From:*Isaac DeFrain

- Prev by Date:
**RE: [tlaplus] CostModel lookup failed** - Next by Date:
**Re: [tlaplus] Finite state machine diagrams** - Previous by thread:
**[tlaplus] Finite state machine diagrams** - Next by thread:
**Re: [tlaplus] Finite state machine diagrams** - Index(es):