%% Verification condition for a water-level controller: % % Finite datatype declaration: type valve_states == on0 | on1 | off0 | off1 % value on0 : valve_states % value on1 : valve_states % value off0 : valve_states % value off1 : valve_states %% All of these "variables", except for tick, can be %% treated as constants: in min_y : real in max_y : real in low_y : real in high_y : real in rate_in : real in rate_out : real in delay : int control s : valve_states value x,y : real variable tick : real ; Forall tick : real . 0 <= tick --> ( min_y <= y /\ y <= max_y /\ (s = off0 \/ s = off1) --> delay < x + tick /\ (s = off1 \/ s = on1) \/ s = off0 /\ y + rate_out * tick < low_y \/ s = on0 /\ high_y < y + rate_out * tick \/ min_y <= y + rate_out * tick /\ y + rate_out * tick <= max_y )