summaryrefslogtreecommitdiff
path: root/Test/inline/Elevator.asml
blob: e2d4bdf13cbfe2c21bcfba473c59436d9574b0e5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
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)