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
|
-- U turn system for a subway
-- See paper HLR-lustre.tse.ps
node edge(X: bool) returns (EDGE: bool)
let
EDGE = X -> (X and not pre X);
tel
node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)
returns (grant_access, grant_exit, do_AB, do_BC: bool)
var empty_section, only_on_B: bool;
let
grant_access = empty_section and ack_AB;
grant_exit = only_on_B and ack_BC;
do_AB = (not ack_AB) and empty_section;
do_BC = (not ack_BC) and only_on_B;
empty_section = not (on_A or on_B or on_C);
only_on_B = on_B and not (on_C or on_A);
tel
node always_from_to(B, A, C: bool) returns (X: bool)
let
X = implies(after(A), always_since(B, A) or once_since(C, A));
tel
node implies(A, B: bool) returns (AimpliesB: bool)
let
AimpliesB = (not A) or B;
tel
node after(A: bool) returns (afterA: bool)
let
afterA = false -> pre(A or afterA);
tel
node always_since(B, A: bool) returns (alwaysBsinceA: bool)
let
alwaysBsinceA = if A then B
else if after(A) then B and pre alwaysBsinceA
else true;
tel
node once_since(C, A: bool) returns (onceCsinceA: bool)
let
onceCsinceA = if A then C
else if after(A) then C or pre onceCsinceA
else true;
tel
node UMS_verif(on_A, on_B, on_C, ack_AB, ack_BC: bool)
returns()
var
grant_access, grant_exit: bool;
do_AB, do_BC: bool;
empty_section, only_on_B: bool;
let
empty_section = not (on_A or on_B or on_C);
only_on_B = on_B and not(on_A or on_C);
assume h1: not(ack_AB and ack_BC);
assume h2: always_from_to(ack_AB, ack_AB, do_BC)
and always_from_to(ack_BC, ack_BC, do_AB);
assume h3: empty_section -> true;
assume h4: true -> implies(edge(not empty_section), pre grant_access);
assume h5: true -> implies(edge(on_C), pre grant_exit);
assume h6: true -> implies(edge(not on_A), on_B);
assume h7: true -> implies(edge(not on_B), on_A or on_C);
grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC);
guarantee no_collision: implies(grant_access, empty_section);
guarantee exclusive_req: not(do_AB and do_BC);
guarantee no_derail_AB: always_from_to(ack_AB, grant_access, only_on_B);
guarantee no_derail_BC: always_from_to(ack_BC, grant_exit, empty_section);
tel
|
