%% 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: 
%%  x + a v v + b v + c 
%% -x + a v v + b v + d 
%% QEPCAD fails on this; so don't know the answer.

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

%%  x + a v v + b v + c 
%% -x + a v v + b v + d 
phi1 :=
  ( ( x >= 74 and x <= 76 and v = 0 ) impl 
    ( x + a*v^2 + b*v + c >= 0 and -x + a*v^2 + b*v + d >= 0 ));

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

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

phi4 :=
  ( ( x + a*v^2 + b*v + c = 0 and -x + a*v^2 + b*v + d >= 0 ) impl
    ( v + 2*a*v + b >= 0 OR  v - 2*a*v - b >= 0 ) );

phi := phi1 and phi2 and phi3 and phi4;

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

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

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

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