Commit c41516bc authored by ga83nob's avatar ga83nob
Browse files

new modificatons

parent 9c703d8b
find ./ -type f -name "*.bdd" -delete
find ./ -type f -name "*.nbdd" -delete
cd examples/FIFO
for dir in *
do
cd ${dir}
make clean
cd scots-files
make clean
cd ..
cd ..
done
No preview for this file type
#
# 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 = dcdc_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 2
#define NCAMAX 2
#define FILE_BDD_REL "scots-files/sys_rel.bdd"
#define FILE_BDD_TS "scots-files/sys_ts.bdd"
#define FILE_NBDD_REL "dcdc_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;
}
#
# 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 = dcdc
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: 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 2
#define iDIM 1
/* data types for the ode solver */
typedef std::array<double,sDIM> state_type;
typedef std::array<double,sDIM> input_type;
/* sampling time */
const double tau = 0.5;
/* number of intermediate steps in the ode solver */
const int nint=5;
OdeSolver ode_solver(sDIM,nint,tau);
/* we integrate the dcdc ode by 0.3 sec (the result is stored in x) */
auto dcdc_post = [](state_type &x, input_type &u) -> void {
/* the ode describing the system */
auto system_ode = [](state_type &dxdt, const state_type &x, const input_type &u) -> void {
const double r0=1.0 ;
const double vs = 1.0 ;
const double rl = 0.05 ;
const double rc = rl / 10 ;
const double xl = 3.0 ;
const double xc = 70.0 ;
const double b[2]={vs/xl, 0};
double a[2][2];
if(u[0]==1) {
a[0][0] = -rl / xl;
a[0][1] = 0;
a[1][0] = 0;
a[1][1] = (-1 / xc) * (1 / (r0 + rc));
} else {
a[0][0] = (-1 / xl) * (rl + ((r0 * rc) / (r0 + rc))) ;
a[0][1] = ((-1 / xl) * (r0 / (r0 + rc))) / 5 ;
a[1][0] = 5 * (r0 / (r0 + rc)) * (1 / xc);
a[1][1] =(-1 / xc) * (1 / (r0 + rc)) ;
}
dxdt[0] = a[0][0]*x[0]+a[0][1]*x[1] + b[0];
dxdt[1] = a[1][0]*x[0]+a[1][1]*x[1] + b[1];
};
ode_solver(system_ode,x,u);
};
/* computation of the growth bound (the result is stored in r) */
auto radius_post = [](state_type &r, input_type &u) -> void {
/* the ode to determine the radius of the cell which over-approximates the
* attainable set see: http://arxiv.org/abs/1503.03715v1 */
auto growth_bound_ode = [](state_type &drdt, const state_type &r, const input_type &u) {
/* for the dcdc boost converter the growth bound is simply given by the metzler matrix of the system matrices */
const double r0=1.0 ;
const double rl = 0.05 ;
const double rc = rl / 10 ;
const double xl = 3.0 ;
const double xc = 70.0 ;
double a[2][2];
if(u[0]==1) {
a[0][0] = -rl / xl;
a[0][1] = 0;
a[1][0] = 0;
a[1][1] = (-1 / xc) * (1 / (r0 + rc));
} else {
a[0][0] = (-1 / xl) * (rl + ((r0 * rc) / (r0 + rc))) ;
a[0][1] = ((1 / xl) * (r0 / (r0 + rc))) / 5 ;
a[1][0] = 5 * (r0 / (r0 + rc)) * (1 / xc);
a[1][1] =(-1 / xc) * (1 / (r0 + rc)) ;
}
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);
};
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 */
/****************************************************************************/
std::cout << "Constructing state-space ... " << std::endl;
/* setup the workspace of the synthesis problem and the uniform grid */
/* lower bounds of the hyper rectangle */
double lb[sDIM]={1.15,5.45};
/* upper bounds of the hyper rectangle */
double ub[sDIM]={1.55,5.85};
/* grid node distance diameter */
double eta[sDIM]={2/4e3,2/4e3};
scots::SymbolicSet ss(mgr,sDIM,lb,ub,eta);
ss.addGridPoints();
ss.writeToFile("sys_ss.bdd");
/****************************************************************************/
/* construct SymbolicSet for the input space */
/****************************************************************************/
std::cout << "Constructing input-space ... " << std::endl;
double ilb[iDIM]={1};
double iub[iDIM]={2};
double ieta[iDIM]={1};
scots::SymbolicSet is(mgr,iDIM,ilb,iub,ieta);
is.addGridPoints();
is.writeToFile("sys_is.bdd");
/****************************************************************************/
/* 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 sss(ss,1);
/* instantiate the SymbolicModel */
scots::SymbolicModelGrowthBound<state_type,input_type> abstraction(&ss, &is, &sss);
/* compute the transition relation */
tt.tic();
abstraction.computeTransitionRelation(dcdc_post, radius_post);
std::cout << std::endl;
tt.toc();
/* get the number of elements in the transition relation */
std::cout << std::endl << "Number of elements in the transition relation: " << abstraction.getSize() << std::endl;
abstraction.getTransitionRelation().writeToFile("sys_rel.bdd");
return 1;
}
Constructing state-space ...
Symbolic set saved to file: sys_ss.bdd
Constructing input-space ...
Symbolic set saved to file: sys_is.bdd
0.........10.........20.........30.........40.........50.........60.........70.........80.........90.........100
Elapsed time is 21.7152 seconds.
Number of elements in the transition relation: 3.79415e+06
Symbolic set saved to file: sys_rel.bdd
......@@ -29,12 +29,12 @@
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;
cuddManager.AutodynEnable();
cout << "Expanding transition relation ... " << endl;
ncsState13.ExpandBDD();
cout << "NCS relation expanded in " << ncsState13.getExpandTime() << " seconds !" << endl;
......
<?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.45751672">
<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.45751672" moduleId="org.eclipse.cdt.core.settings" name="Build (GNU)">
<externalSettings/>
<extensions>
<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.MachO64" 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.PE" 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.GNU_ELF" point="org.eclipse.cdt.core.BinaryParser"/>
</extensions>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<configuration buildProperties="" id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.45751672" name="Build (GNU)" parent="org.eclipse.cdt.build.core.emptycfg">
<folderInfo id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.45751672.23862683" name="/" resourcePath="">
<toolChain id="org.eclipse.linuxtools.cdt.autotools.core.toolChain.242190266" name="GNU Autotools Toolchain" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolChain">
<targetPlatform id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.targetPlatform.642358463" 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.1298239037" managedBuildOn="false" name="null.Build (GNU)" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.builder"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.gnu.toolchain.tool.configure.53480874" name="configure" superClass="org.eclipse.linuxtools.cdt.autotools.core.gnu.toolchain.tool.configure"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.autogen.558008984" name="autogen.sh" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.autogen"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gcc.152367917" name="GCC C Compiler" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gcc"/>
<tool id="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gpp.139559246" name="GCC C++ Compiler" superClass="org.eclipse.linuxtools.cdt.autotools.core.toolchain.tool.gpp"/>
</toolChain>
</folderInfo>
</configuration>
</storageModule>
<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/>
</cconfiguration>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<project id="inver.null.695409282" name="inver"/>
</storageModule>
<storageModule moduleId="scannerConfiguration">
<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
</storageModule>
<storageModule moduleId="org.eclipse.cdt.core.LanguageSettingsProviders"/>
</cproject>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>inver</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.45751672" 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+)?((gcc)|([gc]\+\+)|(clang))" prefer-non-shared="true"/>
<provider-reference id="org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector" ref="shared-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 = inver_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
* dint_ncs.cc
*
* created on: 31.08.2015
* author: M.Khaled
......@@ -14,26 +14,24 @@
#include "SENSE.hh"
/* state-space / input-space dimensions */
#define ssDIM 2
#define ssDIM 3
#define isDIM 1
/* NCS Delay bounds */
#define NSCMAX 3
#define NSCMAX 2
#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;
cuddManager.AutodynEnable();
cout << "Expanding transition relation ... " << endl;
ncsState13.ExpandBDD();
cout << "NCS relation expanded in " << ncsState13.getExpandTime() << " seconds !" << endl;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment