[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] non-atomic Peterson in TLA+
On 22.09.19 16:49, UserA wrote:
> I have that TLA+ Program, and I don't understand why do I get zero
> states when I run the TLC model checker? P.S: The method here is
> non-atomic. Do I need to edit something in the Review Model?
> Thanks in advance,
> Request1a ==
> /\ ~req1
> /\ ~inReq1
> /\ req1 = TRUE
> /\ inReq1 = TRUE
> /\ *UNCHANGED* <<req2, crit1, crit2, inReq2, turn>>
> Request2a ==
> /\ ~req2
> /\ ~inReq2
> /\ req2 = TRUE
> /\ inReq2 = TRUE
> /\ *UNCHANGED* <<req1, crit1, crit2, inReq1, turn>>
it appears as if you missed to prime req1|2 and inReq1|2 in the two
Hope this help,
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/0c0dae3e-842c-e26a-ea69-cb723e9d54c2%40lemmster.de.