From fb6aa697509ddb3775726315c8e4581af4247c28 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 27 Jul 2017 11:28:38 +0200 Subject: [PATCH] started building the model for a given epoch --- .../MultiDimensionalRewardUnfolding.cpp | 38 +++++++++++- .../MultiDimensionalRewardUnfolding.h | 5 +- src/storm/storage/SparseMatrix.cpp | 62 ++++++++++++++----- src/storm/storage/SparseMatrix.h | 43 +++++++++---- 4 files changed, 115 insertions(+), 33 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 9a85e6e64..5cbadbe08 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -3,6 +3,8 @@ #include "storm/utility/macros.h" #include "storm/logic/Formulas.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" + #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -135,12 +137,44 @@ namespace storm { } } - - template typename MultiDimensionalRewardUnfolding::EpochModel MultiDimensionalRewardUnfolding::computeModelForEpoch(Epoch const& epoch) { storm::storage::MemoryStructure memory = computeMemoryStructureForEpoch(epoch); + auto modelMemoryProductBuilder = memory.product(model); + modelMemoryProductBuilder.setBuildFullProduct(); + auto modelMemoryProduct = modelMemoryProductBuilder.build()->template as>(); + + storm::storage::SparseMatrix const& allTransitions = modelMemoryProduct->getTransitionMatrix(); + EpochModel result; + storm::storage::BitVector rewardChoices(allTransitions.getRowCount(), false); + result.epochSteps.resize(modelMemoryProduct->getNumberOfChoices()); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + uint64_t numChoices = allTransitions.getRowGroupSize(modelState); + uint64_t firstChoice = allTransitions.getRowGroupIndices()[modelState]; + for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) { + Epoch step; + bool isZeroStep = true; + for (uint64_t dim = 0; dim < epoch.size(); ++dim) { + step.push_back(scaledRewards[dim][firstChoice + choiceOffset]); + isZeroStep = isZeroStep && (step.back() == 0 || epoch[dim] < 0); + } + if (!isZeroStep) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + uint64_t productState = modelMemoryProductBuilder.getResultState(modelState, memState); + uint64_t productChoice = allTransitions.getRowGroupIndices()[productState] + choiceOffset; + assert(productChoice < allTransitions.getRowGroupIndices()[productState + 1]); + result.epochSteps[productChoice] = step; + rewardChoices.set(productChoice, true); + } + } + } + } + + result.rewardTransitions = allTransitions.filterEntries(rewardChoices); + result.intermediateTransitions = allTransitions.filterEntries(~rewardChoices); + + result.objectiveRewards.resize(objectives.size()); } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index b7e3dafd2..13705aae9 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -17,11 +17,14 @@ namespace storm { class MultiDimensionalRewardUnfolding { public: + typedef std::vector Epoch; // The number of reward steps that are "left" for each dimension + typedef uint64_t EpochClass; // Collection of epochs that consider the same epoch model struct EpochModel { storm::storage::SparseMatrix rewardTransitions; storm::storage::SparseMatrix intermediateTransitions; std::vector> objectiveRewards; + std::vector> epochSteps; }; struct EpochSolution { @@ -29,8 +32,6 @@ namespace storm { std::vector> objectiveValues; }; - typedef std::vector Epoch; // The number of reward steps that are "left" for each dimension - typedef uint64_t EpochClass; // Collection of epochs that consider the same epoch model /* * diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 1a005d2d0..462990fad 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -568,6 +568,27 @@ namespace storm { return rowGroupIndices.get(); } + template + void SparseMatrix::setRowGroupIndices(std::vector const& newRowGroupIndices) { + trivialRowGrouping = false; + rowGroupIndices = newRowGroupIndices; + } + + template + bool SparseMatrix::hasTrivialRowGrouping() const { + return trivialRowGrouping; + } + + template + void SparseMatrix::makeRowGroupingTrivial() { + if (trivialRowGrouping) { + STORM_LOG_ASSERT(!rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1), "Row grouping is supposed to be trivial but actually it is not."); + } else { + trivialRowGrouping = true; + rowGroupIndices = boost::none; + } + } + template storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint) const { storm::storage::BitVector res(this->getRowCount(), false); @@ -968,6 +989,30 @@ namespace storm { return res; } + template + SparseMatrix SparseMatrix::filterEntries(storm::storage::BitVector const& rowFilter) const { + // Count the number of entries in the resulting matrix. + index_type entryCount = 0; + for (auto const& row : rowFilter) { + entryCount += getRow(row).getNumberOfEntries(); + } + + // Build the resulting matrix. + SparseMatrixBuilder builder(getRowCount(), getColumnCount(), entryCount); + for (auto const& row : rowFilter) { + for (auto const& entry : getRow(row)) { + builder.addNextValue(row, entry.getColumn(), entry.getValue()); + } + } + SparseMatrix result = builder.build(); + + // Add a row grouping if necessary. + if (!hasTrivialRowGrouping()) { + result.setRowGroupIndices(getRowGroupIndices()); + } + return result; + } + template SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for @@ -1531,22 +1576,7 @@ namespace storm { typename SparseMatrix::iterator SparseMatrix::end() { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } - - template - bool SparseMatrix::hasTrivialRowGrouping() const { - return trivialRowGrouping; - } - - template - void SparseMatrix::makeRowGroupingTrivial() { - if (trivialRowGrouping) { - STORM_LOG_ASSERT(!rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1), "Row grouping is supposed to be trivial but actually it is not."); - } else { - trivialRowGrouping = true; - rowGroupIndices = boost::none; - } - } - + template ValueType SparseMatrix::getRowSum(index_type row) const { ValueType sum = storm::utility::zero(); diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index bd8c1bad1..6d959d371 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -563,6 +563,27 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; + /*! + * Sets the row grouping to the given one. + * @note It is assumed that the new row grouping is non-trivial. + * + * @param newRowGroupIndices The new row group indices. + */ + void setRowGroupIndices(std::vector const& newRowGroupIndices); + + /*! + * Retrieves whether the matrix has a trivial row grouping. + * + * @return True iff the matrix has a trivial row grouping. + */ + bool hasTrivialRowGrouping() const; + + /*! + * Makes the row grouping of this matrix trivial. + * Has no effect when the row grouping is already trivial. + */ + void makeRowGroupingTrivial(); + /*! * Returns the indices of the rows that belong to one of the selected row groups. * @@ -665,6 +686,15 @@ namespace storm { */ SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups = false) const; + /*! + * Returns a copy of this matrix that only considers entries in the selected rows. + * Non-selected rows will not have any entries + * + * @note does not change the dimensions (row-, column-, and rowGroup count) of this matrix + * @param rowFilter the selected rows + */ + SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; + /** * Compares two rows. * @param i1 Index of first row @@ -1005,19 +1035,6 @@ s * @param insertDiagonalEntries If set to true, the resulting matri */ iterator end(); - /*! - * Retrieves whether the matrix has a trivial row grouping. - * - * @return True iff the matrix has a trivial row grouping. - */ - bool hasTrivialRowGrouping() const; - - /*! - * Makes the row grouping of this matrix trivial. - * Has no effect when the row grouping is already trivial. - */ - void makeRowGroupingTrivial(); - /*! * Returns a copy of the matrix with the chosen internal data type */