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)
|
