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

[tlaplus] non-atomic Peterson in TLA+



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

            

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/91e222b5-2b6e-4b0e-8d57-edffd1869a2c%40googlegroups.com.