node Sofar( X : bool ) returns ( Sofar : bool );
let
Sofar = X -> X or pre Sofar;
tel
node Environment(diff: int; plus,minus: bool) returns (ok: bool);
let
ok = (-4 <= diff or 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
node top(diff:int) returns (OK: bool);
--@ contract guarantees OK;
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);
--%MAIN;
--%PROPERTY OK=true;
tel