From 4d7770aea6ce847235111089c9abdbf4aeb26412 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Oct 2017 14:16:55 +0200 Subject: [PATCH] fixed issue in hybrid reachability reward computation that caused empty row groups --- .../prctl/helper/HybridMdpPrctlHelper.cpp | 4 +++- src/storm/storage/dd/Add.cpp | 24 ++++++++++++------- src/storm/storage/dd/Add.h | 3 ++- 3 files changed, 20 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index c43e3e66a..1d6864fa3 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -530,11 +530,13 @@ namespace storm { // Then compute the reward vector to use in the computation. storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, choiceFilterAdd, submatrix, model.getColumnVariables()); + std::vector rowGroupSizes = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd().sumAbstract(model.getNondeterminismVariables()).toVector(odd); + // Finally cut away all columns targeting non-maybe states (or non-(maybe or target) states, respectively). submatrix *= extendMaybeStates ? maybeStatesWithTargetStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd() : maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Translate the symbolic matrix/vector to their explicit representations. - std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd); + std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(std::move(rowGroupSizes), subvector, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), odd, odd); // Fulfill the solver's requirements. SolverRequirementsData solverRequirementsData; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index ed8e2a966..a62600562 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -799,6 +799,14 @@ namespace storm { template std::pair, std::vector> Add::toMatrixVector(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 { + + // Count how many choices each row group has. + std::vector rowGroupIndices = (this->notZero().existsAbstract(columnMetaVariables) || vector.notZero()).template toAdd().sumAbstract(groupMetaVariables).toVector(rowOdd); + return toMatrixVector(std::move(rowGroupIndices), vector, rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + 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 { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -829,9 +837,6 @@ namespace storm { std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); Bdd columnVariableCube = Bdd::getCube(this->getDdManager(), columnMetaVariables); - - // Count how many choices each row group has. - std::vector rowGroupIndices = (this->notZero().existsAbstract(columnMetaVariables) || vector.notZero()).template toAdd().sumAbstract(groupMetaVariables).toVector(rowOdd); // Transform the row group sizes to the actual row group indices. rowGroupIndices.resize(rowGroupIndices.size() + 1); @@ -853,7 +858,7 @@ namespace storm { for (auto const& internalAdd : internalAddGroups) { groups.push_back(std::make_pair(Add(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables), Add(this->getDdManager(), internalAdd.second, rowMetaVariables))); } - + // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); @@ -866,12 +871,12 @@ namespace storm { std::pair, Add> const& ddPair = groups[i]; Bdd matrixDdNotZero = ddPair.first.notZero(); Bdd vectorDdNotZero = ddPair.second.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()); statesWithGroupEnabled[i] = (matrixDdNotZero.existsAbstract(columnMetaVariables) || vectorDdNotZero).template toAdd(); @@ -881,7 +886,7 @@ namespace storm { // Since we modified the rowGroupIndices, we need to restore the correct values. stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); - + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. tmp = 0; tmp2 = 0; @@ -908,10 +913,11 @@ namespace storm { rowIndications[i] = rowIndications[i - 1]; } rowIndications[0] = 0; - + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector)); - } + } + template void Add::exportToDot(std::string const& filename, bool showVariablesIfPossible) const { internalAdd.exportToDot(filename, this->getDdManager().getDdVariableNames(), showVariablesIfPossible); diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 8f3100b18..c25b5a8c4 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -639,7 +639,8 @@ namespace storm { * @return The matrix that is represented by this ADD. */ 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; + /*! * Exports the DD to the given file in the dot format. *