%% Adaptive Cruise Control Example from HSCC 2003 paper
%% Dynamics: vel = acc, acc = -3 acc - 4 vel + 3 fvel + gap - 10, gap = fvel - vel
%% Safe: gap > 0
%% Template: [vel*a + acc*c + fvel*b + gap - 2 >= 0]
%% We put fvel = p in the antecedent; assuming front car has zero acc.
%% The resulting formula is BIG, but it has a case p >= 5!!
%% No condition on rear-car-init-velocity q.
%% This indicates we have safety whenever front-car-vel >= 5.
%% If we simulate with rear-car-init-vel = 30, we get a collision;
%% so what is wrong?  That trajectory violates our state invariant;
%% namely it requires a to go below -5.

%on echo;
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;

%% Find initial states for which a linear invariant will prove safety

%% Init: if x is an initial states then x is in the invariant
phi1 :=   [[ gap = 10 AND acc = 0 AND fvel=p AND vel = q ] impl [vel*a + acc*c + fvel*b + gap - 2 >= 0]];

%% Safe: if x is in the invariant, then x is in Safe.
phi2 := [[vel*a + acc*c + fvel*b + gap - 2 >= 0 and acc > -5 and acc < 2 and vel > 0 and fvel = p ] impl [ gap >= 0   ]];

%% Induct: if x is on the bdary of the invariant, then vector field points inwards (barrier)
phi3 := [[ vel*a + acc*c + fvel*b + gap - 2 = 0 and acc > -5 and acc < 2 and 
   vel > 0 and fvel = p ] impl 
 [  -4*vel*c - vel + acc*a - 3*acc*c + 3*fvel*c + fvel + gap*c - 10*c >= 0  ]];

phi := phi1 and phi2 and phi3;

psi := rlgqe ex({a,b,c},all({gap,acc,vel,fvel}, phi))$

psi := second psi$

rlqepcad( psi, "acc0b.qepcad");

end;

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

out "acc0b.out";
psi;
shut "acc0b.out";

end;
%% 11*f^3  - 152*f^2  + 512*f - 512 <= 0 or e^3  + 3*e^2 *f - 48*e^2  - 14*e*f^2  + 176*e*f - 320*e + 11*f^3  - 152*f^2  + 512*f - 512 <= 0
%% woframalpha says: f < 8.91