Made sure that the scenario uses the new substate notation

cwi-swat · Jan 12, 2021 · 82ea726 · 82ea726
1 parent 0d75d75
commit 82ea726
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 15 deletions.
diff --git a/examples/paper/els/Scenario6.rebel b/examples/paper/els/Scenario6.rebel
@@ -60,7 +60,7 @@ spec Scenario6
           // Direction lights
           this.d.left' = 100,
           this.d.right' = 0,
-          this.d' is lFlashBright,
+          this.d' is flashBlinkLeft,
           // Pitman arm
           this.p' is neutral; 
 
@@ -75,7 +75,7 @@ spec Scenario6
           this.d.left = 0,
           this.d.right = 0,
           this.d.cycle = 1,
-          this.d is lFlashDark,
+          this.d is flashBlinkLeft::dark,
           // Pitman arm
           this.p is neutral; 
 
@@ -90,7 +90,7 @@ spec Scenario6
           this.d.left = 0,
           this.d.right = 0,
           this.d.cycle = 1,
-          this.d is lFlashDark,
+          this.d is flashBlinkLeft::dark,
           // Pitman arm
           this.p is neutral; 
 
@@ -105,7 +105,7 @@ spec Scenario6
           this.d.left = 100,
           this.d.right = 0,
           this.d.cycle = 2,
-          this.d is lFlashBright,
+          this.d is flashBlinkLeft::bright,
           // Pitman arm
           this.p is neutral; 
 
@@ -120,7 +120,7 @@ spec Scenario6
           this.d.left = 100,
           this.d.right = 0,
           this.d.cycle = 2,
-          this.d is lFlashBright,
+          this.d is flashBlinkLeft::bright,
           // Pitman arm
           this.p is neutral; 
 
@@ -135,13 +135,13 @@ spec Scenario6
           this.d.left = 0,
           this.d.right = 0,
           this.d.cycle = 3,
-          this.d is lFlashDark,
+          this.d is flashBlinkLeft::dark,
           // Pitman arm
           this.p is neutral; 
 
   event doStep10()
     pre:  // Event
-          // Nothing; forcing the timer to +2 ms should force a new flash blink on the direction lights
+          // Nothing; forcing the timer to +1000 ms should force a new flash blink on the direction lights
           // Sensors
           this.s.key = KeyState[IN_IGNITION_ON],
           // Time 
@@ -150,7 +150,7 @@ spec Scenario6
           this.d.left = 0,
           this.d.right = 0,
           this.d.cycle = 5,
-          this.d is lFlashDark,
+          this.d is flashBlinkLeft::dark,
           // Pitman arm
           this.p is neutral; 
 
@@ -165,7 +165,7 @@ spec Scenario6
           this.d.left' = 0,
           this.d.right' = 0,
           this.d.cycle' = -1, // reset performed
-          this.d' is lFlashDark,
+          this.d' is flashBlinkLeft::dark,
           // Pitman arm
           this.p' is tipBlinkingLeft; 
 
@@ -181,7 +181,7 @@ spec Scenario6
           this.d.left' = 0,
           this.d.right' = 0,
           this.d.cycle' = -1,          
-          this.d' is lFlashDark,
+          this.d' is flashBlinkLeft::dark,
           // Pitman arm
           this.p' is neutral; 
 
@@ -196,7 +196,7 @@ spec Scenario6
           this.d.left = 100,
           this.d.right = 0,
           this.d.cycle = 0,
-          this.d is lFlashBright,
+          this.d is flashBlinkLeft::bright,
           // Pitman arm
           this.p is neutral; 
 
@@ -239,7 +239,7 @@ run UpToStep5 from StartConfig in max 6 steps expect trace;
 
 config AfterStep5 =
   s: KeyOnlySensor mocks SensorValues,
-  d: DirectionLights is lFlashDark with left = 0, right = 0, cycle = 1, sensors = s,
+  d: DirectionLights is flashBlinkLeft::dark with left = 0, right = 0, cycle = 1, sensors = s,
   p: PitmanArm is neutral with dirLights = d, sensors = s,
   scen6: Scenario6 is step5 with s = s, d = d, p = p;
 
@@ -260,7 +260,7 @@ run UpToStep10 from AfterStep5 in max 10 steps expect trace;
 
 config AfterStep10 =  
   s: KeyOnlySensor mocks SensorValues,
-  d: DirectionLights is lFlashDark with left = 0, right = 0, cycle = 5, sensors = s, lastBlinkAt = 7500,
+  d: DirectionLights is flashBlinkLeft::dark with left = 0, right = 0, cycle = 5, sensors = s, lastBlinkAt = 7500,
   p: PitmanArm is neutral with dirLights = d, sensors = s,
   scen6: Scenario6 is step10 with s = s, d = d, p = p;
 

diff --git a/examples/paper/els/Timer.rebel b/examples/paper/els/Timer.rebel
@@ -6,8 +6,8 @@ spec Timer[NOW]
   assume TimeMovesForward = always-last forall t:Timer | t.timepast' > t.timepast;
   assume TimeIsPositive = always forall t:Timer | t.timepast >= 0;
 
-assert TimeCannotGoBackwards = eventually exists t:Timer | t.timepast > 0;
+assert TimeCannotGoBackwards = eventually exists t:Timer | t.timepast' < t.timepast;
 
 config SingletonTimer = t:Timer;
 
-run TimeCannotGoBackwards from SingletonTimer in max 2 steps;  
+run TimeCannotGoBackwards from SingletonTimer in max 5 steps expect no trace;