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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

> 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.

Stephan

--
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.