Add a third variable to be able to better discuss stuttering.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

examples/SimpleEventually.tla

@@ -3,29 +3,38 @@
 EXTENDS TLAPS
 
 
-VARIABLE x, y
-vars == <<x, y>>
+VARIABLE x, y, flip
+vars == <<x, y, flip>>
 
 TypeOK ==
     /\ x \in BOOLEAN
     /\ y \in BOOLEAN
+    /\ flip \in BOOLEAN
 
 Init ==
     /\ x = FALSE
     /\ y = FALSE
+    /\ flip = FALSE
 
 A ==
     /\ x = FALSE
     /\ x' = TRUE
-    /\ UNCHANGED y
+    /\ UNCHANGED <<y, flip>>
 
 B ==
-\*    /\ y = FALSE \* WF_vars(Next) suffices hinges on the fact that a B step disables B (s.t. it leaves the vars unchanged). 
+    /\ y = FALSE \* WF_vars(Next) hinges on the fact that a B step disables B, i.e., additional B steps will leave vars unchanged. 
     /\ y' = TRUE
+    /\ flip' = ~flip
+    /\ UNCHANGED x
+
+C ==
+    /\ y = FALSE \* WF_vars(Next) hinges on the fact that a C step disables C. 
+    /\ y' = TRUE
+    /\ flip' = ~flip
     /\ UNCHANGED x
 
 Next ==
-    A \/ B
+    A \/ B \/ C
 
 System ==
     Init /\ [][Next]_vars /\ WF_vars(Next)
@@ -37,8 +46,8 @@ Prop ==
 (* Ordinary safety proof. *)
 LEMMA TypeCorrect == System => []TypeOK
 <1>1. Init => TypeOK BY DEF Init, TypeOK
-<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B
-<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B
+<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B, C
+<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B, C
 
 -------------------------------------------------------------------------------
 
@@ -51,13 +60,13 @@ LEMMA TypeCorrect == System => []TypeOK
 *)
 THEOREM System => Prop
 <1>1. TypeOK /\ ~(x = TRUE) => ENABLED <<Next>>_vars
-  BY ExpandENABLED DEF Next, A, B, vars
+  BY ExpandENABLED DEF Next, A, B, C, vars
 <1>2. TypeOK /\ ~(x = TRUE) /\ (y = TRUE) /\ <<Next>>_vars => (x = TRUE)'
-  BY DEF TypeOK, Next, A, B, vars
+  BY DEF TypeOK, Next, A, B, C, vars
 <1>3. TypeOK /\ ~(x = TRUE) /\ ~(y = TRUE) /\ ~(x = TRUE)' /\ <<Next>>_vars => (y = TRUE)'
-  BY DEF TypeOK, Next, A, B, vars
+  BY DEF TypeOK, Next, A, B, C, vars
 <1>4. TypeOK /\ (y = TRUE) /\ [Next]_vars => (y = TRUE)' \* Could replace [Next]_vars with UNCHANGED vars.
-  BY DEF TypeOK, Next, A, B, vars
+  BY DEF TypeOK, Next, A, B, C, vars
 <1> QED
   BY TypeCorrect, <1>1, <1>2, <1>3, <1>4, PTL DEF System, Prop