Re: [tlaplus] non-atomic Peterson in TLA+

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

Hi,

it appears as if you missed to prime req1|2 and inReq1|2 in the two
actions above.

Hope this help,
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/0c0dae3e-842c-e26a-ea69-cb723e9d54c2%40lemmster.de.