### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / car_1.lus @ 2d37a1e1

1 2 3 b8dc00eb bourbouh ```-- ``` ```-- Source: David Merchat (node voiture + property v6) ``` ```-- ``` ```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); ``` 2d37a1e1 ploc ```--@ contract guarantees OK; ``` b8dc00eb bourbouh ```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 ) and dist < 32767); ``` ``` OK = env => dist >= 0; ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` `tel`