1 files changed, 55 insertions, 55 deletions
diff --git a/Test/inline/Elevator.asml b/Test/inline/Elevator.asml
index 02a58d10..e2d4bdf1 100644
--- a/Test/inline/Elevator.asml
+++ b/Test/inline/Elevator.asml
@@ -1,56 +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)
-  
-  
+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