started building the model for a given epoch

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 ValueType>
             typename MultiDimensionalRewardUnfolding<ValueType>::EpochModel  MultiDimensionalRewardUnfolding<ValueType>::computeModelForEpoch(Epoch const& epoch) {
                 
                 storm::storage::MemoryStructure memory = computeMemoryStructureForEpoch(epoch);
+                auto modelMemoryProductBuilder = memory.product(model);
+                modelMemoryProductBuilder.setBuildFullProduct();
+                auto modelMemoryProduct = modelMemoryProductBuilder.build()->template as<storm::models::sparse::Mdp<ValueType>>();
+                
+                storm::storage::SparseMatrix<ValueType> 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());
                 
                 
             }

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

@@ -17,11 +17,14 @@ namespace storm {
             class MultiDimensionalRewardUnfolding {
             public:
                 
+                typedef std::vector<int64_t> 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<ValueType> rewardTransitions;
                     storm::storage::SparseMatrix<ValueType> intermediateTransitions;
                     std::vector<std::vector<ValueType>> objectiveRewards;
+                    std::vector<boost::optional<Epoch>> epochSteps;
                 };
                 
                 struct EpochSolution {
@@ -29,8 +32,6 @@ namespace storm {
                     std::vector<std::vector<ValueType>> objectiveValues;
                 };
                 
-                typedef std::vector<int64_t> 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
                 
                 /*
                  *

src/storm/storage/SparseMatrix.cpp

@@ -568,6 +568,27 @@ namespace storm {
             return rowGroupIndices.get();
         }
 
+        template<typename ValueType>
+        void SparseMatrix<ValueType>::setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices) {
+            trivialRowGrouping = false;
+            rowGroupIndices = newRowGroupIndices;
+        }
+
+        template<typename ValueType>
+        bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
+            return trivialRowGrouping;
+        }
+        
+        template<typename ValueType>
+        void SparseMatrix<ValueType>::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<typename ValueType>
         storm::storage::BitVector SparseMatrix<ValueType>::getRowFilter(storm::storage::BitVector const& groupConstraint) const {
             storm::storage::BitVector res(this->getRowCount(), false);
@@ -968,6 +989,30 @@ namespace storm {
             return res;
         }
         
+        template<typename ValueType>
+        SparseMatrix<ValueType> SparseMatrix<ValueType>::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<ValueType> builder(getRowCount(), getColumnCount(), entryCount);
+            for (auto const& row : rowFilter) {
+                for (auto const& entry : getRow(row)) {
+                    builder.addNextValue(row, entry.getColumn(), entry.getValue());
+                }
+            }
+            SparseMatrix<ValueType> result = builder.build();
+            
+            // Add a row grouping if necessary.
+            if (!hasTrivialRowGrouping()) {
+                result.setRowGroupIndices(getRowGroupIndices());
+            }
+            return result;
+        }
+        
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> 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<ValueType>::iterator SparseMatrix<ValueType>::end()  {
             return this->columnsAndValues.begin() + this->rowIndications[rowCount];
         }
-        
-        template<typename ValueType>
-        bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
-            return trivialRowGrouping;
-        }
-        
-        template<typename ValueType>
-        void SparseMatrix<ValueType>::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<typename ValueType>
         ValueType SparseMatrix<ValueType>::getRowSum(index_type row) const {
             ValueType sum = storm::utility::zero<ValueType>();

src/storm/storage/SparseMatrix.h

@@ -563,6 +563,27 @@ namespace storm {
              */
             std::vector<index_type> 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<index_type> 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
 			*/