blob: 2dc6f03d72d042409906f68ebc925e4ba4932775 (
plain) (
blame)
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
|
MODULE main
VAR
open : array 0..3 of boolean;
at : array 0..3 of boolean;
req : array 0..3 of boolean;
ind : array 0..3 of boolean;
moving : boolean;
_at : 0..3;
_next_at : 0..3;
--_open : -1..3;
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[_at] : _at; -- stay on requested floor
req[2] : _at=0 ? 1 : 2; -- go to requested floor
req[1] : _at=3 ? 2 : 1;
req[0] : _at=0 ? 0 : _at - 1;
TRUE : 0;
esac;
ASSIGN
init(_at) := 0;
--init(_open) := -1;
init(open[0]) := FALSE;
init(open[1]) := FALSE;
init(open[2]) := FALSE;
init(open[3]) := FALSE;
next(_at) := _next_at;
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] & !req[3];
next(open[1]) := req[1] & at[1] & !req[3];
next(open[2]) := req[2] & at[2] & !req[3];
next(open[3]) := req[3] & at[3];
next(ind[0]) := req[0];
next(ind[1]) := req[1];
next(ind[2]) := req[2];
next(ind[3]) := req[3];
-- physical constraint: 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];
--INVAR _open = 0 <-> open[0]; INVAR _open = 1 <-> open[1];
--INVAR _open = 2 <-> open[2]; INVAR _open = 3 <-> open[3];
-- Help variables
INVAR moving = !(_at = _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
--LTLSPEC G (req[0] -> F open[0]);
--LTLSPEC G (req[1] -> F open[1]);
--LTLSPEC G (req[2] -> F open[2]);
LTLSPEC G (req[3] -> F open[3]);
-- Same, in CTL
--CTLSPEC AG (req[0] -> AF open[0]);
--CTLSPEC AG (req[1] -> AF open[1]);
--CTLSPEC AG (req[2] -> AF open[2]);
CTLSPEC AG (req[3] -> AF open[3]);
-- Property 4: elevator will invariantly return to floor 0
CTLSPEC AF at[0];
-- 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[0] -> F open[0];
--LTLSPEC G ind[1] -> F open[1];
--LTLSPEC G ind[2] -> F open[2];
LTLSPEC G ind[3] -> F open[3];
-- Property 7: no move when no request
LTLSPEC G !(req[0] | req[1] | req[2] | req[3]) -> !moving
-- Test properties
CTLSPEC AG EF moving; -- always eventually exists a state where elevator is moving
LTLSPEC !F G moving; -- elevator isn't moving all the time
CTLSPEC AG EF open[0]; -- it is always possible that any door will open at some point
CTLSPEC AG EF open[1];
CTLSPEC AG EF open[2];
CTLSPEC AG EF open[3];
|
