%% 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 >= its_init_value]
%% ASSUMING vel remain between 20 and 30 during manuever
%% And fvel is set at 25;  for any f = vel(0), safety holds.

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;		% No fallback QE

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

%% Init: if x is an initial states then x is in the invariant
%% init is trivially satisfies since RHS of template is defined by init!
%% Template: [vel*a + acc*c + fvel*b + gap >= its_init_value]
%phi1 := (f*a + e*b + 10 <= 0);
% Initially the value of function V := vel*a+acc*c+fvel*b+gap is negative.
phi1 := (f*a + 25*b + 10 <= 0);

%% Safe: if x is in the invariant, then x is in Safe.
%phi2 := [[vel*a + acc*c + fvel*b + gap >= f*a + 25*b + 10  and acc > -5 and acc < 2 and vel >= 20 and fvel >= 20 and vel<=30 and fvel<=30] impl [gap >= 0]];
phi21 := ( a+md-mf=0 and b+me-mg=0 and c + mb - mc = 0 and 
 0 >= -f*a-25*b-10+5*mb+2*mc-20*md-20*mf+30*me+30*mg and 
 mb >= 0 and mc >= 0 and md >=0 and me >= 0 and mf >= 0 and mg >= 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 <= 0 and acc > -5 and acc < 2 and vel >= 20 and fvel >= 20 and vel <= 30 and fvel <= 30] impl 
%%  [ acc*a - 4*vel*c - 3*acc*c + 3*fvel*c + gap*c - 10*c + fvel - vel >= 0  ]];
phi31 := (-c >= 0 and a - 3*c = c^2 + lb - lc and 
 -4*c-1 = a*c + ld - lf and 3*c+1 = b*c + le - lg and 
 -10*c >= 5*lb + 2*lc - 20*ld - 20*le + 30*lf + 30*lg and 
 lb >= 0 and lc >= 0 and ld >= 0 and le >= 0 and lf >= 0 and lg >= 0);

%% Correctness formula
phi := phi1 and phi21 and phi31;

%% Condition on e,f s.t. safety holds
psi := rlqe ex({a,b,c,mb,mc,md,me,mf,mg,lb,lc,ld,le,lf,lg}, phi);

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

%out "acc3.out";
%psi;
%shut "acc3.out";

end;

%% given to QEPCAD
%% (E c) [[[c^4 f + 8 c^3 f + 5 c^3 + 3 c^2 e + 10 c^2 + c e >= 0 /\ c^4 f + 8 c^3 f - 2 c^3 + 3 c^2 e + 10 c^2 + c e >= 0 /\ c^4 f + 8 c^3 f + 3 c^2 e + 10 c^2 + c e <= 0 /\ c^3 + 8 c^2 + 4 c + 1 <= 0 /\ 3 c^2 + c <= 0 /\ c^2 + 8 c <= 0 /\ c < 0] \/ [c^4 + 8 c^3 + 4 c^2 + c <= 0 /\ c^4 + c^3 + 4 c^2 + c >= 0 /\ 5 c^3 + 3 c^2 e - 4 c^2 f + 10 c^2 + c e - c f >= 0 /\ 2 c^3 - 3 c^2 e + 4 c^2 f - 10 c^2 - c e + c f <= 0 /\ 3 c^2 e - 4 c^2 f + 10 c^2 + c e - c f <= 0 /\ 4 c^2 + c >= 0 /\ 3 c^2 + c <= 0 /\ c < 0]]].
%% (E c) [[
%[c^4 + 8 c^3 + 4 c^2 + c <= 0 /\ 
% c^4 + c^3 + 4 c^2 + c >= 0 /\ 
% 5 c^3 + 3 c^2 e - 4 c^2 f + 10 c^2 + c e - c f >= 0 /\ 
% 3 c^2 e - 4 c^2 f + 10 c^2 + c e - c f <= 0 /\ 
% 4 c^2 + c >= 0 /\ 3 c^2 + c <= 0 ]]].

% This is shown to be equivalent to TRUE.
% That means  there is no constraint on f !