From 5d530bb532d965e57eb4913f1409c0ca28abfdc5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 26 Feb 2020 20:52:15 +0100 Subject: [PATCH] Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards) --- src/storm/api/transformation.h | 2 + src/storm/storage/dd/Add.cpp | 84 +++++++++++--- src/storm/storage/dd/Add.h | 20 +++- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 52 +++++++++ src/storm/storage/dd/cudd/InternalCuddAdd.h | 23 ++++ .../storage/dd/sylvan/InternalSylvanAdd.cpp | 58 ++++++++++ .../storage/dd/sylvan/InternalSylvanAdd.h | 25 ++++- .../SymbolicToSparseTransformer.cpp | 105 +++++++++++++++++- .../transformer/SymbolicToSparseTransformer.h | 8 ++ 9 files changed, 354 insertions(+), 23 deletions(-) diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 9aa99aa01..1ab8f696e 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -105,6 +105,8 @@ namespace storm { return storm::transformer::SymbolicMdpToSparseMdpTransformer::translate(*symbolicModel->template as>(), formulas); case storm::models::ModelType::Ctmc: return storm::transformer::SymbolicCtmcToSparseCtmcTransformer::translate(*symbolicModel->template as>(), formulas); + case storm::models::ModelType::MarkovAutomaton: + return storm::transformer::SymbolicMaToSparseMaTransformer::translate(*symbolicModel->template as>(), formulas); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not supported."); } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 5f1b05586..a9cfbafdf 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -533,7 +533,7 @@ namespace storm { } template - std::vector Add::toVector(storm::dd::Add const& matrix, std::vector const& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::vector Add::toVector(storm::dd::Add const& matrix, std::vector const& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -894,6 +894,38 @@ namespace storm { template std::pair, std::vector> Add::toMatrixVector(std::vector&& rowGroupIndices, storm::dd::Add const& vector, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + auto resultAsVector = toMatrixVectors(std::move(rowGroupIndices), {vector}, rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + return std::make_pair(resultAsVector.first, resultAsVector.second.front()); + } + + template + std::pair, std::vector>> Add::toMatrixVectors(std::vector> const& vectors, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + // Count how many choices each row group has. + Bdd vectorsNotZero = this->getDdManager().getBddZero(); + for (auto const& v : vectors) { + vectorsNotZero |= v.notZero(); + } + std::vector rowGroupIndices = (this->notZero().existsAbstract(columnMetaVariables) || vectorsNotZero).template toAdd().sumAbstract(groupMetaVariables).toVector(rowOdd); + return toMatrixVectors(std::move(rowGroupIndices), vectors, rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + template + std::pair, std::vector>> Add::toMatrixVectors(std::vector&& rowGroupIndices, std::vector> const& vectors, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -936,14 +968,36 @@ namespace storm { } rowGroupIndices[0] = 0; - // Create the explicit vector we need to fill later. - std::vector explicitVector(rowGroupIndices.back()); + // Create the explicit vectors we need to fill later. + std::vector> explicitVectors(vectors.size()); + for (auto& v : explicitVectors) { + v.resize(rowGroupIndices.back()); + } // Next, we split the matrix into one for each group. Note that this only works if the group variables are at the very top. - std::vector, InternalAdd>> internalAddGroups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices); - std::vector, Add>> groups; - for (auto const& internalAdd : internalAddGroups) { - groups.push_back(std::make_pair(Add(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables), Add(this->getDdManager(), internalAdd.second, rowMetaVariables))); + std::vector>> groups; + if (vectors.size() == 1) { + // This version potentially has slightly reduced overhead + std::vector, InternalAdd>> internalAddGroups = internalAdd.splitIntoGroups(vectors.front(), ddGroupVariableIndices); + for (auto const& internalAdd : internalAddGroups) { + groups.push_back({Add(this->getDdManager(), internalAdd.second, rowMetaVariables), Add(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables)}); + } + } else { + std::vector> internalVectors; + for (Add const& v : vectors) { + internalVectors.push_back(v.getInternalAdd()); + } + std::vector>> internalAddGroups = internalAdd.splitIntoGroups(internalVectors, ddGroupVariableIndices); + for (auto const& internalAddGroup : internalAddGroups) { + STORM_LOG_ASSERT(internalAddGroup.size() == vectors.size() + 1, "Unexpected group size."); + std::vector> group; + for (uint64_t vectorIndex = 0; vectorIndex < vectors.size(); ++vectorIndex) { + group.push_back(Add(this->getDdManager(), internalAddGroup[vectorIndex], rowMetaVariables)); + } + // The last group member corresponds to the matrix. + group.push_back(Add(this->getDdManager(), internalAddGroup.back(), rowAndColumnMetaVariables)); + groups.push_back(std::move(group)); + } } // Create the actual storage for the non-zero entries. @@ -955,16 +1009,19 @@ namespace storm { std::vector> statesWithGroupEnabled(groups.size()); InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { - std::pair, Add> const& ddPair = groups[i]; - Bdd matrixDdNotZero = ddPair.first.notZero(); - Bdd vectorDdNotZero = ddPair.second.notZero(); + std::vector> const& group = groups[i]; + Bdd matrixDdNotZero = group.back().notZero(); std::vector tmpRowIndications = matrixDdNotZero.template toAdd().sumAbstract(columnMetaVariables).toVector(rowOdd); for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) { rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset]; } - ddPair.second.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); + Bdd vectorDdNotZero = this->getDdManager().getBddZero(); + for (uint64_t vectorIndex = 0; vectorIndex < vectors.size(); ++vectorIndex) { + vectorDdNotZero |= group[vectorIndex].notZero(); + group[vectorIndex].internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVectors[vectorIndex], std::plus()); + } statesWithGroupEnabled[i] = (matrixDdNotZero.existsAbstract(columnMetaVariables) || vectorDdNotZero).template toAdd(); stateToRowGroupCount += statesWithGroupEnabled[i]; @@ -986,7 +1043,7 @@ namespace storm { // Now actually fill the entry vector. for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i].first; + auto const& dd = groups[i].back(); dd.internalAdd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); @@ -1001,9 +1058,10 @@ namespace storm { } rowIndications[0] = 0; - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector)); + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVectors)); } + template void Add::exportToDot(std::string const& filename, bool showVariablesIfPossible) const { diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 2d94b07fc..4ab7c2983 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -585,17 +585,16 @@ namespace storm { * variables used to distinguish different row groups are at the very top of the ADD. * * @param matrix The symbolic matrix whose row group sizes to respect. - * @param rowGroupSizes A vector specifying the sizes of the row groups. + * @param rowGroupIndices A vector specifying the sizes of the row groups. * @param rowMetaVariables The meta variables that encode the rows of the matrix. * @param columnMetaVariables The meta variables that encode the columns of the matrix. * @param groupMetaVariables The meta variables that are used to distinguish different row groups. * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector * (if it was given). * @return The vector that is represented by this ADD. */ - std::vector toVector(storm::dd::Add const& matrix, std::vector const& rowGroupSizes, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + std::vector toVector(storm::dd::Add const& matrix, std::vector const& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const; /*! * Converts the ADD to a (sparse) matrix. All contained non-primed variables are assumed to encode the @@ -686,6 +685,21 @@ namespace storm { */ std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; std::pair, std::vector> toMatrixVector(std::vector&& rowGroupSizes, storm::dd::Add const& vector, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a row-grouped (sparse) matrix and the given vectors to row-grouped vectors. + * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each + * entry. Note: this function assumes that the meta variables used to distinguish different row groups are + * at the very top of the ADD. + * + * @param vectors The symbolic vectors to convert. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + std::pair, std::vector>> toMatrixVectors(std::vector> const& vectors, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + std::pair, std::vector>> toMatrixVectors(std::vector&& rowGroupSizes, std::vector> const& vectors, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! * Exports the DD to the given file in the dot format. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 1c4e0cf35..98760a293 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -634,6 +634,58 @@ namespace storm { } } + template + std::vector>> InternalAdd::splitIntoGroups(std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const { + std::vector>> result; + std::vector dds; + for (auto const& vector : vectors) { + dds.push_back(vector.getCuddDdNode()); + } + dds.push_back(this->getCuddDdNode()); + + splitIntoGroupsRec(dds, result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + + template + void InternalAdd::splitIntoGroupsRec(std::vector const& dds, std::vector>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + { + bool emptyDd = true; + for (auto const& dd : dds) { + if (dd != Cudd_ReadZero(ddManager->getCuddManager().getManager())) { + emptyDd = false; + break; + } + } + if (emptyDd) { + return; + } + } + + if (currentLevel == maxLevel) { + std::vector> newGroup; + for (auto dd : dds) { + newGroup.emplace_back(ddManager, cudd::ADD(ddManager->getCuddManager(), dd)); + } + groups.push_back(std::move(newGroup)); + } else { + std::vector thenSubDds(dds), elseSubDds(dds); + for (uint64_t ddIndex = 0; ddIndex < dds.size(); ++ddIndex) { + auto const& dd = dds[ddIndex]; + if (ddGroupVariableIndices[currentLevel] == Cudd_NodeReadIndex(dd)) { + thenSubDds[ddIndex] = Cudd_T(dd); + elseSubDds[ddIndex] = Cudd_E(dd); + } + } + splitIntoGroupsRec(thenSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(elseSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + + + + template void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const { return toMatrixComponentsRec(this->getCuddDdNode(), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues); diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 21788a7a7..dd80cb18c 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -609,6 +609,17 @@ namespace storm { */ std::vector, InternalAdd>> splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const; + /*! + * Simultaneously splits the ADD and the given vector ADDs into several ADDs that differ in the encoding of + * the given group variables (given via indices). + * + * @param vectors The vectors to split (in addition to the current ADD). + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of vectors of ADDs such that result.size() is the number of groups and result[i] refers to all ADDs within the same group i (wrt. to the encoding of the given variables). + * result[i].back() always refers to this ADD. + */ + std::vector>> splitIntoGroups(std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const; + /*! * Translates the ADD into the components needed for constructing a matrix. * @@ -716,6 +727,18 @@ namespace storm { */ void splitIntoGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + /*! + * Splits the given DDs into the groups using the given group variables. + * + * @param dds The DDs to split. + * @param negatedDds indicates which of the DDs need to be interpreted as negated. + * @param groups A vector that is to be filled with the DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + */ + void splitIntoGroupsRec(std::vector const& dds, std::vector>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + /*! * Helper function to convert the DD into a (sparse) matrix. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 431ae5713..c8501a25f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -986,6 +986,22 @@ namespace storm { return result; } + template + std::vector>> InternalAdd::splitIntoGroups(std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const { + std::vector>> result; + std::vector dds; + storm::storage::BitVector negatedDds(vectors.size() + 1); + for (auto const& vector : vectors) { + negatedDds.set(dds.size(), mtbdd_hascomp(vector.getSylvanMtbdd().GetMTBDD())); + dds.push_back(mtbdd_regular(vector.getSylvanMtbdd().GetMTBDD())); + } + dds.push_back(this->getSylvanMtbdd().GetMTBDD()); + negatedDds.set(vectors.size(), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD())); + + splitIntoGroupsRec(dds, negatedDds, result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + template void InternalAdd::splitIntoGroupsRec(MTBDD dd, bool negated, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { // For the empty DD, we do not need to create a group. @@ -1063,6 +1079,48 @@ namespace storm { } } + template + void InternalAdd::splitIntoGroupsRec(std::vector const& dds, storm::storage::BitVector const& negatedDds, std::vector>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + { + bool emptyDd = true; + for (auto const& dd : dds) { + if (!(mtbdd_isleaf(dd) && mtbdd_iszero(dd))) { + emptyDd = false; + break; + } + } + if (emptyDd) { + return; + } + } + + if (currentLevel == maxLevel) { + std::vector> newGroup; + for (uint64_t ddIndex = 0; ddIndex < dds.size(); ++ddIndex) { + newGroup.emplace_back(ddManager, negatedDds.get(ddIndex) ? sylvan::Mtbdd(dds[ddIndex]).Negate() : sylvan::Mtbdd(dds[ddIndex])); + } + groups.push_back(std::move(newGroup)); + } else { + std::vector thenSubDds(dds), elseSubDds(dds); + storm::storage::BitVector thenNegatedSubDds(negatedDds), elseNegatedSubDds(negatedDds); + for (uint64_t ddIndex = 0; ddIndex < dds.size(); ++ddIndex) { + auto const& dd = dds[ddIndex]; + if (!mtbdd_isleaf(dd) && ddGroupVariableIndices[currentLevel] == mtbdd_getvar(dd)) { + MTBDD ddThenNode = mtbdd_gethigh(dd); + MTBDD ddElseNode = mtbdd_getlow(dd); + thenSubDds[ddIndex] = mtbdd_regular(ddThenNode); + elseSubDds[ddIndex] = mtbdd_regular(ddElseNode); + // Determine whether we have to evaluate the successors as if they were complemented. + thenNegatedSubDds.set(ddIndex, mtbdd_hascomp(ddThenNode) ^ negatedDds.get(ddIndex)); + elseNegatedSubDds.set(ddIndex, mtbdd_hascomp(ddElseNode) ^ negatedDds.get(ddIndex)); + } + } + splitIntoGroupsRec(thenSubDds, thenNegatedSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(elseSubDds, elseNegatedSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + template void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, std::vector>& columnsAndValues, Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool writeValues) const { return toMatrixComponentsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), mtbdd_hascomp(this->getSylvanMtbdd().GetMTBDD()), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, writeValues); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 6e9238481..19a4c3882 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -601,6 +601,17 @@ namespace storm { */ std::vector, InternalAdd>> splitIntoGroups(InternalAdd vector, std::vector const& ddGroupVariableIndices) const; + /*! + * Simultaneously splits the ADD and the given vector ADDs into several ADDs that differ in the encoding of + * the given group variables (given via indices). + * + * @param vectors The vectors to split (in addition to the current ADD). + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of vectors of ADDs such that result.size() is the number of groups and result[i] refers to all ADDs within the same group i (wrt. to the encoding of the given variables). + * result[i].back() always refers to this ADD. + */ + std::vector>> splitIntoGroups(std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const; + /*! * Translates the ADD into the components needed for constructing a matrix. * @@ -702,7 +713,6 @@ namespace storm { * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. * @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. */ void splitIntoGroupsRec(MTBDD dd, bool negated, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; @@ -717,10 +727,21 @@ namespace storm { * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. * @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. */ void splitIntoGroupsRec(MTBDD dd1, bool negated1, MTBDD dd2, bool negated2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + /*! + * Splits the given DDs into the groups using the given group variables. + * + * @param dds The DDs to split. + * @param negatedDds indicates which of the DDs need to be interpreted as negated. + * @param groups A vector that is to be filled with the DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + */ + void splitIntoGroupsRec(std::vector const& dds, storm::storage::BitVector const& negatedDds, std::vector>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + /*! * Builds an ADD representing the given vector. * diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index 66d3dd1b3..bf43b42e2 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -3,6 +3,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" @@ -83,7 +84,28 @@ namespace storm { template std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate(storm::models::symbolic::Mdp const& symbolicMdp, std::vector> const& formulas) { storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd(); - storm::storage::SparseMatrix transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + + // Collect action reward vectors that need translation + std::vector> symbolicActionRewardVectors; + std::map rewardNameToActionRewardIndexMap; + for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) { + if (rewardModelNameAndModel.second.hasStateActionRewards()) { + rewardNameToActionRewardIndexMap.emplace(rewardModelNameAndModel.first, symbolicActionRewardVectors.size()); + symbolicActionRewardVectors.push_back(rewardModelNameAndModel.second.getStateActionRewardVector()); + } + } + // Build transition matrix and (potentially) actionRewardVectors. + storm::storage::SparseMatrix transitionMatrix; + std::vector> actionRewardVectors; + if (symbolicActionRewardVectors.empty()) { + transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + } else { + auto matrRewards = symbolicMdp.getTransitionMatrix().toMatrixVectors(symbolicActionRewardVectors, symbolicMdp.getNondeterminismVariables(), odd, odd); + transitionMatrix = std::move(matrRewards.first); + actionRewardVectors = std::move(matrRewards.second); + } + + // Translate reward models std::unordered_map> rewardModels; for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) { boost::optional> stateRewards; @@ -92,12 +114,14 @@ namespace storm { if (rewardModelNameAndModel.second.hasStateRewards()) { stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd); } - // Note: .getStateActionRewardVector().toVector(odd); does not work as it needs to have information regarding the nondeterminism - // One could use transitionMatrix().toMatrixVector instead. - STORM_LOG_THROW(!rewardModelNameAndModel.second.hasStateActionRewards(), storm::exceptions::NotImplementedException, "Translation of symbolic to explicit state-action rewards is not yet supported."); + auto actRewIndexIt = rewardNameToActionRewardIndexMap.find(rewardModelNameAndModel.first); + if (actRewIndexIt != rewardNameToActionRewardIndexMap.end()) { + stateActionRewards = std::move(actionRewardVectors[actRewIndexIt->second]); + } STORM_LOG_THROW(!rewardModelNameAndModel.second.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Translation of symbolic to explicit transition rewards is not yet supported."); - rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); + rewardModels.emplace(rewardModelNameAndModel.first, storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); } + storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount()); labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd)); @@ -159,6 +183,72 @@ namespace storm { return std::make_shared>(transitionMatrix, labelling, rewardModels); } + + + template + std::shared_ptr> SymbolicMaToSparseMaTransformer::translate(storm::models::symbolic::MarkovAutomaton const& symbolicMa, std::vector> const& formulas) { + storm::dd::Odd odd = symbolicMa.getReachableStates().createOdd(); + // Collect action reward vectors that need translation + std::vector> symbolicActionRewardVectors; + std::map rewardNameToActionRewardIndexMap; + for (auto const& rewardModelNameAndModel : symbolicMa.getRewardModels()) { + if (rewardModelNameAndModel.second.hasStateActionRewards()) { + rewardNameToActionRewardIndexMap.emplace(rewardModelNameAndModel.first, symbolicActionRewardVectors.size()); + symbolicActionRewardVectors.push_back(rewardModelNameAndModel.second.getStateActionRewardVector()); + } + } + // Build transition matrix and (potentially) actionRewardVectors. + storm::storage::SparseMatrix transitionMatrix; + std::vector> actionRewardVectors; + if (symbolicActionRewardVectors.empty()) { + transitionMatrix = symbolicMa.getTransitionMatrix().toMatrix(symbolicMa.getNondeterminismVariables(), odd, odd); + } else { + auto matrRewards = symbolicMa.getTransitionMatrix().toMatrixVectors(symbolicActionRewardVectors, symbolicMa.getNondeterminismVariables(), odd, odd); + transitionMatrix = std::move(matrRewards.first); + actionRewardVectors = std::move(matrRewards.second); + } + + // Translate reward models + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicMa.getRewardModels()) { + boost::optional> stateRewards; + boost::optional> stateActionRewards; + boost::optional> transitionRewards; + if (rewardModelNameAndModel.second.hasStateRewards()) { + stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd); + } + auto actRewIndexIt = rewardNameToActionRewardIndexMap.find(rewardModelNameAndModel.first); + if (actRewIndexIt != rewardNameToActionRewardIndexMap.end()) { + stateActionRewards = std::move(actionRewardVectors[actRewIndexIt->second]); + } + STORM_LOG_THROW(!rewardModelNameAndModel.second.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Translation of symbolic to explicit transition rewards is not yet supported."); + rewardModels.emplace(rewardModelNameAndModel.first, storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); + } + + storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount()); + + labelling.addLabel("init", symbolicMa.getInitialStates().toVector(odd)); + labelling.addLabel("deadlock", symbolicMa.getDeadlockStates().toVector(odd)); + if (formulas.empty()) { + for (auto const& label : symbolicMa.getLabels()) { + labelling.addLabel(label, symbolicMa.getStates(label).toVector(odd)); + } + } else { + LabelInformation labelInfo(formulas); + for (auto const& label : labelInfo.atomicLabels) { + labelling.addLabel(label, symbolicMa.getStates(label).toVector(odd)); + } + for (auto const& expressionLabel : labelInfo.expressionLabels) { + labelling.addLabel(expressionLabel.first, symbolicMa.getStates(expressionLabel.second).toVector(odd)); + } + } + storm::storage::BitVector markovianStates = symbolicMa.getMarkovianStates().toVector(odd); + storm::storage::sparse::ModelComponents components(std::move(transitionMatrix), std::move(labelling), std::move(rewardModels), false, std::move(markovianStates)); + components.exitRates = symbolicMa.getExitRateVector().toVector(odd); + + return std::make_shared>(std::move(components)); + } + template class SymbolicDtmcToSparseDtmcTransformer; template class SymbolicDtmcToSparseDtmcTransformer; @@ -175,5 +265,10 @@ namespace storm { template class SymbolicCtmcToSparseCtmcTransformer; template class SymbolicCtmcToSparseCtmcTransformer; + template class SymbolicMaToSparseMaTransformer; + template class SymbolicMaToSparseMaTransformer; + template class SymbolicMaToSparseMaTransformer; + template class SymbolicMaToSparseMaTransformer; + } } diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h index e2c191b49..98d486ba3 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.h +++ b/src/storm/transformer/SymbolicToSparseTransformer.h @@ -7,6 +7,8 @@ #include "storm/models/symbolic/Mdp.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/symbolic/Ctmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/storage/dd/Odd.h" @@ -34,5 +36,11 @@ namespace storm { public: static std::shared_ptr> translate(storm::models::symbolic::Ctmc const& symbolicCtmc, std::vector> const& formulas = std::vector>()); }; + + template + class SymbolicMaToSparseMaTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::MarkovAutomaton const& symbolicMa, std::vector> const& formulas = std::vector>()); + }; } }