Skip to content
GitLab
Commit 1b991b02 authored by Matthias Rungger's avatar Matthias Rungger
Browse files

Manual added and some source code re-organization.

parent 91c4bed8
Expand all Hide whitespace changes
Inline Side-by-side
src/CuddMintermIterator.hh → bdd/CuddMintermIterator.hh
View file @ 1b991b02
......@@ -13,6 +13,7 @@
#include <vector>
#include <cassert>
#include <bitset>
#include <stdexcept>
#include "cuddObj.hh"
/* class: CuddMintermIterator
......
src/FixedPoint.hh → bdd/FixedPoint.hh
View file @ 1b991b02
......@@ -9,6 +9,7 @@
#define FIXEDPOINT_HH_
#include <iostream>
#include <stdexcept>
#include "cuddObj.hh"
#include "SymbolicModel.hh"
......@@ -19,23 +20,32 @@ namespace scots {
* class: FixedPoint
*
*
* it provides minimal and maximal fixed point computations
* it provides some minimal and maximal fixed point computations to
* synthesize controllers for simple invarinace and reachability
* spezifications
*
*/
class FixedPoint {
protected:
/* var: ddmgr_ */
Cudd *ddmgr_;
/* var: symbolicModel_
*
* stores the transition relation */
SymbolicModel *symbolicModel_;
/* var: permute
*
* stores the permutation array used to swap pre with post variables */
int* permute_;
/* helper BDDs */
/* transition relation */
BDD R_;
/* transition relation with cubePost_ abstracted */
BDD RR_;
/* cubes with input and post variables; used in the existential abstraction */
BDD cubePost_;
BDD cubeInput_;
public:
/* function: FixedPoint
......@@ -65,22 +75,45 @@ public:
vars[i]=ddmgr_->bddVar(symbolicModel_->postVars_[i]);
cubePost_ = ddmgr_->bddComputeCube(vars,NULL,symbolicModel_->nssVars_);
delete[] vars;
/* copy the transition relation */
R_=symbolicModel_->transitionRelation_;
RR_=R_.ExistAbstract(cubePost_);
}
~FixedPoint() {
delete[] permute_;
}
/* function: maximalFixedPoint
/* function: pre
*
* computes the enforcable predecessor
*
* computation of the maximal fixed point mu Z.pre(Z) & safe
* pre(Z) = { (x,u) | exists x': (x,u,x') in transitionRelation
* and (x,u,x') in transitionRelation => x' in Z }
*
* pre(Z) = { x | exist u, forall x', (x,u,x') in transitionRelation => x' in Z }
*/
BDD pre(BDD Z) {
/* project onto state alphabet */
Z=Z.ExistAbstract(cubePost_*cubeInput_);
/* swap variables */
Z=Z.Permute(permute_);
/* find the (state, inputs) pairs with a post outside the safe set */
BDD nZ = !Z;
BDD F = R_.AndAbstract(nZ,cubePost_);
/* the remaining (state, input) pairs make up the pre */
BDD nF = !F;
BDD preZ= RR_.AndAbstract(nF,cubePost_);
return preZ;
}
/* function: safe
*
* computation of the maximal fixed point mu Z.pre(Z) & S
*
*/
void maximalFixedPoint(BDD safe, BDD &FP, BDD &controller, int verbose=0) {
BDD safe(BDD S, int verbose=0) {
/* check if safe is a subset of the state space */
std::vector<unsigned int> sup = safe.SupportIndices();
std::vector<unsigned int> sup = S.SupportIndices();
for(size_t i=0; i<sup.size();i++) {
int marker=0;
for(size_t j=0; j<symbolicModel_->nssVars_; j++) {
......@@ -89,56 +122,42 @@ public:
}
if(!marker) {
std::ostringstream os;
os << "Error: maximalFixedPoint: the inital set depends on variables outside of the state space.";
os << "Error: safe: the inital set depends on variables outside of the state space.";
throw std::invalid_argument(os.str().c_str());
}
}
size_t k=0;
if(verbose)
std::cout << "Iterations: ";
/* copy the transition relation */
BDD R=symbolicModel_->transitionRelation_;
BDD RR=R.AndAbstract(safe,cubePost_);
BDD Znew=safe;
BDD Zold=ddmgr_->bddOne();
BDD preSI;
while(Znew<Zold) {
/* set new set as old */
Zold=Znew;
/* swap variables */
Znew=Znew.Permute(permute_);
/* find the (state, inputs) pairs with a post outside the safe set */
BDD Out = !Znew;
BDD F = R.AndAbstract(Out,cubePost_);
/* the remaining (state, input) pairs make up the pre */
BDD nF = !F;
preSI= RR.AndAbstract(nF,cubePost_);
/* now extract the states from the (state,input) pairs */
BDD preZ = preSI.ExistAbstract(cubeInput_);
Znew = Zold & preZ;
k++;
BDD Z = ddmgr_->bddZero();
BDD ZZ = ddmgr_->bddOne();
/* as long as not converged */
size_t i;
for(i=1; ZZ != Z; i++ ) {
Z=ZZ;
ZZ=FixedPoint::pre(Z) & S;
/* print progress */
if(verbose) {
std::cout << ".";
std::flush(std::cout);
if(!(i%80))
std::cout << std::endl;
}
}
if(verbose)
std::cout << " number: " << k << std::endl;
controller= preSI;
FP=Znew;
std::cout << " number: " << i << std::endl;
return Z;
}
/* function: minimalFixedPoint
/* function: reach
*
* computation of the minimal fixed point mu Z.pre(Z) | target
*
* pre(Z) = { x | exist u, forall x', (x,u,x') in transitionRelation => x' in Z }
* computation of the minimal fixed point mu Z.pre(Z) | T
*
*/
void minimalFixedPoint(BDD target, BDD &FP, BDD &controller, int verbose=0) {
BDD reach(const BDD &T, int verbose=0) {
/* check if target is a subset of the state space */
std::vector<unsigned int> sup = target.SupportIndices();
std::vector<unsigned int> sup = T.SupportIndices();
for(size_t i=0; i<sup.size();i++) {
int marker=0;
for(size_t j=0; j<symbolicModel_->nssVars_; j++) {
......@@ -146,59 +165,50 @@ public:
marker=1;
}
if(!marker) {
std::ostringstream os;
os << "Error: minimalFixedPoint: the inital set depends on variables outside of the state space.";
throw std::invalid_argument(os.str().c_str());
std::ostringstream os;
os << "Error: reach: the target set depends on variables outside of the state space.";
throw std::invalid_argument(os.str().c_str());
}
}
size_t k=0;
if(verbose)
std::cout << "Iterations: ";
/* copy the transition relation */
BDD R=symbolicModel_->transitionRelation_;
BDD RR=R.ExistAbstract(cubePost_);
BDD Znew=target;
BDD Zold=ddmgr_->bddZero();
controller=ddmgr_->bddZero();
while(Zold<Znew) {
/* set new set as old */
Zold=Znew;
/* swap variables */
Znew=Znew.Permute(permute_);
/* find the (state, inputs) pairs with a post outside the target set */
BDD Out = !Znew;
BDD F = R.AndAbstract(Out,cubePost_);
/* the remaining (state, input) pairs make up the pre */
BDD nF = !F;
BDD preSI = RR.AndAbstract(nF,cubePost_);
/* now extract the states from the (state,input) pairs */
BDD preZ = preSI.ExistAbstract(cubeInput_);
Znew = Zold | preZ;
/*find the new states added in this iteration*/
BDD newStates = preZ & (!Zold);
/* add new states with associated inputs to controller */
controller+= (newStates & preSI) ;
k++;
BDD Z = ddmgr_->bddOne();
BDD ZZ = ddmgr_->bddZero();
/* the controller */
BDD C = ddmgr_->bddZero();
/* as long as not converged */
size_t i;
for(i=1; ZZ != Z; i++ ) {
Z=ZZ;
ZZ=FixedPoint::pre(Z) | T;
/* new (state/input) pairs */
BDD N = ZZ & (!(C.ExistAbstract(cubeInput_)));
/* add new (state/input) pairs to the controller */
C=C | N;
/* print progress */
if(verbose) {
std::cout << ".";
std::flush(std::cout);
if(!(i%80))
std::cout << std::endl;
}
}
if(verbose)
std::cout << " number: " << k << std::endl;
FP=Znew;
std::cout << " number: " << i << std::endl;
return C;
}
/* function: reachAvoid
*
* controller synthesis to enforce reach avoid specification
*
* computation of the minimal fixed point mu Z.(pre(Z) | T) & !A
*
*/
void reachAvoid(BDD target, BDD avoid, BDD &FP, BDD &controller, int verbose=0) {
BDD reachAvoid(const BDD &T, const BDD &A, int verbose=0) {
/* check if target is a subset of the state space */
std::vector<unsigned int> sup = target.SupportIndices();
std::vector<unsigned int> sup = T.SupportIndices();
for(size_t i=0; i<sup.size();i++) {
int marker=0;
for(size_t j=0; j<symbolicModel_->nssVars_; j++) {
......@@ -211,89 +221,41 @@ public:
throw std::invalid_argument(os.str().c_str());
}
}
size_t k=0;
if(verbose)
std::cout << "Iterations: ";
/* system should stay in the negation of avoid */
BDD safe = !avoid;
/* copy the transition relation */
BDD R=symbolicModel_->transitionRelation_;
BDD RR=R.ExistAbstract(cubePost_)& safe;
BDD RR=RR_;
/* remove avoid (state/input) pairs from transition relation */
RR_= RR & (!A);
BDD TT= T & (!A);
BDD Znew=(target & safe);
BDD Zold=ddmgr_->bddZero();
controller=ddmgr_->bddZero();
while(Zold<Znew) {
/* set new set as old */
Zold=Znew;
/* swap variables */
Znew=Znew.Permute(permute_);
/* find the (state, inputs) pairs with a post outside the target set */
BDD Out = !Znew;
BDD F = R.AndAbstract(Out,cubePost_);
/* the remaining (state, input) pairs make up the pre */
BDD nF = !F;
BDD preSI = RR.AndAbstract(nF,cubePost_);
/* now extract the states from the (state,input) pairs */
BDD preZ = preSI.ExistAbstract(cubeInput_);
Znew = Zold | preZ;
/*find the new states added in this iteration*/
BDD newStates = preZ & (!Zold);
/* add new states with associated inputs to controller */
controller+= (newStates & preSI) ;
/* progress */
k++;
BDD Z = ddmgr_->bddOne();
BDD ZZ = ddmgr_->bddZero();
/* the controller */
BDD C = ddmgr_->bddZero();
/* as long as not converged */
size_t i;
for(i=1; ZZ != Z; i++ ) {
Z=ZZ;
ZZ=FixedPoint::pre(Z) | TT;
/* new (state/input) pairs */
BDD N = ZZ & (!(C.ExistAbstract(cubeInput_)));
/* add new (state/input) pairs to the controller */
C=C | N;
/* print progress */
if(verbose) {
std::cout << ".";
std::flush(std::cout);
std::cout << ".";
std::flush(std::cout);
if(!(i%80))
std::cout << std::endl;
}
}
if(verbose)
std::cout << " number: " << k << std::endl;
FP=Znew;
}
/* function: pre
*
* pre(Z) = { x | exist u, forall x', (x,u,x') in transitionRelation => x' in Z }
*
*/
BDD pre(BDD Z) {
/* check if safe is a subset of the state space */
std::vector<unsigned int> sup = Z.SupportIndices();
for(size_t i=0; i<sup.size();i++) {
int marker=0;
for(size_t j=0; j<symbolicModel_->nssVars_; j++) {
if (sup[i]==symbolicModel_->preVars_[j])
marker=1;
}
if(!marker) {
std::ostringstream os;
os << "Error: maximalFixedPoint: the inital set depends on variables outside of the state space.";
throw std::invalid_argument(os.str().c_str());
}
}
/* copy the transition relation */
BDD R=symbolicModel_->transitionRelation_;
BDD RR=R.ExistAbstract(cubePost_);
/* swap variables */
Z=Z.Permute(permute_);
/* find the (state, inputs) pairs with a post outside the safe set */
BDD Out = !Z;
BDD F = R.AndAbstract(Out,cubePost_);
/* the remaining (state, input) pairs make up the pre */
BDD nF = !F;
BDD preSI= RR.AndAbstract(nF,cubePost_);
/* now extract the states from the (state,input) pairs */
BDD preZ = preSI.ExistAbstract(cubeInput_);
return preZ;
std::cout << " number: " << i << std::endl;
/* restor transition relation */
RR_=RR;
return C;
}
}; /* close class def */
} /* close namespace */
......
src/SymbolicModel.hh → bdd/SymbolicModel.hh
View file @ 1b991b02
......@@ -9,6 +9,7 @@
#define SYMBOLICMODEL_HH_
#include <iostream>
#include <stdexcept>
#include "cuddObj.hh"
#include "dddmp.h"
......@@ -36,6 +37,8 @@ protected:
SymbolicSet *stateSpace_;
/* var: inputSpace_ */
SymbolicSet *inputSpace_;
/* var: stateSpacePost_ */
SymbolicSet *stateSpacePost_;
/* var: nssVars_
* number of state space bdd variables (= number of pre/post variables) */
size_t nssVars_;
......@@ -63,12 +66,57 @@ protected:
BDD transitionRelation_;
friend class FixedPoint;
public:
SymbolicModel(SymbolicSet *stateSpace, SymbolicSet *inputSpace): stateSpace_(stateSpace), inputSpace_(inputSpace) {
if(stateSpace_->ddmgr_!=inputSpace_->ddmgr_) {
/* constructor: SymbolicModel
*
* Representation of the transition relation as BDD in the space
*
* preX x U x postX
*
* provide SymbolicSet for preX
* provide SymbolicSet for U
* provide SymbolicSet for postX
*
* the SymbolicSet for preX and postX need to be identical, except the
* BDD variable IDs need to differ
*
*
*/
SymbolicModel(SymbolicSet *stateSpace,
SymbolicSet *inputSpace,
SymbolicSet *stateSpacePost):
stateSpace_(stateSpace), inputSpace_(inputSpace), stateSpacePost_(stateSpacePost) {
if(stateSpace_->ddmgr_!=inputSpace_->ddmgr_ || stateSpacePost_->ddmgr_!=inputSpace_->ddmgr_ ) {
std::ostringstream os;
os << "Error: scots::SymbolicModel: stateSpace and inputSpace need to have the same dd manager.";
throw std::invalid_argument(os.str().c_str());
}
/* check if stateSpace and stateSpacePost have the same domain and grid parameter */
int differ = 0;
if(stateSpace_->dim_!=stateSpacePost_->dim_)
differ=1;
for(size_t i=0; i<stateSpace_->dim_; i++) {
if(stateSpace_->firstGridPoint_[i]!= stateSpacePost_->firstGridPoint_[i])
differ=1;
if(stateSpace_->nofGridPoints_[i]!= stateSpacePost_->nofGridPoints_[i])
differ=1;
if(stateSpace_->eta_[i]!= stateSpacePost_->eta_[i])
differ=1;
}
if(differ) {
std::ostringstream os;
os << "Error: scots::SymbolicModel: stateSpace and stateSpacePost need have the same domain and grid parameter.";
throw std::invalid_argument(os.str().c_str());
}
/* check if stateSpace and stateSpacePost have different BDD IDs */
for(size_t i=0; i<stateSpace_->dim_; i++)
for(size_t j=0; j<stateSpace_->nofBddVars_[i]; j++)
if(stateSpace_->indBddVars_[i][j]==stateSpacePost_->indBddVars_[i][j])
differ=1;
if(differ) {
std::ostringstream os;
os << "Error: scots::SymbolicModel: stateSpace and stateSpacePost are not allowed to have the same BDD IDs.";
throw std::invalid_argument(os.str().c_str());
}
ddmgr_=stateSpace_->ddmgr_;
nssVars_=0;
for(size_t i=0; i<stateSpace_->dim_; i++)
......@@ -78,16 +126,14 @@ public:
for(size_t i=0; i<inputSpace_->dim_; i++)
for(size_t j=0; j<inputSpace_->nofBddVars_[i]; j++)
nisVars_++;
/* set the preVars_ to the variable indices of stateSpace_
* and get new indices for the postVars_ */
* set the postVars_ to the variable indices of stateSpacePost_ */
preVars_ = new size_t[nssVars_];
postVars_ = new size_t[nssVars_];
for(size_t k=0, i=0; i<stateSpace_->dim_; i++) {
for(size_t j=0; j<stateSpace_->nofBddVars_[i]; k++, j++) {
preVars_[k]=stateSpace_->indBddVars_[i][j];
BDD t=stateSpace_->ddmgr_->bddVar();
postVars_[k]=t.NodeReadIndex();
postVars_[k]=stateSpacePost_->indBddVars_[i][j];
}
}
inpVars_ = new size_t[nisVars_];
......@@ -112,11 +158,26 @@ public:
return transitionRelation_.CountMinterm(2*nssVars_+nisVars_);
};
/* function: getTransitionRelation
* get the BDD which represents the transition relation */
inline BDD getTransitionRelation(void) {
return transitionRelation_;
* get the SymbolicSet which represents transition relation in X x U x X */
inline SymbolicSet getTransitionRelation(void) const {
/* create SymbolicSet representing the post stateSpace_*/
/* make a cope of the SymbolicSet of the preSet */
SymbolicSet post(*stateSpace_);
/* set the BDD indices to the BDD indices used for the post stateSpace_ */
post.setIndBddVars(postVars_);
/* create SymbolicSet representing the stateSpace_ x inputSpace_ */
SymbolicSet sis(*stateSpace_,*inputSpace_);
/* create SymbolicSet representing the stateSpace_ x inputSpace_ x stateSpace_ */
SymbolicSet tr(sis,post);
/* fill SymbolicSet with transition relation */
tr.setSymbolicSet(transitionRelation_);
return tr;
};
/* iterator methods */
/* function: setTransitionRelation
* set the transitionRelation_ BDD to transitionRelation */
void setTransitionRelation(BDD transitionRelation) {
transitionRelation_=transitionRelation;
}; /* iterator methods */
/* function: begin
* initilize the iterator and compute the first element */
inline void begin(void) {
......@@ -157,112 +218,6 @@ public:
else
return NULL;
}
/* function: writeToFile
* stores the bdd of transition function as a <SymbolicSet> with all information to file*/
void writeToFile(const char *filename) {
/* produce string with parameters to be written into file */
std::stringstream dim;
std::stringstream z;
std::stringstream eta;
std::stringstream first;
std::stringstream last;
std::stringstream nofGridPoints;
std::stringstream indBddVars;
size_t dim_ = 2*stateSpace_->dim_+inputSpace_->dim_;
dim <<"#scots dimension: " << dim_ << std::endl;
z << "#scots measurement error bound: ";
eta << "#scots grid parameter eta: ";
first << "#scots coordinate of first grid point: ";
last << "#scots coordinate of last grid point: ";
nofGridPoints << "#scots number of grid points (per dim): ";
indBddVars << "#scots index of bdd variables: ";
/* write information of the pre state space */
for(size_t i=0; i<stateSpace_->dim_; i++) {
z << stateSpace_->z_[i] << " ";
eta << stateSpace_->eta_[i] << " ";
first << stateSpace_->firstGridPoint_[i] << " ";
last << stateSpace_->lastGridPoint_[i] << " ";
nofGridPoints << stateSpace_->nofGridPoints_[i] << " ";
}
for(size_t j=0; j<nssVars_; j++)
indBddVars << preVars_[j] << " ";
/* write information of the input space */
for(size_t i=0; i<inputSpace_->dim_; i++) {
z << inputSpace_->z_[i] << " ";
eta << inputSpace_->eta_[i] << " ";
first << inputSpace_->firstGridPoint_[i] << " ";
last << inputSpace_->lastGridPoint_[i] << " ";
nofGridPoints << inputSpace_->nofGridPoints_[i] << " ";
}
for(size_t j=0; j<nisVars_; j++)
indBddVars << inpVars_[j] << " ";
/* write information of the post state space */
for(size_t i=0; i<stateSpace_->dim_; i++) {
z << stateSpace_->z_[i] << " ";
eta << stateSpace_->eta_[i] << " ";
first << stateSpace_->firstGridPoint_[i] << " ";
last << stateSpace_->lastGridPoint_[i] << " ";
nofGridPoints << stateSpace_->nofGridPoints_[i] << " ";
}
for(size_t j=0; j<nssVars_; j++)
indBddVars << postVars_[j] << " ";
z << std::endl;
eta << std::endl;
first << std::endl;
last << std::endl;
nofGridPoints << std::endl;
indBddVars << std::endl;
std::stringstream paramss;
paramss << "################################################################################" << std::endl
<< "########### symbolic controller synthesis toolbox information added ############" << std::endl
<< "################################################################################" << std::endl
<< dim.str() \
<< eta.str() \
<< z.str() \
<< first.str() \
<< last.str() \
<< nofGridPoints.str() \
<< indBddVars.str();
std::string param=paramss.str();
FILE *file = fopen (filename,"w");
if (file == NULL){
std::ostringstream os;
os << "Error: Unable to open file for writing." << filename << "'.";
throw std::runtime_error(os.str().c_str());
}
if (param.size() != fwrite(param.c_str(),1,param.size(),file)) {
throw "Error: Unable to write set information to file.";
}
int storeReturnValue = Dddmp_cuddBddStore(
ddmgr_->getManager(),
NULL,
transitionRelation_.getNode(),
//(char**)varnameschar, // char ** varnames, IN: array of variable names (or NULL)
NULL, // char ** varnames, IN: array of variable names (or NULL)
NULL,
DDDMP_MODE_BINARY,
// DDDMP_VARNAMES,
DDDMP_VARIDS,
NULL,
file
);
fclose(file);
if (storeReturnValue!=DDDMP_SUCCESS)
throw "Error: Unable to write BDD to file.";