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

Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?

> How/can we ask TLA to tell us legal next states from a specified label?

I don't know a straightforward way to list them, but you can easily ask the model checker whether a particular label-to-label transition is possible. For instance, to detect if a process can transition from label "la" to label "lb", you could check the temporal property:

[][~\E pid \in ProcSet: pc[pid] = "la" /\ pc'[pid] = "lb"]_vars

A "violation" of this property would be a trace where some process takes a step from label "la" to label "lb". I often do things like this to check whether certain events are possible in my specifications.

Similarly, you can check a property such as

\A pid \in ProcSet : [][ pc[pid] = "la" => pc'[pid] \in {"la", "lb", "lc"} ]_vars

to verify that your understanding of possible transitions is correct.


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/4CF3CDD9-D8A4-433A-A89C-EE12D9548998%40gmail.com.