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