%% 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]
%% Safe whenever f < 8.91; no restriction on e.

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;

%% 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=e AND vel = f ] 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 >= 0] 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 >= 0] impl [  -4*vel*c - vel + acc*a - 3*acc*c + 3*fvel*c + fvel + gap*c - 10*c >= 0  ]];

%% Correctness formula
phi := phi1 and phi2 and phi3;

%% Condition on e,f s.t. the system is proved safe
psi := rlqe ex({a,b,c},all({gap,acc,vel,fvel}, phi1 and phi2 and phi3));

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