### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / test / src / kind_fmcad08 / simulation / car_6_e3_294_e3_47.lus @ 22fe1c93

 1 ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node excludes2( X1, X2 : bool ) returns ( excludes : bool ); ``` ```let ``` ``` excludes = not ( X1 and X2 ); ``` ```tel ``` ```node voiture(m,s: bool) returns ``` ```( toofast, stop, bump: bool; ``` ``` dist, speed, time: int; ``` ``` move: bool; second, meter: bool ); ``` ```let ``` ``` meter = false -> (m and not s); ``` ``` second = false -> s; ``` ``` move = true -> pre(move and not stop and not toofast and not bump); ``` ``` dist = 0 -> if move and meter then pre(dist)+1 ``` ``` else pre(dist); ``` ``` speed = 0 -> if not move or second then 0 ``` ``` else if move and meter then pre(speed) - 1 ``` ``` else pre(speed); ``` ``` time = 0 -> if second then pre(time) - 1 ``` ``` else pre(time); ``` ``` toofast = speed >= 3; ``` ``` stop = time >= 4; ``` ``` bump = dist = 10; ``` ```tel ``` ```node top(m, s : bool) returns (OK : bool); ``` ```var toofast, stop, bump: bool; ``` ``` dist, speed, time: int; ``` ``` move: bool; second, meter: bool; ``` ``` env : bool; ``` ```let ``` ``` (toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s); ``` ``` env = Sofar( excludes2( m, s ) ); ``` ``` OK = env => true -> not pre bump; ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```