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