%% 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:
%%  a t - p p + b p + c 
%% -a t - p p + b p + d 
%% We FAIL. We should find a solution. 
%% If we subtitute a by 2, we find a solution immediately.
%% slfq can simplify each conjunct.  It fails to simplify the
%% whole formula I think.  Perhaps we need to simplify and retry qepcad.

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 
   ( a*x - v^2 + b*v + c >= 0 and  -a*x - v^2 + b*v + d >= 0) );

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

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

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

phi := phi1 and phi2 and phi3 and phi4;

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

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

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

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