Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.57 KB)

 1 node Sofar( X : bool ) returns ( Sofar : bool ); let Sofar = X -> X or pre Sofar; tel node controleur(nB,nS:int) returns (diff:int; avance,retard:bool); let diff = nB-nS; avance = false -> if not (pre avance) then diff >= 10 else diff > 0; retard = false -> if not (pre retard) then (diff <= -10) else (diff < 0); tel node hypothese(B,S,avance,retard:bool) returns (ok:bool); var c:int; let ok = true -> (if pre retard then not S else true) and (if pre c >= 9 then not B else true); c = 0 -> if pre avance and avance then if B then pre c +1+ 1 else pre c else 0; tel node main(B0, B1 : bool; S : bool) returns ( ast: bool; nB0, nB1 : int; nS : int; diff0, diff1:int; avance0, avance1, retard0, retard1 : bool ); var H0, H1:bool; let nB0 = 0 -> if B0 then pre nB0 + 1 else pre nB0; nB1 = 0 -> if B1 then pre nB1 + 1 else pre nB1; nS = 0 -> if S then pre nS + 1 else pre nS; H0 = hypothese(B0,S,avance0,retard0); H1 = hypothese(B1,S,avance1,retard1); (diff0,avance0,retard0) = controleur(nB0,nS); (diff1,avance1,retard1) = controleur(nB1,nS); ast = H0 and H1; tel node top(B0, B1 : bool; S : bool) returns (OK:bool); var nB0, nB1 : int; nS : int; diff0, diff1 :int; avance0, avance1, retard0, retard1 : bool; pOK:bool; ast:bool; let (ast,nB0,nB1,nS,diff0,diff1,avance0,avance1,retard0,retard1) = main(B0,B1,S); pOK = true -> not (pre avance0 and retard0 or pre retard0 and avance0); OK = Sofar( ast and nB0 < 1 and nB1 < 1 and nS < 1 and diff0 < 32767 ) => (true -> pre pOK); --%MAIN; --%PROPERTY OK=true; tel