lustrec / test / src / kind_fmcad08 / simulation / metros_4_e5_1150.lus @ 0cbf0839
History | View | Annotate | Download (1.44 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
node controleur(nB,nS:int) returns (diff:int; avance,retard:bool); |
7 |
let |
8 |
diff = nB-nS; |
9 |
avance = false -> |
10 |
if not (pre avance) then diff >= 10 else diff > 0; |
11 |
retard = false -> |
12 |
if not (pre retard) then (diff <= -10) else (diff < 0); |
13 |
tel |
14 |
node hypothese(B,S,avance,retard:bool) returns (ok:bool); |
15 |
var c:int; |
16 |
let |
17 |
ok = true -> |
18 |
(if pre retard then not S else true) and |
19 |
(if pre c >= 9 then not B else true); |
20 |
c = 0 -> |
21 |
if pre avance and avance then |
22 |
if B then pre c + 1 else pre c |
23 |
else |
24 |
0; |
25 |
tel |
26 |
node main(B0, B1 : bool; S : bool) |
27 |
returns ( ast: bool; nB0, nB1 : int; nS : int; |
28 |
diff0, diff1:int; |
29 |
avance0, avance1, retard0, retard1 : bool ); |
30 |
var H0, H1:bool; |
31 |
let |
32 |
nB0 = 0 -> if B0 then pre nB0 + 1 else pre nB0; |
33 |
nB1 = 0 -> if B1 then pre nB1 + 1 else pre nB1; |
34 |
nS = 0 -> if S then pre nS + 1 else pre nS; |
35 |
H0 = hypothese(B0,S,avance0,retard0); |
36 |
H1 = hypothese(B1,S,avance1,retard1); |
37 |
(diff0,avance0,retard0) = controleur(nB0,nS); |
38 |
(diff1,avance1,retard1) = controleur(nB1,nS); |
39 |
ast = H0 and H1; |
40 |
tel |
41 |
node top(B0,B1 : bool; S : bool) |
42 |
returns (OK:bool); |
43 |
var nB0,nB1 : int; |
44 |
nS : int; |
45 |
diff0,diff1:int; |
46 |
avance0,avance1,retard0,retard1 : bool; |
47 |
ast:bool; |
48 |
let |
49 |
(ast,nB0,nB1,nS,diff0,diff1,avance0,avance1,retard0,retard1) = main(B0,B1,S); |
50 |
OK = Sofar( ast ) => true -> (pre(nB0) -1- pre (nB1)) <= 30; |
51 |
--%MAIN; |
52 |
--%PROPERTY OK=true; |
53 |
tel |