diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/inline/Elevator.asml | |
Initial set of files.
Diffstat (limited to 'Test/inline/Elevator.asml')
| -rw-r--r-- | Test/inline/Elevator.asml | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/Test/inline/Elevator.asml b/Test/inline/Elevator.asml new file mode 100644 index 00000000..02a58d10 --- /dev/null +++ b/Test/inline/Elevator.asml @@ -0,0 +1,56 @@ +var floors as Set of Integer
+var DoorsOpen as Set of Integer = {}
+var liftDoorOpen as Boolean = false
+var liftLevel as Integer = 1
+var moving as Boolean = false
+var headingTo as Integer = 0
+
+[Action]
+ButtonPress(i as Integer)
+ require i in floors
+ headingTo := i
+
+[Action]
+MoveUp()
+ require liftDoorOpen = false and liftLevel < headingTo
+ require not (liftLevel in DoorsOpen)
+ moving := true
+ liftLevel:= liftLevel + 1
+
+[Action]
+MoveDown()
+ //bug, should require that liftDoorOpen = false
+ require liftLevel > headingTo and headingTo > 0
+ require not (liftLevel in DoorsOpen)
+ moving := true
+ liftLevel := liftLevel - 1
+
+[Action]
+Stop()
+ require liftLevel = headingTo
+ moving := false
+
+[Action]
+OpenLiftDoor()
+ require moving = false
+ liftDoorOpen := true
+
+[Action]
+CloseLiftDoor()
+ liftDoorOpen := false
+
+[Action]
+OpenFloorDoor(i as Integer)
+ require liftLevel = i
+ DoorsOpen := DoorsOpen union {i}
+
+[Action]
+CloseFloorDoor(i as Integer)
+ DoorsOpen := DoorsOpen - {i}
+
+
+Invariant ()
+ require not (liftDoorOpen = true and moving = true)
+
+
+
\ No newline at end of file |