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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 23 Nov 2020 09:43:22 +0100*References*: <da07b1ce-41d4-4c7b-b0cb-9c2e6eadfff9n@googlegroups.com> <3dee081f-dac9-c381-50b1-c95ac17b49a8@lemmster.de> <999ac752-32a6-4195-b94f-9c03917927b5n@googlegroups.com> <CABf5HMjZ8Y4=zksguvtgXxdVQy+EPwzZKzc0fVuBu0xiWpPb-w@mail.gmail.com> <3603c2f3-ee37-4d76-a7d4-ec8a1d49ce2cn@googlegroups.com> <7ada711f-ac7c-413b-a496-e3ce2e1c7c1dn@googlegroups.com> <CABf5HMiLE7OWQdU47VEyJni71QBtnu9dBcLVo7e078tOHxXGJA@mail.gmail.com>

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

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

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

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

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

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

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

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

- Prev by Date:
**Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?** - Next by Date:
**Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?** - Previous by thread:
**Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?** - Next by thread:
**Re: [tlaplus] Is this a (hidden) variable that tells me the state the model checker is in?** - Index(es):