Correctly handled reward bounded objectives in multi-objective preprocessing

src/storm/modelchecker/multiobjective/Objective.h

@@ -5,6 +5,7 @@
 #include "storm/logic/Formula.h"
 #include "storm/logic/Bound.h"
 #include "storm/logic/TimeBound.h"
+#include "storm/logic/TimeBoundType.h"
 #include "storm/solver/OptimizationDirection.h"
 
 namespace storm {
@@ -28,8 +29,9 @@ namespace storm {
                 // if originalFormula does ot specifies one, the direction is derived from the bound.
                 storm::solver::OptimizationDirection optimizationDirection;
                 
-                // Lower and upper time/step bouds
+                // Lower and upper time/step/reward bouds
                 boost::optional<storm::logic::TimeBound> lowerTimeBound, upperTimeBound;
+                boost::optional<storm::logic::TimeBoundReference> timeBoundReference;
                 
                 boost::optional<ValueType> lowerResultBound, upperResultBound;
                 

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -1,7 +1,7 @@
 #include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h"
 
 #include <algorithm>
-#include <storm/transformer/GoalStateMerger.h>
+#include <set>
 
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
@@ -12,7 +12,7 @@
 #include "storm/storage/memorystructure/MemoryStructureBuilder.h"
 #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
 #include "storm/storage/expressions/ExpressionManager.h"
-#include "storm/transformer/SubsystemBuilder.h"
+#include "storm/transformer/GoalStateMerger.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
@@ -266,8 +266,6 @@ namespace storm {
             
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) {
-                STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata.");
-                
                 if (formula.hasLowerBound()) {
                     STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables");
                     if (!storm::utility::isZero(formula.getLowerBound<double>()) || formula.isLowerBoundStrict()) {
@@ -280,6 +278,8 @@ namespace storm {
                         data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound());
                     }
                 }
+                
+                data.objectives.back()->timeBoundReference = formula.getTimeBoundReference();
                 preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data);
             }
             
@@ -375,6 +375,9 @@ namespace storm {
                 std::set<std::string> relevantRewardModels;
                 for (auto const& obj : result.objectives) {
                     relevantRewardModels.insert(*obj.rewardModelName);
+                    if (obj.timeBoundReference->isRewardBound()) {
+                        relevantRewardModels.insert(obj.timeBoundReference->getRewardName());
+                    }
                 }
                 
                 // Build a subsystem that discards states that yield infinite reward for all schedulers.

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

@@ -41,6 +41,10 @@ namespace storm {
             template <class SparseMaModelType>
             void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
                 
+                for (auto const& obj : this->objectives) {
+                    STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass.");
+                }
+                
                 // Split the preprocessed model into transitions from/to probabilistic/Markovian states.
                 SubModel MS = createSubModel(true, weightedRewardVector);
                 SubModel PS = createSubModel(false, weightedRewardVector);

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

@@ -6,6 +6,9 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 
 namespace storm {
@@ -28,6 +31,24 @@ namespace storm {
             
             template <class SparseMdpModelType>
             void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
+                // Check whether reward bounded objectives occur.
+                bool containsRewardBoundedObjectives = false;
+                for (auto const& obj : this->objectives) {
+                    if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) {
+                        containsRewardBoundedObjectives = true;
+                        break;
+                    }
+                }
+                
+                if (containsRewardBoundedObjectives) {
+                    boundedPhaseWithRewardBounds(weightVector, weightedRewardVector);
+                } else {
+                    boundedPhaseOnlyStepBounds(weightVector, weightedRewardVector);
+                }
+            }
+
+            template <class SparseMdpModelType>
+            void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhaseOnlyStepBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
                 // Allocate some memory so this does not need to happen for each time epoch
                 std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->model.getNumberOfStates());
                 std::vector<ValueType> choiceValues(weightedRewardVector.size());
@@ -97,6 +118,13 @@ namespace storm {
                 }
             }
             
+            
+            template <class SparseMdpModelType>
+            void SparseMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhaseWithRewardBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Multi-objective model checking with reward bounded objectives is not supported.");
+            }
+            
+            
             template class SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
 #ifdef STORM_HAVE_CARL
             template class SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h

@@ -19,6 +19,7 @@ namespace storm {
             class SparseMdpPcaaWeightVectorChecker : public SparsePcaaWeightVectorChecker<SparseMdpModelType> {
             public:
                 typedef typename SparseMdpModelType::ValueType ValueType;
+                typedef typename SparseMdpModelType::RewardModelType RewardModelType;
             
                 /*
                  * Creates a weight vextor checker.
@@ -40,16 +41,32 @@ namespace storm {
             private:
                 
                 /*!
-                 * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method
-                 * - determines the objectives that are relevant in the current time epoch
-                 * - determines the maximizing scheduler for the weighted reward vector of these objectives
-                 * - computes the values of these objectives w.r.t. this scheduler
+                 * Computes the maximizing scheduler for the weighted sum of the objectives, including also step or reward bounded objectives.
+                 * Moreover, the values of the individual objectives are computed w.r.t. this scheduler.
                  *
                  * @param weightVector the weight vector of the current check
                  * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
                  */
                 virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override;
-  
+                
+                /*!
+                 * Computes the bounded phase for the case that only step bounded objectives are considered.
+                 *
+                 * @param weightVector the weight vector of the current check
+                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
+                 */
+                void boundedPhaseOnlyStepBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector);
+                
+                /*!
+                 * Computes the bounded phase for the case that also reward bounded objectives occurr.
+                 *
+                 * @param weightVector the weight vector of the current check
+                 * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this.
+                 */
+                void boundedPhaseWithRewardBounds(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector);
+                
+ 
+                
             };
             
         }