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

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



UserA <hana.anber@xxxxxxxxx> 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

-- 
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/87impjxia8.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.

Attachment: signature.asc
Description: PGP signature