%% Redlog file for NAV (Navigation benchmarks) relational abstraction.
%% Results:
%% For continuous mode that goes EAST; i.e.,
%% 4-d system with dynamics:
%% dx/dt = vx,  dvx/dt = -1.2 (vx-vx0) + 0.1 (vy-vy0)
%% dy/dt = vy,  dvy/dt =  0.1 (vx-vx0) - 1.2 (vy-vy0)
%% Assume we are going east; so vx0 = 1, vy0 = 0
%% We get following invariants: R(xinit,yinit,vxinit,vyinit,x,y,vx,vy):
%%  (vxinit-1)+-vyinit >= 0 => 0 <= (vx-1) +- vy <= (vxinit-1) +- vyinit
%%  (vxinit-1)+-vyinit <= 0 => 0 >= (vx-1) +- vy >= (vxinit-1) +- vyinit
%%         +- means we can choose either + or -
%%  (y - yinit) + 10/143*(vx - vxinit) + 120/143*(vy - vyinit) = 0
%%  (x - xinit) + (vx - vxinit) + 2*(vy - vyinit) + 2.3*(y - yinit) >= 0
%% There are infinitely many invariants of the last form.
%% I picked coefficients 1,2,2.3 arbitrarily.
%% We just need to ensure b=12a-10 and 10c = 12b-a
%% where a is coeff of (vx-vxinit), b of (vy-vyinit), c of (y-yinit)

on echo;
load_package redlog;
rlset r;
load_package qepcad;
on rlqefbqepcad;
rlqepcadn(100*10^6);
rlqepcadl(200*10^3);
on rlverbose;
on time;
%off rlqefb;

% 8 directions in the NAV benchmarks
north := {dx = 0, dy = 1}$
south := {dx = 0, dy = -1}$
east := {dx = 1, dy = 0}$
west := {dx = -1, dy = 0}$
southeast := {dx = 0.7, dy = -0.7}$
southwest := {dx = -0.7, dy = -0.7}$
northwest := {dx = -0.7, dy = 0.7}$
northeast := {dx = 0.7, dy = 0.7}$
directions := {north, northeast, east, southeast, south, southwest, west, northwest}$

% nav01, nav07, nav09, nav10 dynamics: 
% nav02-05 is the same as nav01, nav08 is the same as nav07
nav01 := {a11 = -12/10, a12 = 1/10, a21 = 1/10, a22 = -12/10}$
nav07 := {a11 = -0.8, a12 = -0.2, a21 = 0.2, a22 = -0.8}$
nav09 := {a11 = -1.8, a12 = -0.2, a21 = -0.2, a22 = -1.8}$
nav10 := {a11 = -0.8, a12 = -0.1, a21 = -0.2, a22 = -0.8}$
examples := {nav01, nav07, nav09, nav10}$

% Navigation Benchmark Dynamics (parametric)
dynamics := 
 {ydot = vy, xdot = vx, vxdot = a11*(vx-dx)+a12*(vy-dy), vydot = a21*(vx-dx)+a22*(vy-dy)}$

% Possible assumptions: Assumption to be made, if any
% Stronger assumptions lead to stronger invariants
assume0 := true;
assume1 := (vx >= -12/10 and vx <= 12/10 and vy >= -12/10 and vy <= 12/10)$
assume2 := (vxinit >= -12/10 and vxinit <= 12/10 and 
	vyinit >= -12/10 and vyinit <= 12/10)$
assume3 := (xinit >= 0 and xinit <= 5 and yinit >= 0 and yinit <= 5)$
assume4 := (x >= 0 and x <= 5 and y >= 0 and y <= 5)$
assume5 := assume1 and assume2 and assume3 and assume4$

% Possible templates
eigentemplate := vxdot + a * vydot - l * ((vx - dx) + a*(vy - dy)) $
affinetemplate := (a*xdot + b*ydot + c*vxdot + d*vydot)$
alltemplates := {eigentemplate, affinetemplate}$
template := affinetemplate$

% Make all choices here
assume := assume5;

% With assume0, Time = 60ms for >=,  70ms for =
% With assume5, Time = 340ms for =,  6740ms for >=
for each i in alltemplates collect
 for each j in directions collect
  for each k in examples collect
   rlqe(ex(l,l<0 and all({x,y,vx,vy,vxinit,vyinit,xinit,yinit}, 
 	assume impl (sub(j, sub(k, sub(dynamics, i))) >= 0 ) )));

end$