%% Modified thermostat example with delay (see VMCAI paper)
%% Dynamics: 
%% Mode ON : vdot=1, xdot=v;   // previously xdot = v-10
%% Mode OFF: vdot=-1, xdot=v
%% Goal: synthesize switching logic s.t. x in [70,80]
%% Init v=0, x\in [74,76]
%% Template:
%%  -(v)^2 - a*(x-75)^2 + b
%% We immediately get the desired answer; 
%% constraint on a,b : which we can solve by looking at it;
%% a=1/25,b=1 is a solution. We use slfq on the constraint
%% and see that it simplifies in  50 milliseconds to:
%% [ a > 0 /\ b - 25 a <= 0 /\ b >= 0 /\ a b - 1 <= 0 ]

load redlog;
rlset r;

load_package qepcad;
on rlqefbqepcad;      % use QEPCAD as the fallback QE
rlqepcadn(100*10^6);  % The number of cells used by QEPCAD. The
rlqepcadl(200*10^3);  % The size of the prime list used by QEPCAD. The
on rlverbose;
on time;
off rlqefb;		% No fallback QE

phi1 :=
  (( 74 <= x AND x <= 76 AND  v = 0   ) impl 
    ( -v^2 - a * (x-75)^2 + b >= 0 ) );

phi2 :=
  ( ( -v^2 - a * (x-75)^2 + b >= 0 ) impl
    ( 80 >= x    AND  x >= 70   ) );

phi3 :=
  ( ( -v^2 - a * (x-75)^2 + b = 0 ) impl
    ( -2*v - a * 2 * (x-75)* v >= 0 OR
       2*v - a * 2 * (x-75)* v >= 0 ) );

phi := phi1 and phi2 and phi3;

psi := rlqe( all({ x,  v}, phi ))$

% psi1 := second psi$

psi2 := rlqepcad( rlex(psi), "thermo-two-quad.qepcad" );

off nat;	% Output same syntax as input (for reduce)

out "thermo-two.out";
psi;
psi2;
shut "thermo-two.out";
 
end;