sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Further step towards finalizing the abstraction layer for DDs. 

Former-commit-id: efd5822b67
tempestpy_adaptions
dehnert 11 years ago
parent
70fc3ec29a
commit
97e4e01250
6 changed files with 163 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 144
      src/storage/dd/CuddDd.cpp
  2. 20
      src/storage/dd/CuddDd.h
  3. 8
      src/storage/dd/CuddDdManager.cpp
  4. 1
      src/storage/dd/CuddDdManager.h
  5. 1
      src/storage/dd/DdMetaVariable.cpp
  6. 5
      src/storage/dd/DdMetaVariable.h

144
src/storage/dd/CuddDd.cpp
View File

@ -1,8 +1,9 @@
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {
Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
Dd<CUDD>::Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::unordered_set<std::string> const& containedMetaVariableNames) noexcept : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
// Intentionally left empty.
}
@ -13,10 +14,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) {
cuddAdd += other;
cuddAdd += other.getCuddAdd();
// Join the variable sets of the two participating DDs.
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@ -28,10 +29,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) {
cuddAdd *= other;
cuddAdd *= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@ -43,10 +44,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) {
cuddAdd -= other;
cuddAdd -= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@ -58,10 +59,10 @@ namespace storm {
}
Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) {
cuddAdd.Divide(other);
cuddAdd.Divide(other.getCuddAdd());
// Join the variable sets of the two participating DDs.
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().containedMetaVariableNames.end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
std::copy(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end(), std::inserter(this->containedMetaVariableNames, this->containedMetaVariableNames.end()));
return *this;
}
@ -77,12 +78,137 @@ namespace storm {
return *this;
}
Dd<CUDD> Dd<CUDD>::equals(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().Equals(other.getCuddAdd());
return result;
}
Dd<CUDD> Dd<CUDD>::notEquals(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().NotEquals(other.getCuddAdd());
return result;
}
Dd<CUDD> Dd<CUDD>::less(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().LessThan(other.getCuddAdd());
return result;
}
Dd<CUDD> Dd<CUDD>::lessOrEqual(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().LessThanOrEqual(other.getCuddAdd());
return result;
}
Dd<CUDD> Dd<CUDD>::greater(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().GreaterThan(other.getCuddAdd());
return result;
}
Dd<CUDD> Dd<CUDD>::greaterOrEqual(Dd<CUDD> const& other) const {
Dd<CUDD> result(*this);
result.getCuddAdd().GreaterThanOrEqual(other.getCuddAdd());
return result;
}
void Dd<CUDD>::existsAbstract(std::unordered_set<std::string> const& metaVariableNames) {
Dd<CUDD> cubeDd(this->getDdManager()->getOne());
for (auto const& metaVariableName : metaVariableNames) {
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd());
}
void Dd<CUDD>::sumAbstract(std::unordered_set<std::string> const& metaVariableNames) {
Dd<CUDD> cubeDd(this->getDdManager()->getOne());
for (auto const& metaVariableName : metaVariableNames) {
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd());
}
void Dd<CUDD>::minAbstract(std::unordered_set<std::string> const& metaVariableNames) {
Dd<CUDD> cubeDd(this->getDdManager()->getOne());
for (auto const& metaVariableName : metaVariableNames) {
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->getCuddAdd().Minimum(cubeDd.getCuddAdd());
}
void Dd<CUDD>::maxAbstract(std::unordered_set<std::string> const& metaVariableNames) {
Dd<CUDD> cubeDd(this->getDdManager()->getOne());
for (auto const& metaVariableName : metaVariableNames) {
DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
cubeDd *= metaVariable.getCube();
}
this->getCuddAdd().Maximum(cubeDd.getCuddAdd());
}
void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {
std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
metaVariableNameToValueMap.emplace(metaVariableName, variableValue);
this->setValue(metaVariableNameToValueMap, targetValue);
}
void Dd<CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) {
std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1);
metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2);
this->setValue(metaVariableNameToValueMap, targetValue);
}
void Dd<CUDD>::setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
// TODO: Fill this
}
bool Dd<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
return metaVariable != containedMetaVariableNames.end();
}
bool Dd<CUDD>::containsMetaVariables(std::unordered_set<std::string> metaVariableNames) const {
for (auto const& metaVariableName : metaVariableNames) {
auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
if (metaVariable == containedMetaVariableNames.end()) {
return false;
}
}
return true;
}
std::unordered_set<std::string> const& Dd<CUDD>::getContainedMetaVariableNames() const {
return containedMetaVariableNames;
}
void Dd<CUDD>::exportToDot(std::string const& filename) const {
FILE* filePointer = fopen(filename.c_str() , "w");
this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer);
fclose(filePointer);
}
ADD Dd<CUDD>::getCuddAdd() {
return this->cuddAdd;
}
ADD const& Dd<CUDD>::getCuddAdd() const {
return this->cuddAdd;
}
std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const {
return this->ddManager;
}

