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

towards labeling generation in dd to sparse conversion

main
dehnert 7 years ago
parent
733bec60bd
commit
cedae194e3
7 changed files with 83 additions and 32 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. 7
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  2. 31
      src/storm/storage/dd/Add.cpp
  3. 2
      src/storm/storage/dd/Add.h
  4. 29
      src/storm/storage/dd/cudd/InternalCuddAdd.cpp
  5. 6
      src/storm/storage/dd/cudd/InternalCuddAdd.h
  6. 34
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  7. 6
      src/storm/storage/dd/sylvan/InternalSylvanAdd.h

7
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -476,9 +476,12 @@ namespace storm {
} else {
STORM_LOG_TRACE("Using hybrid solving.");
storm::dd::Odd odd = (maybeMin || maybeMax || targetStates).createOdd();
auto relevantStates = maybeMin || maybeMax || targetStates;
auto relevantStatesAdd = relevantStates.template toAdd<ValueType>();
storm::dd::Odd odd = relevantStates.createOdd();
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, true);
auto relevantStatesTransitionMatrix = game.getTransitionMatrix() * relevantStatesAdd * relevantStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs());
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixLabeling = relevantStatesTransitionMatrix.toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true);
auto const& transitionMatrix = transitionMatrixLabeling.first;
auto const& labeling = transitionMatrixLabeling.second;

31
src/storm/storage/dd/Add.cpp
View File

@ -9,6 +9,7 @@
#include "storm/storage/dd/Odd.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
@ -703,14 +704,15 @@ namespace storm {
}
// Create the canonical row group sizes and build the matrix.
return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).first;
return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, groupMetaVariables, rowOdd, columnOdd).first;
}
template<DdType LibraryType, typename ValueType>
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> Add<LibraryType, ValueType>::toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> Add<LibraryType, ValueType>::toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, std::set<storm::expressions::Variable> const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const {
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
storm::storage::BitVector ddLabelVariableIndices;
std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
for (auto const& variable : rowMetaVariables) {
@ -736,7 +738,25 @@ namespace storm {
}
}
std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
if (buildLabeling) {
std::set<uint64_t> ddLabelVariableIndicesSet;
for (auto const& variable : labelMetaVariables) {
DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager().getMetaVariable(variable);
for (auto const& ddVariable : metaVariable.getDdVariables()) {
ddLabelVariableIndicesSet.insert(ddVariable.getIndex());
}
}
ddLabelVariableIndices = storm::storage::BitVector(ddGroupVariableIndices.size());
uint64_t position = 0;
for (auto const& index : ddGroupVariableIndices) {
if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) {
ddLabelVariableIndices.set(position);
}
++position;
}
}
Bdd<LibraryType> columnVariableCube = Bdd<LibraryType>::getCube(this->getDdManager(), columnMetaVariables);
// Start by computing the offsets (in terms of rows) for each row group.
@ -763,7 +783,7 @@ namespace storm {
// Create the group labelings if requested.
std::vector<uint64_t> groupLabels;
if (buildLabeling) {
groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices);
groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices);
STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes.");
}
@ -794,7 +814,8 @@ namespace storm {
if (buildLabeling) {
uint64_t currentLabel = groupLabels[i];
statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; });
std::cout << "current label is " << currentLabel << std::endl;
// statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; });
}
}

2
src/storm/storage/dd/Add.h
View File

@ -655,7 +655,7 @@ namespace storm {
* @return The matrix that is represented by this ADD and a vector corresponding to row labeling
* (if requested).
*/
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const;
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, std::set<storm::expressions::Variable> const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const;
/*!
* Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.

29
src/storm/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -6,6 +6,7 @@
#include "storm/storage/dd/Odd.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
@ -525,14 +526,15 @@ namespace storm {
}
template<typename ValueType>
std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const {
std::vector<uint64_t> result;
decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0);
std::cout << ddLabelVariableIndices << std::endl;
decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0);
return result;
}
template<typename ValueType>
void InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
void InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
// For the empty DD, we do not need to create a group.
if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
return;
@ -540,12 +542,23 @@ namespace storm {
if (currentLevel == maxLevel) {
labels.push_back(label);
} else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1);
} else {
decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 );
uint64_t elseLabel = label;
uint64_t thenLabel = label;
std::cout << "currentLevel " << currentLevel << " is in labels? " << ddLabelVariableIndices.get(currentLevel) << std::endl;
if (ddLabelVariableIndices.get(currentLevel)) {
elseLabel <<= 1;
thenLabel = (thenLabel << 1) | 1;
}
if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
} else {
decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
}
}
}

6
src/storm/storage/dd/cudd/InternalCuddAdd.h
View File

@ -575,9 +575,10 @@ namespace storm {
* The labeling is then made by interpreting the group encodings as binary encodings.
*
* @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups.
* @param ddLabelVariableIndices The indices of variables that are considered as labels.
* @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables).
*/
std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const;
/*!
* Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of
@ -676,12 +677,13 @@ namespace storm {
* @param dd The DD to split.
* @param labels A vector that is to be filled with the labels of the individual groups.
* @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
* @param ddLabelVariableIndices A bit vector indicating which variables are considered label variables.
* @param currentLevel The currently considered level in the DD.
* @param maxLevel The number of levels that need to be considered.
* @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
* @param label The currently followed label.
*/
void decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
void decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
/*!
* Splits the given DDs into the groups using the given group variables.

34
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -5,6 +5,7 @@
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/macros.h"
#include "storm/utility/constants.h"
@ -922,14 +923,14 @@ namespace storm {
}
template<typename ValueType>
std::vector<uint64_t> InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
std::vector<uint64_t> InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const {
std::vector<uint64_t> result;
decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0);
decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0);
return result;
}
template<typename ValueType>
void InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
void InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
// For the empty DD, we do not need to create a group.
if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
return;
@ -937,17 +938,26 @@ namespace storm {
if (currentLevel == maxLevel) {
labels.push_back(label);
} else if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
MTBDD thenDdNode = mtbdd_gethigh(dd);
MTBDD elseDdNode = mtbdd_getlow(dd);
decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 );
uint64_t elseLabel = label;
uint64_t thenLabel = label;
if (ddLabelVariableIndices.get(currentLevel)) {
elseLabel <<= 1;
thenLabel = (thenLabel << 1) | 1;
}
if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
MTBDD thenDdNode = mtbdd_gethigh(dd);
MTBDD elseDdNode = mtbdd_getlow(dd);
decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
}
}
}

6
src/storm/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -566,9 +566,10 @@ namespace storm {
* The labeling is then made by interpreting the group encodings as binary encodings.
*
* @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups.
* @param ddLabelVariableIndices The indices of variables that are considered as labels.
* @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables).
*/
std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices) const;
/*!
* Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of
@ -666,12 +667,13 @@ namespace storm {
* @param dd The DD to split.
* @param labels A vector that is to be filled with the labels of the individual groups.
* @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
* @param ddLabelVariableIndices A bit vector indicating which variables are considered label variables.
* @param currentLevel The currently considered level in the DD.
* @param maxLevel The number of levels that need to be considered.
* @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
* @param label The currently followed label.
*/
void decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
void decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
/*!
* Splits the given matrix DD into the groups using the given group variables.

Write Preview
Loading…
Cancel
Save