Fixed an issue related to multi-objective model checking of models with potentially infinite expected reward

src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp

@@ -42,12 +42,13 @@ namespace storm {
                 // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers.
                 // We can also merge the states that will have reward zero anyway.
                 storm::storage::BitVector maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates;
+                storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(preprocessorResult.rewardLessInfinityEStates.get(), preprocessorResult.rewardLessInfinityEStates.get());
                 std::set<std::string> relevantRewardModels;
                 for (auto const& obj : this->objectives) {
                     obj.formula->gatherReferencedRewardModels(relevantRewardModels);
                 }
                 storm::transformer::GoalStateMerger<SparseModelType> merger(*preprocessorResult.preprocessedModel);
-                auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
+                auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices);
                 
                 // Initialize data specific for the considered model type
                 initializeModelTypeSpecificData(*mergerResult.model);

src/storm/transformer/GoalStateMerger.cpp

@@ -24,10 +24,10 @@ namespace storm {
         }
             
         template <typename SparseModelType>
-        typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels) const {
+        typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
             STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case.");
   
-            auto result = initialize(maybeStates, targetStates, sinkStates);
+            auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter);
             
             auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second);
             auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first);
@@ -39,7 +39,7 @@ namespace storm {
         }
         
         template <typename SparseModelType>
-        std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const {
+        std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
             
             storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& origMatrix = originalModel.getTransitionMatrix();
             
@@ -58,6 +58,7 @@ namespace storm {
                 for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) {
                     uint_fast64_t transitionsToMaybeStates = 0;
                     bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false);
+                    if (!choiceFilter || choiceFilter.get().get(row)) {
                         for (auto const& entry : origMatrix.getRow(row)) {
                             if (maybeStates.get(entry.getColumn())) {
                                 ++transitionsToMaybeStates;
@@ -83,8 +84,9 @@ namespace storm {
                                 sinkStateRequired = true;
                             }
                         }
-                    STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
                     }
+                }
+                STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
                 ++stateCount;
             }
             

src/storm/transformer/GoalStateMerger.h

@@ -35,6 +35,8 @@ namespace storm {
              *  * one target state to which all transitions to a state selected by targetStates are redirected and
              *  * one sink state to which all transitions to a state selected by sinkStates are redirected.
              *
+             * If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed.
+             *
              *  Notes:
              *  * the target (or sink) state is not created, if it is not reachable
              *  * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label.
@@ -43,7 +45,7 @@ namespace storm {
              *  * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.
              *  * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model).
              */
-             ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>()) const;
+             ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>(), boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
             
         private:
             SparseModelType const& originalModel;
@@ -53,7 +55,7 @@ namespace storm {
              *
              * @return The initialized result and the number of transitions of the result model
              */
-            std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const;
+            std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
             
             /*!
              * Builds the transition matrix of the resulting model