Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / metros_1.lus @ 22fe1c93

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