Improved and fixed multiObjectivePreprocessor

src/storm/modelchecker/multiobjective/Objective.h

@@ -31,6 +31,8 @@ namespace storm {
                 // Lower and upper time/step bouds
                 boost::optional<storm::logic::TimeBound> lowerTimeBound, upperTimeBound;
                 
+                boost::optional<ValueType> lowerResultBound, upperResultBound;
+                
                 void printToStream(std::ostream& out) const {
                     out  << originalFormula->toString();
                     out << " \t";
@@ -39,7 +41,7 @@ namespace storm {
                     out << " \t";
                     out << "intern bound: ";
                     if (bound){
-                        out << bound;
+                        out << *bound;
                     } else {
                         out << " -none-    ";
                     }
@@ -55,7 +57,23 @@ namespace storm {
                         out << " -none-    ";
                     }
                     out << " \t";
-                    out << "intern reward model: " << *rewardModelName;
+                    out << "intern reward model: ";
+                    if (rewardModelName) {
+                        out << *rewardModelName;
+                    } else {
+                        out << " -none-    ";
+                    }
+                    out << " \t";
+                    out << "result bounds: ";
+                    if (lowerResultBound && upperResultBound) {
+                        out << "[" << *lowerResultBound << ", " << *upperResultBound << "]";
+                    } else if (lowerResultBound) {
+                        out << ">=" << *lowerResultBound;
+                    } else if (upperResultBound) {
+                        out << "<=" << *upperResultBound;
+                    } else {
+                        out << " -none-    ";
+                    }
                  }
             };
         }

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -44,16 +44,19 @@ namespace storm {
                     }
                 }
                 
+                // Incorporate the required memory into the state space
                 storm::storage::SparseModelMemoryProduct<ValueType> product = data.memory->product(originalModel);
                 std::shared_ptr<SparseModelType> preprocessedModel = std::dynamic_pointer_cast<SparseModelType>(product.build());
                 
                 auto backwardTransitions = preprocessedModel->getBackwardTransitions();
                 
+                // compute the end components of the model (if required)
                 bool endComponentAnalysisRequired = false;
                 for (auto& task : data.tasks) {
                     endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis();
                 }
                 if (endComponentAnalysisRequired) {
+                    // TODO
                     STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented.");
                 }
                 
@@ -61,41 +64,8 @@ namespace storm {
                     task->perform(*preprocessedModel);
                 }
                 
-                ReturnType result(originalFormula, originalModel);
-                for (auto& obj : data.objectives) {
-                    result.objectives.push_back(std::move(*obj));
-                }
-                result.preprocessedModel = std::move(preprocessedModel);
-                result.queryType = ReturnType::QueryType::Achievability;
-                
-                auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions);
-                auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions);
-                
-                std::set<std::string> relevantRewardModels;
-                for (auto const& obj : result.objectives) {
-                    relevantRewardModels.insert(*obj.rewardModelName);
-                }
-                
-                // Build a subsystem 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 zeroRewardStates = ~minMaxNonZeroRewardStates.second;
-                storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel);
-                typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(finiteRewardStates, zeroRewardStates, storm::storage::BitVector(finiteRewardStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
-                
-                result.preprocessedModel = mergerResult.model;
-                result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % finiteRewardStates;
-                if (mergerResult.targetState) {
-                    storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
-                    targetStateAsVector.set(*mergerResult.targetState, true);
-                    result.possibleECChoices = storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector);
-                    result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true);
-                    // There is an additional state in the result
-                    result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true);
-                }
-                assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates());
-                
-                
-                return result;
+                // Build the actual result
+                return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions);
             }
             
             template <typename SparseModelType>
@@ -139,8 +109,6 @@ namespace storm {
                         break;
                     }
                 }
-                
-                
             }
             
             template<typename SparseModelType>
