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

[Markus Kuppe]

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

[Marko Schuetz-Schmuck]

UserA <hana....@gmail.com> writes:

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

> *VARIABLES* req1, req2, crit1, crit2, turn, inReq1, inReq2
>
>
>
>
> TypeInv ==
>
> /\ req1 \in BOOLEAN
>
> /\ req2 \in BOOLEAN
>
> /\ crit1 \in BOOLEAN
>
> /\ crit2 \in BOOLEAN
>
> /\ turn \in {1,2}
>
> /\ inReq1 \in BOOLEAN
>
> /\ inReq2 \in BOOLEAN
>
>
>
> v == <<req1, req2, crit1, crit2, turn, inReq1, inReq2>>
>
>
> Init ==
>
> /\ req1 = FALSE
>
> /\ crit1 = FALSE
>
> /\ req2 = FALSE
>
> /\ crit2 = FALSE
>
> /\ inReq1 = FALSE
>
> /\ inReq2 = FALSE
>
> /\ TypeInv

>
>
>
> Request1a ==
>
> /\ ~req1
>
> /\ ~inReq1
>
> /\ req1 = TRUE
>
> /\ inReq1 = TRUE
>
> /\ *UNCHANGED* <<req2, crit1, crit2, inReq2, turn>>

I guess you want to express an action here:

Request1a ==
/\ ~req1
/\ ~inReq1
/\ req1' = TRUE
/\ inReq1' = TRUE

/\ UNCHANGED <<req2, crit1, crit2, inReq2, turn>>

What you had written would require both req1 and inReq1 to be FALSE and
simultaneously to be TRUE.

Best regards,

Marko

> Request2a ==
>
> /\ ~req2
>
> /\ ~inReq2
>
> /\ req2 = TRUE
>
> /\ inReq2 = TRUE
>
> /\ *UNCHANGED* <<req1, crit1, crit2, inReq1, turn>>
>
>
>

> Request1b ==
>
> /\ inReq1
>
> /\ inReq1' = FALSE
>
> /\ turn' = 2
>
> /\ *UNCHANGED* <<req1, req2, crit1, crit2, inReq2>>
>
>
>
> Request2b ==
>
> /\ inReq2
>
> /\ inReq2' = FALSE
>
> /\ turn' = 1
>
> /\ *UNCHANGED* <<req1, req2, crit1, crit2, inReq1>>
>
>
>
> Enter1 ==
>
> /\ ~inReq1 \* here we check if it is not in the req1,
>
> /\ req1 \* then we get into req1
>
> /\ ~req2 \/ turn = 1 \* then we check if it is not in the req2,
> and not turn 1
>
> /\ crit1' = TRUE \* then we get into the other flag which
> is crit1 and assign it to TRUE
>
> /\ *UNCHANGED* <<req1, req2, crit2, turn, inReq1, inReq2>>
>
>
>
> Enter2 ==
>
> /\ ~inReq2
>
> /\ req2
>
> /\ ~req1 \/ turn = 2
>
> /\ crit2' = TRUE
>
> /\ *UNCHANGED* <<req1, req2, crit1, turn, inReq1, inReq2>>
>
>
>
> Exit1 ==
>
> /\ crit1
>
> /\ crit1' = FALSE
>
> /\ req1' = FALSE
>
> /\ *UNCHANGED* <<req2, crit2, inReq1, inReq2, turn>>
>
>
>
> Exit2 ==
>
> /\ crit2
>
> /\ crit2' = FALSE
>
> /\ req2' = FALSE
>
> /\ *UNCHANGED* <<req1, crit1, inReq1, inReq2, turn>>
>
>
>
>
>
> Prog1 ==
>
> \/ Request1a
>
> \/ Request1b
>
> \/ Enter1
>
> \/ Exit1
>
>
>
> Prog2 ==
>
> \/ Request2a
>
> \/ Request2b
>
> \/ Enter2
>
> \/ Exit2
>
>
>
> Next == Prog1 \/ Prog2
>
>
>
> Prog == Init /\ [][Next]_v /\ WF_v(Prog1) /\ WF_v(Prog2)
>
>
>
> ====================================================
>
> Safety == [] ~(crit1 /\ crit2)
>
>
> Liveness == /\ (req1 ~> crit1)
>
> /\ (req2 ~> crit2)
>
>
> Spec == Safety /\ Liveness