state
Init0 : bool;
Pminus, Pplus : bool;
Pspeed, PV98_cpt : int ;
input
diff : int ;
local
realistic, minus, plus, V99_acceptable, ok : bool;
speed, V98_cpt : int ;
definition
realistic = (((((-4) <= diff) and (diff <= 4)) and (if (if Init0 then true
else Pplus) then (diff >= 1) else true)) and (if (if Init0 then false else
Pminus) then (diff <= (-1)) else true));
minus = ((if Init0 then 0 else (Pspeed + diff)) >= 11);
plus = ((if Init0 then 0 else (Pspeed + diff)) <= 9);
V99_acceptable = ((8 <= (if Init0 then 0 else (Pspeed + diff))) and ((if
Init0 then 0 else (Pspeed + diff)) <= 12));
ok = (if Init0 then true else (PV98_cpt <= 7));
speed = (if Init0 then 0 else (Pspeed + diff));
V98_cpt = (if Init0 then 0 else (if V99_acceptable then 0 else (PV98_cpt + 1
)));
transition
Init0' = not true;
Pminus' = ((if Init0 then 0 else (Pspeed + diff)) >= 11);
Pplus' = ((if Init0 then 0 else (Pspeed + diff)) <= 9);
Pspeed' = (if Init0 then 0 else (Pspeed + diff));
PV98_cpt' = V98_cpt;
initial
Init0;
assertion
(((((-4) <= diff) and (diff <= 4)) and (if (if Init0 then true else Pplus)
then (diff >= 1) else true)) and (if (if Init0 then false else Pminus) then (
diff <= (-1)) else true));
invariant ok;