From 82ea7261bff9c239607bec829541eb11a5a2f9d1 Mon Sep 17 00:00:00 2001 From: Jouke Stoel Date: Tue, 12 Jan 2021 10:03:12 +0100 Subject: [PATCH] Made sure that the scenario uses the new substate notation --- examples/paper/els/Scenario6.rebel | 26 +++++++++++++------------- examples/paper/els/Timer.rebel | 4 ++-- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/examples/paper/els/Scenario6.rebel b/examples/paper/els/Scenario6.rebel index 8ac5be3..401195f 100644 --- 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 index 552c943..0c8ffac 100644 --- 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; \ No newline at end of file +run TimeCannotGoBackwards from SingletonTimer in max 5 steps expect no trace; \ No newline at end of file