11.08., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

Commit 127c052a authored by Mahmoud Mahmoud's avatar Mahmoud Mahmoud

modifications

parent 8deb815a
find ./ -type f -name "*.bdd" -delete
find ./ -type f -name "*.nbdd" -delete
find ./ -type f -name "*.csv" -delete
find ./ -type f -name "*.fsm" -delete
find ./ -type f -name "*.scs" -delete
find ./ -type f -name "*.o" -delete
......@@ -17,6 +20,17 @@ done
cd ../prolonged_ncs_nondet
for dir in *
do
cd ${dir}
make clean
cd scots-files
make clean
cd ..
cd ..
done
cd ../others
for dir in *
do
cd ${dir}
make clean
......
#
# 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 = robot
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
/*
* vehicle.cc
*
* created on: 15.01.2018
* author: M. Khaled
*/
#include <array>
#include <iostream>
#define VERBOSEBASIC
#include "cuddObj.hh"
#include "SENSE.hh"
/* state-space / input-space dimensions */
#define ssDIM 2
#define isDIM 2
/* NCS Delay bounds */
#define NSCMAX 2
#define NCAMAX 2
#define FILE_BDD_REL "scots-files/robot_rel.bdd"
#define FILE_BDD_TS "scots-files/robot_ts.bdd"
#define FILE_NBDD_REL "robot_ncs_rel.nbdd"
#define FILE_NBDD_CONTR "robot_ncs_controller.bdd"
int main() {
Cudd cuddManager;
cout << "Initiating the NCS Transition relation from the original relation ... " << endl;
ncsFIFOTransitionRelation ncsRobot(cuddManager, FILE_BDD_REL, ssDIM, isDIM, NSCMAX, NCAMAX);
cout << "NCS relation intialized !" << endl;
cuddManager.AutodynEnable();
cout << "Expanding transition relation ... " << endl;
ncsRobot.ExpandBDD();
cout << "NCS relation expanded in " << ncsRobot.getExpandTime() << " seconds !" << endl;
cout << "Computing a reach controller ... " << endl;
ncsController ncsContr = ncsRobot.ComputeReachController(FILE_BDD_TS);
cout << "Controller computed in " << ncsContr.getControllerComputeTile() << " seconds !" << endl;
ncsContr.WriteToSCOTS2File(FILE_NBDD_CONTR);
cout << "Synthesized controller is saved to the file: " << FILE_NBDD_CONTR << endl;
return 1;
}
#
# 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 = robot
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 ./*.bdd
/*
* robot.cc
*
* created on: 15.11.2016
* author: M. Khaled
*/
/*
* 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 2
#define iDIM 2
/* data types for the ode solver */
typedef std::array<double,2> state_type;
typedef std::array<double,2> input_type;
/* sampling time */
const double tau = 1;
/* number of intermediate steps in the ode solver */
const int nint=5;
OdeSolver ode_solver(sDIM,nint,tau);
/* we integrate the robot ode by 0.3 sec (the result is stored in x) */
auto robot_post = [](state_type &x, input_type &u) -> void {
/* the ode describing the robot */
auto rhs =[](state_type& xx, const state_type &x, input_type &u) -> void {
double x0=x[0];
x0=x0-1;
xx[0] = u[0];
xx[1] = 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 {
u[0]=u[0];
r[0] = 0;
r[1] = 0;
};
/* forward declaration of the functions to setup the state space
* and input space of the robot example */
scots::SymbolicSet robotCreateStateSpace(Cudd &mgr);
scots::SymbolicSet robotCreateInputSpace(Cudd &mgr);
int main() {
TicToc tt;
Cudd mgr;
/****************************************************************************/
/* construct SymbolicSet for the state space */
/****************************************************************************/
scots::SymbolicSet ss=robotCreateStateSpace(mgr);
ss.writeToFile("robot_ss.bdd");
/* write SymbolicSet of obstacles to robot_obst.bdd */
ss.complement();
ss.writeToFile("robot_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,
1, 0,
0,-1,
0, 1};
/* compute inner approximation of P={ x | H x<= h1 } */
double h1[4] = {-12,13,-12,13};
ts.addPolytope(4,H,h1, scots::OUTER);
double h2[4] = {-12,13,-2,3};
ts.addPolytope(4,H,h2, scots::OUTER);
ts.writeToFile("robot_ts.bdd");
/****************************************************************************/
/* construct SymbolicSet for the input space */
/****************************************************************************/
scots::SymbolicSet is=robotCreateInputSpace(mgr);
is.writeToFile("robot_is.bdd");
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(robot_post, radius_post);
std::cout << std::endl;
tt.toc();
abstraction.getTransitionRelation().writeToFile("robot_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();
/* we implement the nested fixed point algorithm
*
* mu X. nu Y. ( pre(Y) & T ) | pre(X)
*
*/
//BDD C = fp.reach(T, 1);
size_t i,j;
/* outer fp*/
BDD X=mgr.bddOne();
BDD XX=mgr.bddZero();
/* inner fp*/
BDD Y=mgr.bddZero();
BDD YY=mgr.bddOne();
/* the controller */
BDD C=mgr.bddZero();
BDD U=is.getCube();
/* as long as not converged */
for(i=1; XX != X; i++) {
X=XX;
BDD preX=fp.pre(X);
/* init inner fp */
YY = mgr.bddOne();
for(j=1; YY != Y; j++) {
Y=YY;
YY= ( fp.pre(Y) & T ) | preX;
}
XX=YY;
std::cout << "Iterations inner: " << j << std::endl;
/* remove all (state/input) pairs that have been added
* to the controller already in the previous iteration * */
BDD N = XX & (!(C.ExistAbstract(U)));
/* add the remaining pairs to the controller */
C=C | N;
//std::cout << C.CountMinterm(17) << std::endl;
}
std::cout << "Iterations outer: " << i << std::endl;
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("robot_controller.bdd");
return 1;
}
scots::SymbolicSet robotCreateStateSpace(Cudd &mgr) {
/* setup the workspace of the synthesis problem and the uniform grid */
/* lower bounds of the hyper rectangle */
double lb[sDIM]={0,0};
/* upper bounds of the hyper rectangle */
double ub[sDIM]={15,15};
/* grid node distance diameter */
double eta[sDIM]={1,1};
/* 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,
1, 0,
0,-1,
0, 1,};
double h1[4] = {-3,6,-3, 6};
ss.remPolytope(4,H,h1, scots::OUTER);
return ss;
}
scots::SymbolicSet robotCreateInputSpace(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]={1,1};
scots::SymbolicSet is(mgr,iDIM,lb,ub,eta);
is.addGridPoints();
return is;
}
%
% robot.m
%
% created on: 15.11.2016
% author: M. Khaled
%
% see readme file for more information on the vehicle example
%
% you need to run ./robot binary first
%
% so that the files: robot_ss.bdd
% robot_obst.bdd
% robot_target.bdd
% robot_controller.bdd
% are created
%
function robot
clear set
close all
%% Initialization
% simulation time
SIM_STEPS = 100;
SIM_REPEATS = 100;
% initial state
x0=[0 0];
tau = 1;
controller=SymbolicSet('robot_controller.bdd','projection',[1 2]);
target=SymbolicSet('robot_ts.bdd');
%% plot the vehicle domain
% colors
colors=get(groot,'DefaultAxesColorOrder');
% load the symbolic set containig the abstract state space
set=SymbolicSet('robot_ss.bdd');
plotCells(set,'facecolor','none','edgec',[0.8 0.8 0.8],'linew',.1)
hold on
% load the symbolic set containig obstacles
set=SymbolicSet('robot_obst.bdd');
plotCells(set,'facecolor',colors(1,:)*0.5+0.5,'edgec',colors(1,:),'linew',.1)
% load the symbolic set containig target set
set=SymbolicSet('robot_ts.bdd');
plotCells(set,'facecolor',colors(2,:)*0.5+0.5,'edgec',colors(2,:),'linew',.1)
%% Simulation
for s=1:SIM_REPEATS
y=x0;
i=0;
while(i<SIM_STEPS)
u=controller.getInputs(y(end,:));
u_selected = u(ceil(rand*size(u,1)),:);
%if (target.isElement(y(end,:)))
% break;
%end
[t x]=ode45(@robot_ode,[0 tau], y(end,:),[],u_selected);
y=[y; x(end,:)];
i = i+1;
end
%% plot initial state and trajectory
plot(y(:,1),y(:,2),'k.-')
plot(y(1,1),y(1,2),'.','color',colors(5,:),'markersize',20)
end
box on
axis([-.5 15.5 -.5 15.5])
end
function dxdt = robot_ode(t,x,u)
dxdt = zeros(2,1);
dxdt(1)=u(1);
dxdt(2)=u(2);
end
#
# 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 = state13
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 = clang++
CXXFLAGS = -Wall -Wextra -std=c++11 -DNDEBUG -g
#
# 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 = state13
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 ./*.bdd
/*
* fifo.cc
*
* created on: 16.08.2016
* author: M. Khaled
*/
#include <array>
#include <iostream>
#include "cuddObj.hh"
#include "SymbolicSet.hh"
#include "SymbolicModelGrowthBound.hh"
#include "SymbolicModel.hh"
#include "TicToc.hh"
#include "RungeKutta4.hh"
#include "FixedPoint.hh"
using namespace std;
using namespace scots;
#define SS_DIM 1
#define IS_DIM 1
typedef array<double,1> state_type;
typedef array<double,1> input_type;
bool cbFunc_add_ts(double* x);
bool cbFunc_add_obs(double* x);
void sys_post(state_type &x, input_type &u);
void r_post(state_type &r, input_type &u);
int main() {
system("rm *.bdd");
/* to measure time */
TicToc tt;
/* there is one unique manager to organize the bdd variables */
Cudd mgr;
double sslb[1]={1};
double ssub[1]={13};
double sseta[1]={1};
double islb[1]={1};
double isub[1]={2};
double iseta[1]={1};
/****************************************************************************/
/* construct SymbolicSet for the state space and input */
/****************************************************************************/
SymbolicSet ss(mgr,SS_DIM,sslb,ssub,sseta);
ss.addGridPoints();
ss.writeToFile("state13_ss.bdd");
SymbolicSet is(mgr,IS_DIM,islb,isub,iseta);
is.addGridPoints();
is.writeToFile("state13_is.bdd");
SymbolicSet sspost(mgr,SS_DIM,sslb,ssub,sseta);
sspost.addGridPoints();
sspost.writeToFile("state13_sspost.bdd");
/****************************************************************************/
/* construct SymbolicSet for the obstacles */
/****************************************************************************/
/* first make a copy of the state space so that we obtain the grid
* information in the new symbolic set */
SymbolicSet obs(ss);
obs.addByFunction(cbFunc_add_obs);
obs.writeToFile("state13_obst.bdd");
/****************************************************************************/
/* 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 */
SymbolicSet ts(ss);
ts.addByFunction(cbFunc_add_ts);
ts.writeToFile("state13_ts.bdd");
/****************************************************************************/
/* we define t fhe abstraction */
/****************************************************************************/
SymbolicModelGrowthBound<state_type, input_type> abstraction(&ss,&is,&sspost);
abstraction.computeTransitionRelation(sys_post, r_post);
abstraction.getTransitionRelation().writeToFile("state13_rel.bdd");
/****************************************************************************/
/* we continue with the controller synthesis */
/****************************************************************************/
/* we setup a fixed point object to compute reachabilty controller */
FixedPoint fp(&abstraction);
/* the fixed point algorithm operates on the BDD directly */
BDD T = ts.getSymbolicSet();
//BDD O = obs.getSymbolicSet();
/* compute controller */
//BDD C=fp.reachAvoid(T,O,1);
BDD C=fp.reach(T,1);
/****************************************************************************/
/* 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("state13_controller.bdd");
return 1;
}
bool cbFunc_add_ts(double* x)
{
if(x[0] == 12)
return true;
else
return false;
}
bool cbFunc_add_obs(double* x)
{
if(x[0] == 11 || x[0] == 8)
return true;
else
return false;
}
void sys_post(state_type &x, input_type &u)
{
if(x[0] == 1 && u[0] == 1) { x[0] = 2; return; }
if(x[0] == 1 && u[0] == 2) { x