@@ -189,6 +157,10 @@ namespace storm {
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) {
                 
+                // Probabilities are between zero and one
+                data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
+                data.objectives.back()->upperResultBound = storm::utility::one<ValueType>();
+                
                 if (formula.getSubformula().isUntilFormula()){
                     preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data);
                 } else if (formula.getSubformula().isBoundedUntilFormula()){
@@ -217,6 +189,8 @@ namespace storm {
                     rewardModelName = data.originalModel.getRewardModels().begin()->first;
                 }
                 
+                data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
+                
                 if (formula.getSubformula().isEventuallyFormula()){
                     preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName);
                 } else if (formula.getSubformula().isCumulativeRewardFormula()) {
@@ -233,6 +207,8 @@ namespace storm {
                 // Time formulas are only supported for Markov automata
                 STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
                 
+                data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
+                
                 if (formula.getSubformula().isEventuallyFormula()){
                     preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data);
                 } else {
@@ -344,6 +320,8 @@ namespace storm {
                     data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound());
                 }
 
+                assert(optionalRewardModelName.is_initialized());
+                data.objectives.back()->rewardModelName = *optionalRewardModelName;
 
             }
             
@@ -354,6 +332,68 @@ namespace storm {
                 data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
             }
             
+            template<typename SparseModelType>
+            typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr<SparseModelType> const& preprocessedModel, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+                        
+                ReturnType result(originalFormula, originalModel);
+                
+                result.preprocessedModel = preprocessedModel;
+                
+                for (auto& obj : data.objectives) {
+                    result.objectives.push_back(std::move(*obj));
+                }
+                
+                result.queryType = getQueryType(result.objectives);
+                
+                auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions);
+                auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions);
+                
+                std::set<std::string> relevantRewardModels;
+                for (auto const& obj : result.objectives) {
+                    relevantRewardModels.insert(*obj.rewardModelName);
+                }
+                
+                // Build a subsystem 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 zeroRewardStates = ~minMaxNonZeroRewardStates.second;
+                storm::storage::BitVector maybeStates = finiteRewardStates & ~zeroRewardStates;
+                storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel);
+                typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, zeroRewardStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
+                
+                result.preprocessedModel = mergerResult.model;
+                result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % maybeStates;
+                if (mergerResult.targetState) {
+                    storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
+                    targetStateAsVector.set(*mergerResult.targetState, true);
+                    result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowIndicesOfRowGroups(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
+                    result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true);
+                    // There is an additional state in the result
+                    result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true);
+                }
+                assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates());
+                
+                return result;
+            }
+            
+            template<typename SparseModelType>
+            typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType::QueryType SparseMultiObjectivePreprocessor<SparseModelType>::getQueryType(std::vector<Objective<ValueType>> const& objectives) {
+                uint_fast64_t numOfObjectivesWithThreshold = 0;
+                for (auto& obj : objectives) {
+                    if (obj.bound) {
+                        ++numOfObjectivesWithThreshold;
+                    }
+                }
+                if (numOfObjectivesWithThreshold == objectives.size()) {
+                    return ReturnType::QueryType::Achievability;
+                } else if (numOfObjectivesWithThreshold + 1 == objectives.size()) {
+                    // Note: We do not want to consider a Pareto query when the total number of objectives is one.
+                    return ReturnType::QueryType::Quantitative;
+                } else if (numOfObjectivesWithThreshold == 0) {
+                    return ReturnType::QueryType::Pareto;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Invalid Multi-objective query: The numer of qualitative objectives should be either 0 (Pareto query), 1 (quantitative query), or #objectives (achievability query).");
+                }
+            }
             
             template<typename SparseModelType>
             std::pair<storm::storage::BitVector, storm::storage::BitVector> SparseMultiObjectivePreprocessor<SparseModelType>::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h

@@ -65,6 +65,17 @@ namespace storm {
                 static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique.
                 
                 
+                /*!
+                 * Builds the result from preprocessing
+                 */
+                static ReturnType buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr<SparseModelType> const& preprocessedModel, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+                
+                /*!
+                 * Returns the query type
+                 */
+                 static typename ReturnType::QueryType getQueryType(std::vector<Objective<ValueType>> const& objectives);
+                
+                
                 /*!
                  * Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively.
                  */

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h

@@ -6,6 +6,7 @@
 
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/multiobjective/Objective.h"
+#include "storm/storage/BitVector.h"
 
 #include "storm/exceptions/UnexpectedException.h"
 
@@ -16,7 +17,7 @@ namespace storm {
             template <class SparseModelType>
             struct SparseMultiObjectivePreprocessorReturnType {
                 
-                enum class QueryType { Achievability };
+                enum class QueryType { Achievability, Quantitative, Pareto };
                 
                 storm::logic::MultiObjectiveFormula const& originalFormula;
                 SparseModelType const& originalModel;