summaryrefslogtreecommitdiff
path: root/Test/inline/Elevator.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline/Elevator.bpl')
-rw-r--r--Test/inline/Elevator.bpl312
1 files changed, 156 insertions, 156 deletions
diff --git a/Test/inline/Elevator.bpl b/Test/inline/Elevator.bpl
index 2e146643..dc364ce2 100644
--- a/Test/inline/Elevator.bpl
+++ b/Test/inline/Elevator.bpl
@@ -1,156 +1,156 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %boogie -removeEmptyBlocks:0 "%s" >> "%t"
-// RUN: %diff "%s.expect" "%t"
-// A Boogie version of Elevator.asml (see Boogie/Test/inline/Elevator.asml)
-
-var floors: [int]bool; // set of integer
-var DoorsOpen: [int]bool;
-var liftDoorOpen: bool;
-var liftLevel: int;
-var moving: bool;
-var headingTo: int;
-
-procedure Main_Error()
- modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
-{
- var i: int;
-
- call Initialize();
- while (true)
- invariant !(liftDoorOpen && moving);
- {
- if (*) {
- havoc i; call ButtonPress(i);
- } else if (*) {
- call MoveUp();
- } else if (*) {
- call MoveDown_Error();
- } else if (*) {
- call Stop();
- } else if (*) {
- call OpenLiftDoor();
- } else if (*) {
- call CloseLiftDoor();
- } else if (*) {
- havoc i; call OpenFloorDoor(i);
- } else {
- havoc i; call CloseFloorDoor(i);
- }
- }
-}
-
-procedure Main_Correct()
- modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
-{
- var i: int;
-
- call Initialize();
- while (true)
- invariant !(liftDoorOpen && moving);
- {
- if (*) {
- havoc i; call ButtonPress(i);
- } else if (*) {
- call MoveUp();
- } else if (*) {
- call MoveDown_Correct();
- } else if (*) {
- call Stop();
- } else if (*) {
- call OpenLiftDoor();
- } else if (*) {
- call CloseLiftDoor();
- } else if (*) {
- havoc i; call OpenFloorDoor(i);
- } else {
- havoc i; call CloseFloorDoor(i);
- }
- }
-}
-
-procedure {:inline 1} Initialize()
- modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
-{
- DoorsOpen := EmptySet;
- liftDoorOpen := false;
- liftLevel := 1;
- moving := false;
- headingTo := 0;
-}
-
-procedure {:inline 1} ButtonPress(i: int)
- modifies headingTo;
-{
- assume floors[i];
- headingTo := i;
-}
-
-procedure {:inline 1} MoveUp()
- modifies moving, liftLevel;
-{
- assume !liftDoorOpen && liftLevel < headingTo;
- assume !DoorsOpen[liftLevel];
- moving := true;
- liftLevel:= liftLevel + 1;
-}
-
-procedure {:inline 1} MoveDown_Error()
- modifies moving, liftLevel;
-{
- //bug, should require that liftDoorOpen = false
- // assume !liftDoorOpen;
- assume liftLevel > headingTo && headingTo > 0;
- assume !DoorsOpen[liftLevel];
- moving := true;
- liftLevel := liftLevel - 1;
-}
-
-procedure {:inline 1} MoveDown_Correct()
- modifies moving, liftLevel;
-{
- assume !liftDoorOpen;
- assume liftLevel > headingTo && headingTo > 0;
- assume !DoorsOpen[liftLevel];
- moving := true;
- liftLevel := liftLevel - 1;
-}
-
-procedure {:inline 1} Stop()
- modifies moving;
-{
- assume liftLevel == headingTo;
- moving := false;
-}
-
-procedure {:inline 1} OpenLiftDoor()
- modifies liftDoorOpen;
-{
- assume !moving;
- liftDoorOpen := true;
-}
-
-procedure {:inline 1} CloseLiftDoor()
- modifies liftDoorOpen;
-{
- liftDoorOpen := false;
-}
-
-procedure {:inline 1} OpenFloorDoor(i: int)
- modifies DoorsOpen;
-{
- assume liftLevel == i;
- DoorsOpen[i] := true; // DoorsOpen := DoorsOpen union {i};
-}
-
-procedure {:inline 1} CloseFloorDoor(i: int)
- modifies DoorsOpen;
-{
- DoorsOpen[i] := false; // DoorsOpen := DoorsOpen - {i}
-}
-
-// ---------------------------------------------------------------
-
-const EmptySet: [int]bool;
-axiom (forall o: int :: { EmptySet[o] } !EmptySet[o]);
-
-// ---------------------------------------------------------------
+// RUN: %boogie "%s" > "%t"
+// RUN: %boogie -removeEmptyBlocks:0 "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+// A Boogie version of Elevator.asml (see Boogie/Test/inline/Elevator.asml)
+
+var floors: [int]bool; // set of integer
+var DoorsOpen: [int]bool;
+var liftDoorOpen: bool;
+var liftLevel: int;
+var moving: bool;
+var headingTo: int;
+
+procedure Main_Error()
+ modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+ var i: int;
+
+ call Initialize();
+ while (true)
+ invariant !(liftDoorOpen && moving);
+ {
+ if (*) {
+ havoc i; call ButtonPress(i);
+ } else if (*) {
+ call MoveUp();
+ } else if (*) {
+ call MoveDown_Error();
+ } else if (*) {
+ call Stop();
+ } else if (*) {
+ call OpenLiftDoor();
+ } else if (*) {
+ call CloseLiftDoor();
+ } else if (*) {
+ havoc i; call OpenFloorDoor(i);
+ } else {
+ havoc i; call CloseFloorDoor(i);
+ }
+ }
+}
+
+procedure Main_Correct()
+ modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+ var i: int;
+
+ call Initialize();
+ while (true)
+ invariant !(liftDoorOpen && moving);
+ {
+ if (*) {
+ havoc i; call ButtonPress(i);
+ } else if (*) {
+ call MoveUp();
+ } else if (*) {
+ call MoveDown_Correct();
+ } else if (*) {
+ call Stop();
+ } else if (*) {
+ call OpenLiftDoor();
+ } else if (*) {
+ call CloseLiftDoor();
+ } else if (*) {
+ havoc i; call OpenFloorDoor(i);
+ } else {
+ havoc i; call CloseFloorDoor(i);
+ }
+ }
+}
+
+procedure {:inline 1} Initialize()
+ modifies floors, DoorsOpen, liftDoorOpen, liftLevel, moving, headingTo;
+{
+ DoorsOpen := EmptySet;
+ liftDoorOpen := false;
+ liftLevel := 1;
+ moving := false;
+ headingTo := 0;
+}
+
+procedure {:inline 1} ButtonPress(i: int)
+ modifies headingTo;
+{
+ assume floors[i];
+ headingTo := i;
+}
+
+procedure {:inline 1} MoveUp()
+ modifies moving, liftLevel;
+{
+ assume !liftDoorOpen && liftLevel < headingTo;
+ assume !DoorsOpen[liftLevel];
+ moving := true;
+ liftLevel:= liftLevel + 1;
+}
+
+procedure {:inline 1} MoveDown_Error()
+ modifies moving, liftLevel;
+{
+ //bug, should require that liftDoorOpen = false
+ // assume !liftDoorOpen;
+ assume liftLevel > headingTo && headingTo > 0;
+ assume !DoorsOpen[liftLevel];
+ moving := true;
+ liftLevel := liftLevel - 1;
+}
+
+procedure {:inline 1} MoveDown_Correct()
+ modifies moving, liftLevel;
+{
+ assume !liftDoorOpen;
+ assume liftLevel > headingTo && headingTo > 0;
+ assume !DoorsOpen[liftLevel];
+ moving := true;
+ liftLevel := liftLevel - 1;
+}
+
+procedure {:inline 1} Stop()
+ modifies moving;
+{
+ assume liftLevel == headingTo;
+ moving := false;
+}
+
+procedure {:inline 1} OpenLiftDoor()
+ modifies liftDoorOpen;
+{
+ assume !moving;
+ liftDoorOpen := true;
+}
+
+procedure {:inline 1} CloseLiftDoor()
+ modifies liftDoorOpen;
+{
+ liftDoorOpen := false;
+}
+
+procedure {:inline 1} OpenFloorDoor(i: int)
+ modifies DoorsOpen;
+{
+ assume liftLevel == i;
+ DoorsOpen[i] := true; // DoorsOpen := DoorsOpen union {i};
+}
+
+procedure {:inline 1} CloseFloorDoor(i: int)
+ modifies DoorsOpen;
+{
+ DoorsOpen[i] := false; // DoorsOpen := DoorsOpen - {i}
+}
+
+// ---------------------------------------------------------------
+
+const EmptySet: [int]bool;
+axiom (forall o: int :: { EmptySet[o] } !EmptySet[o]);
+
+// ---------------------------------------------------------------
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 11:23:55 +0000