Commit 137cfff4 authored by MK's avatar MK
Browse files

First commit

parents
File added
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<?fileVersion 4.0.0?><cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
<storageModule moduleId="org.eclipse.cdt.core.settings">
<cconfiguration id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.673534307">
<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.673534307" moduleId="org.eclipse.cdt.core.settings" name="Build (GNU)">
<externalSettings/>
<extensions>
<extension id="org.eclipse.cdt.core.MachO64" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.Cygwin_PE" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.PE" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.GNU_ELF" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
</extensions>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<configuration buildProperties="" id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.673534307" name="Build (GNU)" parent="org.eclipse.cdt.build.core.emptycfg">
<folderInfo id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.673534307.1090946054" name="/" resourcePath="">
<toolChain id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.1643548950" name="GNU Autotools Toolchain" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolChain">
<targetPlatform id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.targetPlatform.360436042" isAbstract="false" name="GNU Autotools Target Platform" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.targetPlatform"/>
<builder id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.builder.1751677527" managedBuildOn="false" name="Autotools Makefile Generator.Build (GNU)" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.builder"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.gnu.toolchain.tool.configure.1895789128" name="configure" superClass="org.eclipse.linuxtools.cdt.autotools.core.gnu.toolchain.tool.configure"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.autogen.2090351233" name="autogen.sh" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.autogen"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gcc.480962648" name="GCC C Compiler" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gcc">
<inputType id="cdt.managedbuild.tool.gnu.c.compiler.input.260835825" superClass="cdt.managedbuild.tool.gnu.c.compiler.input"/>
</tool>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gpp.270365064" name="GCC C++ Compiler" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gpp">
<inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.886869747" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/>
</tool>
</toolChain>
</folderInfo>
</configuration>
</storageModule>
<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/>
</cconfiguration>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<project id="ncsact-ex-dint.null.1426002170" name="ncsact-ex-dint"/>
</storageModule>
<storageModule moduleId="scannerConfiguration">
<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
</storageModule>
<storageModule moduleId="org.eclipse.cdt.core.LanguageSettingsProviders"/>
<storageModule moduleId="refreshScope"/>
<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"/>
</cproject>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>ncsact-ex-dint</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
<triggers>clean,full,incremental,</triggers>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.cdt.managedbuilder.core.ScannerConfigBuilder</name>
<triggers>full,incremental,</triggers>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.cdt.core.cnature</nature>
<nature>org.eclipse.cdt.core.ccnature</nature>
<nature>org.eclipse.cdt.managedbuilder.core.managedBuildNature</nature>
<nature>org.eclipse.cdt.managedbuilder.core.ScannerConfigNature</nature>
</natures>
</projectDescription>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<project>
<configuration id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.673534307" name="Build (GNU)">
<extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
<provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
<provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
<provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuildCommandParser" id="org.eclipse.cdt.autotools.core.LibtoolGCCBuildCommandParser" keep-relative-paths="false" name="CDT Libtool GCC Build Output Parser" parameter="(libtool:\s+compile:\s+)?((g?cc)|([gc]\+\+)|(clang))" prefer-non-shared="true"/>
<provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuiltinSpecsDetector" console="false" env-hash="1362322948582132066" id="org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector" keep-relative-paths="false" name="CDT GCC Built-in Compiler Settings" parameter="${COMMAND} ${FLAGS} -E -P -v -dD &quot;${INPUTS}&quot;" prefer-non-shared="true">
<language-scope id="org.eclipse.cdt.core.gcc"/>
<language-scope id="org.eclipse.cdt.core.g++"/>
</provider>
<provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
</extension>
</configuration>
</project>
#
# 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 = dint_ncs
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
/*
* dint_ncs.cc
*
* created on: 31.08.2015
* 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 1
/* NCS Delay bounds */
#define NSCMAX 3
#define NCAMAX 3
#define FILE_BDD_REL "scots-files/dint_rel.bdd"
#define FILE_BDD_TS "scots-files/dint_ts.bdd"
#define FILE_NBDD_REL "dint_rel.nbdd"
#define FILE_NBDD_CONTR "dint_contr.nbdd"
int main() {
Cudd cuddManager;
cuddManager.AutodynEnable();
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;
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;
cout << "Computing a reach controller ... " << endl;
ncsController ncsContr = ncsState13.ComputeReachController(FILE_BDD_TS);
cout << "Controller computed in " << ncsContr.getControllerComputeTile() << " seconds !" << endl;
ncsContr.WriteToFile(FILE_NBDD_CONTR);
cout << "Synthesized controller is saved to the file: " << FILE_NBDD_CONTR << endl;
return 1;
}
%
% dintncs.m
%
% created on: 04.10.2016
% author: M. Khaled
%
% you need to run ./dint_ncs binary first
%
% so that the file: dint_cont.nbdd is created
%
function dint
clear set
close all
clear all
clc
% initial state of the original system (non NCS)
x0 = [0.6 0.6];
u0 = 0.9;
% NCS
Nscmax = 3;
Ncamax = 3;
%% 1] load the symbolic sets
contr = ncsFIFOController('dint_contr.nbdd');
%% 2] plotting !
% colors
colors=get(groot,'DefaultAxesColorOrder');
% load the symbolic set containig the abstract state space
set=SymbolicSet('scots-files/dint_ss.bdd');
plotCells(set,'facecolor','none','edgec',[0.8 0.8 0.8],'linew',.1)
hold on
% load the symbolic set containig target set
set=SymbolicSet('scots-files/dint_ts.bdd');
plotCells(set,'facecolor',colors(2,:)*0.5+0.5,'edgec',colors(2,:),'linew',.1)
box on
axis([0.3 3.7 0 3.7])
%% 3] Simulation
for i=1:20
buffer_sc = cell(1,Nscmax);
buffer_ca = cell(1,Ncamax);
for k=1:length(buffer_ca)
buffer_ca{k}=u0;
end
y=x0;
v=[];
tau = 0.3;
SIM_STEPS=100;
isError = 0;
for t=1:SIM_STEPS/tau
% Chech end point (When TS is reached !)
if(y(end,1) >= 2.4 && y(end,2) >= 1.5)
break;
end
% NCS filling SC channel:
buffer_sc(end) = [];
buffer_sc = [y(end,:) buffer_sc];
% are we ready to construct the xBig ?
if(isempty(buffer_sc{end}))
u = u0;
else
qValues = [0 0 0];
xValues = [ buffer_sc{1}(1) buffer_sc{1}(2) ...
buffer_sc{2}(1) buffer_sc{2}(2) ...
buffer_sc{3}(1) buffer_sc{3}(2) ...
buffer_ca{1}(1)...
buffer_ca{2}(1)...
buffer_ca{3}(1)];
try
u=contr.getInputs(qValues, xValues);
if(isempty(u))
isError = 1;
break;
end
catch mexp
isError = 1;
break;
end
end
% selecting one u from the offered inputs
u_selected = u(ceil(rand*length(u)));
u_at_sys = buffer_ca{end};
% NCS: filling ca channel
buffer_ca(end) = [];
buffer_ca = [u_selected buffer_ca];
%simulate and update
[t x]=ode45(@dint_ode,[0 tau], y(end,:), odeset('abstol',1e-4,'reltol',1e-4),u_at_sys);
y=[y; x(end,:)];
end
% initial state and trajectory:
plot(y(:,1),y(:,2),'.-','color',colors(1,:))
plot(y(1,1),y(1,2),'.','color',colors(5,:),'markersize',20)
hold on
if(isError==1)
plot(y(end-1,1),y(end-1,2),'o','color','r')
plot(y(end,1),y(end,2),'o','color','g')
end
end
end
function dxdt = dint_ode(t,x,u)
B = [0; 1];
A = [0 1; 0 0];
dxdt= A*x+B*u;
end
#
# compiler
#
#CC = g++
CC = clang++
CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
# cudd
#
CUDDPATH = /opt/local
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = dint
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
/*
* dcdc.cc
*
* created on: 31.08.2015
* author: m.khaled
*/
#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 1
/* data types for the ode solver */
typedef std::array<double,2> state_type;
typedef std::array<double,1> input_type;
/* sampling time */
const double tau = 0.30;
/* number of intermediate steps in the ode solver */
const int nint=5;
OdeSolver ode_solver(sDIM,nint,tau);
auto dint_post = [](state_type &x, input_type &u) -> void {
auto system_ode = [](state_type &dxdt, const state_type &x, const input_type &u) -> void {
const double b[2] = {0, 1};
const double a[2][2] = {{0, 1},
{0, 0}};
dxdt[0] = a[0][0]*x[0]+a[0][1]*x[1] + b[0]*u[0];
dxdt[1] = a[1][0]*x[0]+a[1][1]*x[1] + b[1]*u[0];
};
ode_solver(system_ode,x,u);
};
auto radius_post = [](state_type &r, input_type &u) -> void {
/*
auto growth_bound_ode = [](state_type &drdt, const state_type &r, const input_type &u) {
const double a[2][2] = {{0, 1},
{0, 0}};
drdt[0] = a[0][0]*r[0]+a[0][1]*r[1];
drdt[1] = a[1][0]*r[0]+a[1][1]*r[1];
};
ode_solver(growth_bound_ode,r,u);
*/
r[0]=0;
r[1]=0;
};
int main() {
TicToc tt;
Cudd mgr;
/****************************************************************************/
/* construct SymbolicSet for the state space */
/****************************************************************************/
double xlb[sDIM] ={0.60,0.30};
double xub[sDIM] ={3.40,3.30};
double xeta[sDIM] ={0.20,0.30};
scots::SymbolicSet ss(mgr,sDIM,xlb,xub,xeta);
ss.addGridPoints();
ss.writeToFile("dint_ss.bdd");
/****************************************************************************/
/* construct SymbolicSet for the input space */
/****************************************************************************/
double ulb[iDIM] ={0.00};
double uub[iDIM] ={1.00};
double ueta[iDIM] ={0.3};
scots::SymbolicSet is(mgr,iDIM,ulb,uub,ueta);
is.addGridPoints();
is.writeToFile("dint_is.bdd");
/****************************************************************************/
/* setup class for symbolic model computation */
/****************************************************************************/
scots::SymbolicSet sspost(ss,1);
scots::SymbolicModelGrowthBound<state_type,input_type> abstraction(&ss, &is, &sspost);
tt.tic();
abstraction.computeTransitionRelation(dint_post, radius_post);
std::cout << std::endl;
tt.toc();
std::cout << std::endl << "Number of elements in the transition relation: " << abstraction.getSize() << std::endl;
abstraction.getTransitionRelation().writeToFile("dint_rel.bdd");
/****************************************************************************/
/* we continue with the specification:: target set to reach */
/****************************************************************************/
double H[4*sDIM]={-1, 0,
1, 0,
0,-1,
0, 1};
double h[4] = {-2.4,3.4,-1.5, 3.3};
// double h[4] = {-2.85,3.3,-2.5, 3.1};
scots::SymbolicSet ts(ss);
ts.addPolytope(4,H,h, scots::INNER);
ts.writeToFile("dint_ts.bdd");
/****************************************************************************/
/* we continue with the controller synthesis */
/****************************************************************************/
scots::FixedPoint fp(&abstraction);
/* the fixed point algorithm operates on the BDD directly */
BDD T = ts.getSymbolicSet();
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 cont(ss,is);
cont.setSymbolicSet(C);
cont.writeToFile("dint_cont.bdd");
std::cout << "Controller size: " << cont.getSize() << std::endl;
return 1;
}
#
# 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 = pip_ncs
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
/*
* pip_ncs.cc
*
* created on: 31.08.2015
* 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 1
/* NCS Delay bounds */
#define NSCMAX 3
#define NCAMAX 2
#define FILE_BDD_REL "scots-files/pip_rel.bdd"
#define FILE_BDD_TS "scots-files/pip_ts.bdd"
#define FILE_NBDD_REL "pip_rel.nbdd"
int main() {
Cudd cuddManager;
cuddManager.AutodynEnable();
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;
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;
}
#
# compiler
#
#CC = g++
CC = clang++
CXXFLAGS = -Wall -Wextra -std=c++11 -O3 -DNDEBUG
#
# scots
#
SCOTSROOT = ../../../../../scots
SCOTSINC = -I$(SCOTSROOT)/bdd -I$(SCOTSROOT)/utils
#
# cudd
#
CUDDPATH = /opt/local
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = pip
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