%% Train gate controller example from VMCAI 2009 paper.
%% Dynamics: 2 MODES:
%% gdot = -10 or 0;;  xdot = -50; 
%% template: x + a*g - b >= 0
%% Safety: x >= g
%% The result of rlqe, after simplifying with slfq, yields:
%% a + 5 <= 0 /\ b - 90 a - 1000 <= 0 /\ b >= 0
%% gqe and qe yield identical result.

load_package 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
		      % default is (only) 1 * 10^6.
rlqepcadl(200*10^3);  % The size of the prime list used by QEPCAD. The
		      % default is (only) 2 * 10^3.
on rlverbose;
on time;
off rlqefb;		% No fallback QE


phi := ( ( x > 1000    AND  g = 90   ) impl (g >= 0 AND x + g*a - b >= 0)) and
  [ [g >= 0 AND x + g*a - b >= 0] impl [ x=0 impl g = 0  ]] AND
  [ [ g = 0 AND x + g*a - b >= 0 ] impl [  -10 >= 0  OR  0 >= 0  ] ]  AND
  [ [ g >= 0 AND x + g*a - b = 0 ] impl [  -10*a - 50 >= 0  OR  -50 >= 0  ] ]$

psi := rlgqe( all({x,g}, phi) );

psi := second psi;

psi2 := rlqepcad( rlex(psi), "train-gate.qepcad" )$
off nat;	% Output same syntax as input (for reduce)
out "train-gate.out";
psi;
psi2;
shut "train-gate.out";
end;

end;
%redlog give
% a<=-5 and b>=0 and 90a-b+1000>=0