20
src/storage/dd/CuddDd.h
View File

@ -1,14 +1,18 @@
#ifndef STORM_STORAGE_DD_CUDDDD_H_
#define STORM_STORAGE_DD_CUDDDD_H_
#include <unordered_set>
#include <unordered_map>
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/CuddDdManager.h"
// Include the C++-interface of CUDD.
#include "cuddObj.hh"
namespace storm {
namespace dd {
// Forward-declare the DdManager class.
template<DdType Type> class DdManager;
template<>
class Dd<CUDD> {
@ -264,6 +268,20 @@ namespace storm {
std::shared_ptr<DdManager<CUDD>> getDdManager() const;
private:
/*!
* Retrieves the CUDD ADD object associated with this DD.
*
* @return The CUDD ADD object assoicated with this DD.
*/
ADD getCuddAdd();
/*!
* Retrieves the CUDD ADD object associated with this DD.
*
* @return The CUDD ADD object assoicated with this DD.
*/
ADD const& getCuddAdd() const;
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*

8
src/storage/dd/CuddDdManager.cpp
View File

@ -24,10 +24,10 @@ namespace storm {
std::vector<Dd<CUDD>> variables;
for (std::size_t i = 0; i < numberOfBits; ++i) {
variables.emplace_back(cuddManager.addVar());
variables.emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
}
metaVariableMap.emplace(name, low, high, variables, this->shared_from_this());
metaVariableMap.emplace(name, DdMetaVariable<CUDD>(name, low, high, variables, this->shared_from_this()));
}
void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
@ -40,13 +40,13 @@ namespace storm {
std::vector<std::vector<Dd<CUDD>>> variables;
for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
for (uint_fast64_t i = 0; i < names.size(); ++i) {
variables[i].emplace_back(cuddManager.addVar());
variables[i].emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
}
}
// Now add the meta variables.
for (uint_fast64_t i = 0; i < names.size(); ++i) {
metaVariableMap.emplace(names[i], low, high, variables[i], this->shared_from_this());
metaVariableMap.emplace(names[i], DdMetaVariable<CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
}
}

1
src/storage/dd/CuddDdManager.h
View File

@ -16,7 +16,6 @@ namespace storm {
template<>
class DdManager<CUDD> : std::enable_shared_from_this<DdManager<CUDD>> {
// To break the cylic dependencies, we need to forward-declare the other DD-related classes.
friend class DdMetaVariable<CUDD>;
friend class Dd<CUDD>;
/*!

1
src/storage/dd/DdMetaVariable.cpp
View File

@ -1,4 +1,5 @@
#include "src/storage/dd/DdMetaVariable.h"
#include "src/storage/dd/CuddDdManager.h"
namespace storm {
namespace dd {

5
src/storage/dd/DdMetaVariable.h
View File

@ -6,16 +6,19 @@
#include <cstdint>
#include <string>
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddDd.h"
namespace storm {
namespace dd {
// Forward-declare the DdManager class.
template<DdType Type> class DdManager;
template <DdType Type>
class DdMetaVariable {
public:
// Declare the DdManager class as friend so it can access the internals of a meta variable.
friend class DdManager<Type>;
friend class Dd<Type>;
/*!
* Creates a meta variable with the given name, range bounds.

Write Preview
Loading…
Cancel
Save