%% 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*v + b*x + c
%% -v^2 - a*v - b*x + d
%% In this case, we FAIL; 
%% We get a constraint on a,b,c,d, which is shown to be
%% FALSE by slfq, but not by qepcad in reasoble time.

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

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

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

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

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

phi := phi1 and phi2 and phi3 and phi4;

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

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

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

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