### Profile

 1 ```-- ``` ```-- Source Bertrand Jeannet, NBAC tutorial ``` ```-- ``` ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node Environment(diff: int; plus,minus: bool) returns (ok: bool); ``` ```let ``` ``` ok = (-4 <= diff and diff <= 4) and ``` ``` (if (true -> pre plus) then diff >= 1 else true) and ``` ``` (if (false -> pre minus) then diff <= -1 else true); ``` ```tel ``` ```node Controller(diff: int) returns (speed: int; plus,minus: bool); ``` ```let ``` ``` speed = 0 -> pre(speed)+diff; ``` ``` plus = speed <= 9; ``` ``` minus = speed >= 11; ``` ```tel ``` ```node Property(speed: int) returns (ok: bool); ``` ```var cpt: int; ``` ``` acceptable: bool; ``` ```let ``` ``` acceptable = 8 <= speed and speed <= 12; ``` ``` cpt = 0 -> if acceptable then 0 else pre(cpt)+1; ``` ``` ok = true -> (pre cpt<=7); ``` ```tel ``` ```--@ ensures OK; ``` ```node top(diff:int) returns (OK: bool); ``` ```var speed: int; ``` ``` plus,minus,realistic: bool; ``` ```let ``` ``` (speed,plus,minus) = Controller(diff); ``` ``` realistic = Environment(diff,plus,minus); ``` ``` OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed); ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```