Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

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+ 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) - pre (nB1)) <= 30;
51
  --%MAIN;
52
  --%PROPERTY  OK=true;
53
tel