Commit d7cda510 authored by Mahmoud Mahmoud's avatar Mahmoud Mahmoud

modifications

parent 0d5286c5
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -g
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
#
# compiler
#
CC = g++
CXXFLAGS = -Wall -Wextra -std=c++11 -g -O0
#
# ncsAct
#
NCSACTROOT = ../../..
NCSACTINC = -I$(NCSACTROOT)/src -I$(NCSACTROOT)/utils
#
# cudd
#
CUDDPATH = /opt/local
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = vehicle
all: $(TARGET)
%.o:%.cc
$(CC) -c $(CXXFLAGS) $(CUDDINC) $(NCSACTINC) $< -o $@
$(TARGET): $(TARGET).o
$(CC) $(CXXFLAGS) -o $(TARGET) $(TARGET).o $(CUDDLPATH) $(CUDDLIBS)
clean:
rm ./$(TARGET) ./$(TARGET).o
This is an exxample of using SENSE and saving the output as BDD compatible with SCOTS v2.0.
\ No newline at end of file
#
# compiler
#
#CC = g++
CC = clang++
CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
# cudd
#
CUDDPATH = /opt/local
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = vehicle
all: $(TARGET)
%.o:%.cc
$(CC) -c $(CXXFLAGS) $(CUDDINC) $(SCOTSINC) $< -o $@
$(TARGET): $(TARGET).o
$(CC) $(CXXFLAGS) -o $(TARGET) $(TARGET).o $(CUDDLPATH) $(CUDDLIBS)
clean:
rm ./$(TARGET) ./$(TARGET).o
/*
* vehicle_exp2.cc
*
* created on: 30.09.2015
* author: rungger
*/
/*
* information about this example is given in the readme file
*
*/
#include <array>
#include <iostream>
#include "cuddObj.hh"
#include "SymbolicSet.hh"
#include "SymbolicModelGrowthBound.hh"
#include "TicToc.hh"
#include "RungeKutta4.hh"
#include "FixedPoint.hh"
/* state space dim */
#define sDIM 3
#define iDIM 2
/* data types for the ode solver */
typedef std::array<double,3> state_type;
typedef std::array<double,2> input_type;
/* sampling time */
const double tau = 0.3;
/* number of intermediate steps in the ode solver */
const int nint=5;
OdeSolver ode_solver(sDIM,nint,tau);
/* we integrate the vehicle ode by 0.3 sec (the result is stored in x) */
auto vehicle_post = [](state_type &x, input_type &u) -> void {
/* the ode describing the vehicle */
auto rhs =[](state_type& xx, const state_type &x, input_type &u) -> void {
double alpha=std::atan(std::tan(u[1])/2.0);
xx[0] = u[0]*std::cos(alpha+x[2])/std::cos(alpha);
xx[1] = u[0]*std::sin(alpha+x[2])/std::cos(alpha);
xx[2] = u[0]*std::tan(u[1]);
};
ode_solver(rhs,x,u);
};
/* computation of the growth bound (the result is stored in r) */
auto radius_post = [](state_type &r, input_type &u) -> void {
double c = std::abs(u[0]*std::sqrt(std::tan(u[1])*std::tan(u[1])/4.0+1));
r[0] = r[0]+c*r[2]*0.3;
r[1] = r[1]+c*r[2]*0.3;
};
/* forward declaration of the functions to setup the state space
* and input space of the vehicle example */
scots::SymbolicSet vehicleCreateStateSpace(Cudd &mgr);
scots::SymbolicSet vehicleCreateInputSpace(Cudd &mgr);
int main() {
/* to measure time */
TicToc tt;
/* there is one unique manager to organize the bdd variables */
Cudd mgr;
/****************************************************************************/
/* construct SymbolicSet for the state space */
/****************************************************************************/
scots::SymbolicSet ss=vehicleCreateStateSpace(mgr);
ss.writeToFile("vehicle_ss.bdd");
/* write SymbolicSet of obstacles to vehicle_obst.bdd */
ss.complement();
ss.writeToFile("vehicle_obst.bdd");
ss.complement();
std::cout << "Unfiorm grid details:" << std::endl;
ss.printInfo(1);
/****************************************************************************/
/* we define the target set */
/****************************************************************************/
/* first make a copy of the state space so that we obtain the grid
* information in the new symbolic set */
scots::SymbolicSet ts = ss;
/* define the target set as a symbolic set */
double H[4*sDIM]={-1, 0, 0,
1, 0, 0,
0,-1, 0,
0, 1, 0};
/* compute inner approximation of P={ x | H x<= h1 } */
double h[4] = {-8.4,10,-0,2};
ts.addPolytope(4,H,h, scots::INNER);
ts.writeToFile("vehicle_ts.bdd");
/****************************************************************************/
/* construct SymbolicSet for the input space */
/****************************************************************************/
scots::SymbolicSet is=vehicleCreateInputSpace(mgr);
std::cout << std::endl << "Input space details:" << std::endl;
is.printInfo(0);
/****************************************************************************/
/* setup class for symbolic model computation */
/****************************************************************************/
/* first create SymbolicSet of post variables
* by copying the SymbolicSet of the state space and assigning new BDD IDs */
scots::SymbolicSet sspost(ss,1);
/* instantiate the SymbolicModel */
scots::SymbolicModelGrowthBound<state_type,input_type> abstraction(&ss, &is, &sspost);
/* compute the transition relation */
tt.tic();
abstraction.computeTransitionRelation(vehicle_post, radius_post);
std::cout << std::endl;
tt.toc();
abstraction.getTransitionRelation().writeToFile("vehicle_rel.bdd");
/* get the number of elements in the transition relation */
std::cout << std::endl << "Number of elements in the transition relation: " << abstraction.getSize() << std::endl;
/****************************************************************************/
/* we continue with the controller synthesis */
/****************************************************************************/
/* we setup a fixed point object to compute reachabilty controller */
scots::FixedPoint fp(&abstraction);
/* the fixed point algorithm operates on the BDD directly */
BDD T = ts.getSymbolicSet();
/* the output of the fixed point computation are two bdd's */
tt.tic();
BDD C = fp.reach(T, 1);
tt.toc();
/****************************************************************************/
/* last we store the controller as a SymbolicSet
* the underlying uniform grid is given by the Cartesian product of
* the uniform gird of the space and uniform gird of the input space */
/****************************************************************************/
scots::SymbolicSet controller(ss,is);
controller.setSymbolicSet(C);
controller.writeToFile("vehicle_controller.bdd");
return 1;
}
scots::SymbolicSet vehicleCreateStateSpace(Cudd &mgr) {
/* setup the workspace of the synthesis problem and the uniform grid */
/* lower bounds of the hyper rectangle */
double lb[sDIM]={0,0,-M_PI-0.4};
/* upper bounds of the hyper rectangle */
double ub[sDIM]={10,10,M_PI+0.4};
/* grid node distance diameter */
double eta[sDIM]={.2,.2,.2};
/* eta is added to the bound so as to ensure that the whole
* [0,10]x[0,10]x[-pi-eta,pi+eta] is covered by the cells */
scots::SymbolicSet ss(mgr,sDIM,lb,ub,eta);
/* add the grid points to the SymbolicSet ss */
ss.addGridPoints();
/* remove the obstacles from the state space */
/* the obstacles are defined as polytopes */
/* define H* x <= h */
double H[4*sDIM]={-1, 0, 0,
1, 0, 0,
0,-1, 0,
0, 1, 0};
/* remove outer approximation of P={ x | H x<= h1 } form state space */
double h1[4] = {-1,1.2,-0, 9};
ss.remPolytope(4,H,h1, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h2 } form state space */
double h2[4] = {-2.2,2.4,-0,5};
ss.remPolytope(4,H,h2, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h3 } form state space */
double h3[4] = {-2.2,2.4,-6,10};
ss.remPolytope(4,H,h3, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h4 } form state space */
double h4[4] = {-3.4,3.6,-0,9};
ss.remPolytope(4,H,h4, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h5 } form state space */
double h5[4] = {-4.6 ,4.8,-1,10};
ss.remPolytope(4,H,h5, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h6 } form state space */
double h6[4] = {-5.8,6,-0,6};
ss.remPolytope(4,H,h6, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h7 } form state space */
double h7[4] = {-5.8,6,-7,10};
ss.remPolytope(4,H,h7, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h8 } form state space */
double h8[4] = {-7,7.2,-1,10};
ss.remPolytope(4,H,h8, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h9 } form state space */
double h9[4] = {-8.2,8.4,-0,8.5};
ss.remPolytope(4,H,h9, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h10 } form state space */
double h10[4] = {-8.4,9.3,-8.3,8.5};
ss.remPolytope(4,H,h10, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h11 } form state space */
double h11[4] = {-9.3,10,-7.1,7.3};
ss.remPolytope(4,H,h11, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h12 } form state space */
double h12[4] = {-8.4,9.3,-5.9,6.1};
ss.remPolytope(4,H,h12, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h13 } form state space */
double h13[4] = {-9.3,10 ,-4.7,4.9};
ss.remPolytope(4,H,h13, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h14 } form state space */
double h14[4] = {-8.4,9.3,-3.5,3.7};
ss.remPolytope(4,H,h14, scots::OUTER);
/* remove outer approximation of P={ x | H x<= h15 } form state space */
double h15[4] = {-9.3,10 ,-2.3,2.5};
ss.remPolytope(4,H,h15, scots::OUTER);
return ss;
}
scots::SymbolicSet vehicleCreateInputSpace(Cudd &mgr) {
/* lower bounds of the hyper rectangle */
double lb[sDIM]={-1,-1};
/* upper bounds of the hyper rectangle */
double ub[sDIM]={1,1};
/* grid node distance diameter */
double eta[sDIM]={.3,.3};
scots::SymbolicSet is(mgr,iDIM,lb,ub,eta);
is.addGridPoints();
return is;
}
%
% vehicle.m
%
% created on: 09.10.2015
% author: rungger
%
% see readme file for more information on the vehicle example
%
% you need to run ./vehicle binary first
%
% so that the files: vehicle_ss.bdd
% vehicle_obst.bdd
% vehicle_target.bdd
% vehicle_controller.bdd
% are created
%
function vehicle
clear set
close all
%% simulation
% target set
lb=[9 0];
ub=lb+0.5;
v=[9 0; 9.5 0; 9 0.5; 9.5 .5];
% initial state
x0=[0.4 0.4 0];
controller=SymbolicSet('vehicle_controller.bdd','projection',[1 2 3]);
target=SymbolicSet('vehicle_target.bdd');
y=x0;
v=[];
while(1)
u=controller.getInputs(y(end,:));
v=[v; u(1,:)];
if (target.isElement(y(end,:)))
break;
end
[t x]=ode45(@unicycle_ode,[0 .3], y(end,:),[],u(1,:));
y=[y; x(end,:)];
end
%% plot the vehicle domain
% colors
colors=get(groot,'DefaultAxesColorOrder');
% load the symbolic set containig the abstract state space
set=SymbolicSet('vehicle_ss.bdd','projection',[1 2]);
plotCells(set,'facecolor','none','edgec',[0.8 0.8 0.8],'linew',.1)
hold on
% load the symbolic set containig obstacles
set=SymbolicSet('vehicle_obst.bdd','projection',[1 2]);
plotCells(set,'facecolor',colors(1,:)*0.5+0.5,'edgec',colors(1,:),'linew',.1)
% plot the real obstacles and target set
plot_domain
% load the symbolic set containig target set
set=SymbolicSet('vehicle_target.bdd','projection',[1 2]);
plotCells(set,'facecolor',colors(2,:)*0.5+0.5,'edgec',colors(2,:),'linew',.1)
% plot initial state and trajectory
plot(y(:,1),y(:,2),'k.-')
plot(y(1,1),y(1,1),'.','color',colors(5,:),'markersize',20)
box on
axis([-.5 10.5 -.5 10.5])
end
function dxdt = unicycle_ode(t,x,u)
dxdt = zeros(3,1);
c=atan(tan(u(2)/2));
dxdt(1)=u(1)*cos(c+x(3))/cos(c);
dxdt(2)=u(1)*sin(c+x(3))/cos(c);
dxdt(3)=u(1)*tan(u(2));
end
function plot_domain
colors=get(groot,'DefaultAxesColorOrder');
v=[9 0; 9.5 0; 9 0.5; 9.5 .5];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(2,:),'edgec',colors(2,:));
v=[1 0 ;1.2 0 ; 1 9 ; 1.2 9 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[2.2 0 ;2.4 0 ; 2.2 5 ; 2.4 5 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[2.2 6 ;2.4 6 ; 2.2 10 ; 2.4 10 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[3.4 0 ;3.6 0 ; 3.4 9 ; 3.6 9 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[4.6 1 ;4.8 1 ; 4.6 10 ; 4.8 10 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[5.8 0 ;6 0 ; 5.8 6 ; 6 6 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[5.8 7 ;6 7 ; 5.8 10 ; 6 10 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[7 1 ;7.2 1 ; 7 10 ; 7.2 10 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[8.2 0 ;8.4 0 ; 8.2 8.5 ; 8.4 8.5 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[8.4 8.3;9.3 8.3 ; 8.4 8.5 ; 9.3 8.5 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[9.3 7.1;10 7.1 ; 9.3 7.3 ; 10 7.3 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[8.4 5.9;9.3 5.9 ; 8.4 6.1 ; 9.3 6.1 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[9.3 4.7;10 4.7 ; 9.3 4.9 ; 10 4.9 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[8.4 3.5;9.3 3.5 ; 8.4 3.7 ; 9.3 3.7 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
v=[9.3 2.3;10 2.3 ; 9.3 2.5 ; 10 2.5 ];
patch('vertices',v,'faces',[1 2 4 3],'facec',colors(1,:),'edgec',colors(1,:));
end
/*
* vehicle.cc
*
* created on: 31.08.2015
* author: M. Khaled
*/
#include <array>
#include <iostream>
#define VERBOSEBASIC
#include "cuddObj.hh"
#include "SENSE.hh"
#include "SCOTS2Interface.hh"
/* state-space / input-space dimensions */
#define ssDIM 3
#define isDIM 2
/* NCS Delay bounds */
#define NSCMAX 2
#define NCAMAX 2
#define FILE_BDD_REL "scots-files/vehicle_rel.bdd"
#define FILE_NBDD_REL "vehicle_rel.nbdd"
int main() {
Cudd cuddManager;
cout << "Initiating the NCS Transition relation from the original relation ... " << endl;
ncsFIFOTransitionRelation ncsState13(cuddManager, FILE_BDD_REL, ssDIM, isDIM, NSCMAX, NCAMAX);
cout << "NCS relation intialized !" << endl;
cuddManager.AutodynEnable();
cout << "Expanding transition relation ... " << endl;
ncsState13.ExpandBDD();
cout << "NCS relation expanded in " << ncsState13.getExpandTime() << " seconds !" << endl;
ncsState13.WriteToFile(FILE_NBDD_REL);
cout << "New expanded transition relation is saved to the file: " << FILE_NBDD_REL << endl;
return 1;
}
......@@ -7,7 +7,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -DNDEBUG -g
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -8,7 +8,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -7,7 +7,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
......@@ -7,7 +7,7 @@ CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSROOT = ../../../../lib/scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
......
#
# compiler
#
CC = g++
CXXFLAGS = -Wall -Wextra -std=c++11 -g -O0
#
# ncsAct
#
NCSACTROOT = ../../..
NCSACTINC = -I$(NCSACTROOT)/src -I$(NCSACTROOT)/utils
#
# cudd