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

Commit ccef7247 authored by Matthias Rungger's avatar Matthias Rungger
Browse files

Adapt Makefiles to cudd-3.0.0

parent 85ddb103
......@@ -14,11 +14,10 @@ SCOTSINC = -I$(SCOTSROOT)/src
#
# cudd
#
CUDDPATH = ../../../../code/ext/cudd-2.5.1
CUDDPATH = /opt/local
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd -lobj -ldddmp -lmtr -lepd -lst -lutil
CUDDLPATH = -L$(CUDDPATH)/cudd -L$(CUDDPATH)/util -L$(CUDDPATH)/mtr -L$(CUDDPATH)/st -L$(CUDDPATH)/dddmp -L$(CUDDPATH)/epd -L$(CUDDPATH)/obj
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = dcdc
......
......@@ -52,7 +52,7 @@ DCDC_name='DCDC';
% For the chosen values of tau, eta, and mu we have an approximate
% bisimulation. Hence we set Relation to 1.
Relation=2;
Relation=1;
% The BatchSize flag controls the size of the computation batches.
% Transitions are generated and added to the symbolic model in batches of
......
......@@ -14,11 +14,10 @@ SCOTSINC = -I$(SCOTSROOT)/src
#
# cudd
#
CUDDPATH = ../../../../code/ext/cudd-2.5.1
CUDDPATH = /opt/local/
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd -lobj -ldddmp -lmtr -lepd -lst -lutil
CUDDLPATH = -L$(CUDDPATH)/cudd -L$(CUDDPATH)/util -L$(CUDDPATH)/mtr -L$(CUDDPATH)/st -L$(CUDDPATH)/dddmp -L$(CUDDPATH)/epd -L$(CUDDPATH)/obj
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = vehicle
......
......@@ -62,7 +62,8 @@ auto radius_post = [](state_type &r, input_type &u) -> void {
* input space and obstacles of the vehicle example */
scots::SymbolicSet vehicleCreateStateSpace(Cudd &mgr);
scots::SymbolicSet vehicleCreateInputSpace(Cudd &mgr);
void vehicleCreateObstacles(Cudd &mgr, scots::SymbolicSet &obs);
void vehicleCreateObstacles(scots::SymbolicSet &obs);
int main() {
......@@ -83,7 +84,7 @@ int main() {
/* first make a copy of the state space so that we obtain the grid
* information in the new symbolic set */
scots::SymbolicSet obs(ss);
vehicleCreateObstacles(mgr,obs);
vehicleCreateObstacles(obs);
obs.writeToFile("vehicle_obst.bdd");
/****************************************************************************/
......@@ -165,7 +166,7 @@ scots::SymbolicSet vehicleCreateStateSpace(Cudd &mgr) {
return ss;
}
void vehicleCreateObstacles(Cudd &mgr, scots::SymbolicSet &obs) {
void vehicleCreateObstacles(scots::SymbolicSet &obs) {
/* add the obstacles to the symbolic set */
/* the obstacles are defined as polytopes */
......
......@@ -14,11 +14,10 @@ SCOTSINC = -I$(SCOTSROOT)/src
#
# cudd
#
CUDDPATH = ../../../../code/ext/cudd-2.5.1
CUDDPATH = /opt/local/
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd -lobj -ldddmp -lmtr -lepd -lst -lutil
CUDDLPATH = -L$(CUDDPATH)/cudd -L$(CUDDPATH)/util -L$(CUDDPATH)/mtr -L$(CUDDPATH)/st -L$(CUDDPATH)/dddmp -L$(CUDDPATH)/epd -L$(CUDDPATH)/obj
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = vehicle
......
......@@ -19,10 +19,10 @@ SCOTSINC = -I$(SCOTSROOT)/src
#
# cudd
#
CUDDPATH = ../../../code/ext/cudd-2.5.1
CUDDPATH = /opt/local/
CUDDINC = -I$(CUDDPATH)/include
CUDDLIBS = -lcudd -lobj -ldddmp -lmtr -lepd -lst -lutil
CUDDLPATH = -L$(CUDDPATH)/cudd -L$(CUDDPATH)/util -L$(CUDDPATH)/mtr -L$(CUDDPATH)/st -L$(CUDDPATH)/dddmp -L$(CUDDPATH)/epd -L$(CUDDPATH)/obj
CUDDLIBS = -lcudd
CUDDLPATH = -L$(CUDDPATH)/lib
TARGET = mexSymbolicSetReadFromFile
......
......@@ -13,12 +13,11 @@ Requirements
- The CUDD library by Fabio Somenzi, which can be downlaod at
'http://vlsi.colorado.edu/~fabio/'.
- SCOTS uses the C++ wraper of the CUDD library, which you need to compile seperately.
Got to $(CUDDROOT)/obj/ and run
SCOTS uses the dddmp and C++ wraper of the CUDD library.
$ make
We successfully use cudd-3.0.0 which we configured with
$./configure --enable-shared --enable-obj --enable-dddmp --prefix=/opt/local/
SCOTS is a header only library. You only need to add SCOTS src directory to
the include directory in the compiler command.
......@@ -41,4 +40,4 @@ Directory structure
A mex-file to read the C++ output from file
- ./doc/
Documentation directory
Class documentation directory
......@@ -401,7 +401,7 @@ private:
delete[] y;
delete[] v;
return std::sqrt(max.getNode()->type.value);
return std::sqrt(Cudd_V(max.getNode()));
}
public:
/* constructor: SymbolicSet
......
Markdown is supported
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