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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
MODULE main
VAR
-- APs
open : array 0..3 of boolean;
at : array 0..3 of boolean;
req : array 0..3 of boolean;
ind : array 0..3 of boolean;
-- Helper
moving : boolean;
-- Program logic
_at : 0..3;
_next_at : 0..3;
_prio : array 0..2 of 0..2;
ASSIGN
init(_at) := 0;
init(open[0]) := FALSE;
init(open[1]) := FALSE;
init(open[2]) := FALSE;
init(open[3]) := FALSE;
init(_prio[0]) := 0;
init(_prio[1]) := 1;
init(_prio[2]) := 2;
INVAR
-- Setting next(at) in a variable itself enables us to use it in the moving
-- variable below.
_next_at = case
req[3] : _at=3 ? 3 : _at + 1; -- top floor priority
req[_prio[0]] : case -- go to requested floor & stay
_at > _prio[0] : _at - 1;
_at < _prio[0] : _at + 1;
_at = _prio[0] : _at;
esac;
req[_prio[1]] : case
_at > _prio[1] : _at - 1;
_at < _prio[1] : _at + 1;
_at = _prio[1] : _at;
esac;
req[_prio[2]] : case
_at > _prio[2] : _at - 1;
_at < _prio[2] : _at + 1;
_at = _prio[2] : _at;
esac;
TRUE : _at; -- no request; stay
esac;
-- Help variables
-- Can't use next(_at) here, because this is a simple_expression
INVAR moving = !(_at = _next_at)
ASSIGN
next(_at) := _next_at;
-- A request holds until the elevator opens on that floor
-- Any floor can be requested at any moment
next(req[0]) := req[0] & !open[0] ? TRUE : {TRUE, FALSE};
next(req[1]) := req[1] & !open[1] ? TRUE : {TRUE, FALSE};
next(req[2]) := req[2] & !open[2] ? TRUE : {TRUE, FALSE};
next(req[3]) := req[3] & !open[3] ? TRUE : {TRUE, FALSE};
next(open[0]) := req[0] & at[0] & !moving & !req[3] & _prio[0] = 0;
next(open[1]) := req[1] & at[1] & !moving & !req[3] & _prio[0] = 1;
next(open[2]) := req[2] & at[2] & !moving & !req[3] & _prio[0] = 2;
next(open[3]) := req[3] & at[3] & !moving;
next(ind[0]) := req[0];
next(ind[1]) := req[1];
next(ind[2]) := req[2];
next(ind[3]) := req[3];
-- Priorities
next(_prio[0]) := case
!(open[0] | open[1] | open[2] | open[3]) : case
req[_prio[0]] : _prio[0];
req[_prio[1]] : _prio[1];
req[_prio[2]] : _prio[2];
TRUE : _prio[0];
esac;
open[_prio[0]] : _prio[1];
TRUE : _prio[0];
esac;
next(_prio[1]) := case
open[_prio[0]] | open[_prio[1]] : _prio[2];
req[_prio[0]] & req[_prio[1]] : _prio[1];
req[_prio[0]] & req[_prio[2]] : _prio[2];
req[_prio[1]] & req[_prio[2]] : _prio[2];
req[_prio[1]] : _prio[2];
TRUE : _prio[1];
esac;
-- Every floor has only one priority
INVAR !(_prio[0] = _prio[1] | _prio[0] = _prio[2] | _prio[1] = _prio[2])
-- The last priority is the remaining floor
INVAR !(_prio[0] = 0 | _prio[1] = 0) -> _prio[2] = 0;
INVAR !(_prio[0] = 1 | _prio[1] = 1) -> _prio[2] = 1;
INVAR !(_prio[0] = 2 | _prio[1] = 2) -> _prio[2] = 2;
-- Physical constraint: elevator is at only one place at a time
INVAR at[0] -> !(at[1]|at[2]|at[3]); INVAR at[1] -> !(at[0]|at[2]|at[3]);
INVAR at[2] -> !(at[0]|at[1]|at[3]); INVAR at[3] -> !(at[0]|at[1]|at[2]);
-- Link between program logic and APs
INVAR _at = 0 <-> at[0]; INVAR _at = 1 <-> at[1];
INVAR _at = 2 <-> at[2]; INVAR _at = 3 <-> at[3];
-- Test properties
-- There is always some possibility for the elevator to move
CTLSPEC AG EF moving;
-- The elevator isn't moving all the time
LTLSPEC !F G moving;
-- It is always possible that the doors at any floor will eventually open
CTLSPEC AG EF open[0];
CTLSPEC AG EF open[1];
CTLSPEC AG EF open[2];
CTLSPEC AG EF open[3];
-- It is always possible that the elevator will be at any floor at some point
CTLSPEC AG EF at[0];
CTLSPEC AG EF at[1];
CTLSPEC AG EF at[2];
CTLSPEC AG EF at[3];
-- One step at a time
LTLSPEC G (_at = _next_at | _at + 1 = _next_at | _at - 1 = _next_at)
-- Property 1: door is never open if the elevator is not at that floor
LTLSPEC G (open[0] -> at[0]);
LTLSPEC G (open[1] -> at[1]);
LTLSPEC G (open[2] -> at[2]);
LTLSPEC G (open[3] -> at[3]);
-- Property 2: requested floor will be served sometime, unless 3 will be served
-- invariantly
LTLSPEC G (req[0] -> F open[0] | G F open[3]);
LTLSPEC G (req[1] -> F open[1] | G F open[3]);
LTLSPEC G (req[2] -> F open[2] | G F open[3]);
LTLSPEC G (req[3] -> F open[3]);
-- Same, in CTL
CTLSPEC AG (req[0] -> AF open[0] | EF open[3]);
CTLSPEC AG (req[1] -> AF open[1] | EF open[3]);
CTLSPEC AG (req[2] -> AF open[2] | EF open[3]);
CTLSPEC AG (req[3] -> AF open[3]);
-- Property 3: it is always possible to go to any floor, unless floor 3 will be
-- served invariantly
CTLSPEC AG (req[0] -> AF open[0] | EF AF open[3]);
CTLSPEC AG (req[1] -> AF open[1] | EF AF open[3]);
CTLSPEC AG (req[2] -> AF open[2] | EF AF open[3]);
CTLSPEC AG (req[3] -> AF open[3]);
-- Property 5: top floor priority
LTLSPEC G (req[3] -> (!X(open[0] | open[1] | open[2]) U open[3]));
-- Property 6: lights are correct
LTLSPEC G ind[3] -> F open[3];
-- Since the top floor has priority, it is also possible that this floor will
-- be served invariantly and the other floors suffer starvation. The next oper-
-- ator is here, because the indicator lights are updated only the next step.
LTLSPEC G (X ind[0] -> F open[0] | G F open[3]);
LTLSPEC G (X ind[1] -> F open[1]) | G F open[3];
LTLSPEC G (X ind[2] -> F open[2]) | G F open[3];
-- Property 7: no move when no request
LTLSPEC G count(req[0], req[1], req[2], req[3]) = 0 -> !moving;
-- Properties that do not hold
-- Property 2: requested floor, if not 3, will be served sometime (floor 3 may
-- be served invariantly)
--LTLSPEC G (req[0] -> F open[0]);
--LTLSPEC G (req[1] -> F open[1]);
--LTLSPEC G (req[2] -> F open[2]);
-- Property 3: it is always possible to go to any floor (does not hold for any
-- floor except 3)
--CTLSPEC AF (req[0] -> open[0]);
--CTLSPEC AF (req[1] -> open[1]);
--CTLSPEC AF (req[2] -> open[2]);
-- Property 4: elevator will invariantly return to floor 0 (if floor 0 is never
-- requested but other floors are, elevator will never go to floor 0)
--LTLSPEC G F at[0];
|
