adapt multi-objective model checking components to new preprocessing

src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp

@@ -26,8 +26,8 @@ namespace storm {
             
             
             template <class SparseModelType>
-            SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) {
-                STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
+            SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) {
+                STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
                 solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager);
             }
 

src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h

@@ -19,7 +19,7 @@ namespace storm {
                 
                 typedef typename SparseModelType::ValueType ValueType;
                 
-                SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
+                SparseCbAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
                 
                 virtual ~SparseCbAchievabilityQuery() = default;
 

src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp

@@ -1,5 +1,6 @@
 #include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h"
 
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
@@ -20,26 +21,28 @@ namespace storm {
             
             
             template <class SparseModelType>
-            SparseCbQuery<SparseModelType>::SparseCbQuery(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) :
+            SparseCbQuery<SparseModelType>::SparseCbQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) :
                 originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), objectives(std::move(preprocessorResult.objectives)) {
              
-                STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult<SparseModelType>::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
-                STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
+                auto rewardAnalysis = preprocessing::SparseMultiObjectiveRewardAnalysis<SparseModelType>::analyze(preprocessorResult);
+                STORM_LOG_THROW(rewardAnalysis.rewardFinitenessType != preprocessing::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "TThere is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
+                
+                STORM_LOG_THROW(rewardAnalysis.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
                 STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
                 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
                 
                 // 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 maybeStates = rewardAnalysis.rewardLessInfinityEStates.get() & ~rewardAnalysis.reward0AStates;
                 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, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
                 
                 preprocessedModel = mergerResult.model;
-                reward0EStates = preprocessorResult.reward0EStates % maybeStates;
+                reward0EStates = rewardAnalysis.reward0EStates % maybeStates;
                 if (mergerResult.targetState) {
                     // There is an additional state in the result
                     reward0EStates.resize(reward0EStates.size() + 1, true);

src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h

@@ -3,7 +3,7 @@
 #include <memory>
 
 #include "storm/modelchecker/results/CheckResult.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
 namespace storm {
@@ -30,7 +30,7 @@ namespace storm {
                 
             protected:
                 
-                SparseCbQuery(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
+                SparseCbQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
                 
                 SparseModelType const& originalModel;
                 storm::logic::MultiObjectiveFormula const& originalFormula;

src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp

@@ -5,13 +5,12 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
 #include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/utility/Stopwatch.h"
 
@@ -23,7 +22,7 @@ namespace storm {
         namespace multiobjective {
             
             template<typename SparseModelType>
-            std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula,  MultiObjectiveMethodSelection methodSelection) {
+            std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) {
                 storm::utility::Stopwatch swTotal(true);
                 storm::utility::Stopwatch swPreprocessing(true);
                 STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported.");
@@ -34,7 +33,7 @@ namespace storm {
                 }
                 
                 // Preprocess the model
-                auto preprocessorResult = SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(model, formula);
+                auto preprocessorResult = preprocessing::SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(model, formula);
                 swPreprocessing.stop();
                 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
                     STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl);
@@ -42,29 +41,23 @@ namespace storm {
                     STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl);
                 }
                 
-                // Get the solution method
-                MultiObjectiveMethod method;
-                if (methodSelection == MultiObjectiveMethodSelection::FROMSETTINGS) {
-                     method =  storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMultiObjectiveMethod();
-                } else {
-                    method = convert(methodSelection);
-                }
                 
                 // Invoke the analysis
                 storm::utility::Stopwatch swAnalysis(true);
                 std::unique_ptr<CheckResult> result;
+                MultiObjectiveMethod method = env.modelchecker().multi().getMethod();
                 switch (method) {
                     case MultiObjectiveMethod::Pcaa:
                     {
                         std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query;
                         switch (preprocessorResult.queryType) {
-                            case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
+                            case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
                                 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaAchievabilityQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
                                 break;
-                            case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative:
+                            case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative:
                                 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaQuantitativeQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
                                 break;
-                            case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto:
+                            case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto:
                                 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaParetoQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
                                 break;
                             default:
@@ -83,7 +76,7 @@ namespace storm {
                     {
                         std::unique_ptr<SparseCbQuery<SparseModelType>> query;
                         switch (preprocessorResult.queryType) {
-                            case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
+                            case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
                                 query = std::unique_ptr<SparseCbQuery<SparseModelType>> (new SparseCbAchievabilityQuery<SparseModelType>(preprocessorResult));
                                 break;
                             default:
@@ -93,7 +86,7 @@ namespace storm {
                         
                         result = query->check(env);
                      
-                        if(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) {
+                        if (env.modelchecker().multi().isExportPlotSet()) {
                             STORM_LOG_ERROR("Can not export plot for the constrained based solver.");
                         }
                         break;
@@ -112,10 +105,10 @@ namespace storm {
             }
      
             
-            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<double>>(Environment const& env, storm::models::sparse::Mdp<double> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection);
-            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<double>>(Environment const& env, storm::models::sparse::MarkovAutomaton<double> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection);
-            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<storm::RationalNumber>>(Environment const& env, storm::models::sparse::Mdp<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection);
-            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(Environment const& env, storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection);
+            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<double>>(Environment const& env, storm::models::sparse::Mdp<double> const& model, storm::logic::MultiObjectiveFormula const& formula);
+            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<double>>(Environment const& env, storm::models::sparse::MarkovAutomaton<double> const& model, storm::logic::MultiObjectiveFormula const& formula);
+            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<storm::RationalNumber>>(Environment const& env, storm::models::sparse::Mdp<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula);
+            template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(Environment const& env, storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula);
 
         }
     }

src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h

@@ -15,7 +15,7 @@ namespace storm {
             
             
             template<typename SparseModelType>
-            std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS);
+            std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula);
             
         }
     }

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

@@ -53,7 +53,7 @@ namespace storm {
 
             template <typename ModelType>
             template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type>
-            std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {
+            std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {
                 if (preprocessorResult.containsOnlyTrivialObjectives()) {
                     return std::make_unique<StandardMdpPcaaWeightVectorChecker<ModelType>>(preprocessorResult);
                 } else {
@@ -64,7 +64,7 @@ namespace storm {
             
             template <typename ModelType>
             template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::MarkovAutomaton<VT>>::value, int>::type>
-            std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {
+            std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {
                 return std::make_unique<StandardMaPcaaWeightVectorChecker<ModelType>>(preprocessorResult);
             }
             
@@ -78,10 +78,10 @@ namespace storm {
             template class WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<double>>;
             template class WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
             
-            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>>  WeightVectorCheckerFactory<storm::models::sparse::Mdp<double>>::create(SparseMultiObjectivePreprocessorResult<storm::models::sparse::Mdp<double>> const& preprocessorResult);
-            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>>  WeightVectorCheckerFactory<storm::models::sparse::Mdp<storm::RationalNumber>>::create(SparseMultiObjectivePreprocessorResult<storm::models::sparse::Mdp<storm::RationalNumber>> const& preprocessorResult);
-            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>>  WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<double>>::create(SparseMultiObjectivePreprocessorResult<storm::models::sparse::MarkovAutomaton<double>> const& preprocessorResult);
-            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>>  WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::create(SparseMultiObjectivePreprocessorResult<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> const& preprocessorResult);
+            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>>  WeightVectorCheckerFactory<storm::models::sparse::Mdp<double>>::create(preprocessing::SparseMultiObjectivePreprocessorResult<storm::models::sparse::Mdp<double>> const& preprocessorResult);
+            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>>  WeightVectorCheckerFactory<storm::models::sparse::Mdp<storm::RationalNumber>>::create(preprocessing::SparseMultiObjectivePreprocessorResult<storm::models::sparse::Mdp<storm::RationalNumber>> const& preprocessorResult);
+            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>>  WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<double>>::create(preprocessing::SparseMultiObjectivePreprocessorResult<storm::models::sparse::MarkovAutomaton<double>> const& preprocessorResult);
+            template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>>  WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::create(preprocessing::SparseMultiObjectivePreprocessorResult<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> const& preprocessorResult);
             
 
         }

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

@@ -5,7 +5,7 @@
 #include "storm/storage/Scheduler.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 #include "storm/modelchecker/multiobjective/Objective.h"
 
 
@@ -93,10 +93,10 @@ namespace storm {
             public:
 
                 template<typename VT = typename ModelType::ValueType, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type = 0>
-                static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
+                static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
                 
                 template<typename VT = typename ModelType::ValueType, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::MarkovAutomaton<VT>>::value, int>::type = 0>
-                static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
+                static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(preprocessing::SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult);
             };
 
         }

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

@@ -3,6 +3,7 @@
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/ProgressMeasurement.h"
@@ -32,9 +33,10 @@ namespace storm {
         namespace multiobjective {
             
             template <class SparseMdpModelType>
-            RewardBoundedMdpPcaaWeightVectorChecker<SparseMdpModelType>::RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) {
+            RewardBoundedMdpPcaaWeightVectorChecker<SparseMdpModelType>::RewardBoundedMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) {
                 
-                STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one  objective. This is not supported.");
+                auto rewardAnalysis = preprocessing::SparseMultiObjectiveRewardAnalysis<SparseMdpModelType>::analyze(preprocessorResult);
+                STORM_LOG_THROW(rewardAnalysis.rewardFinitenessType == preprocessing::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one  objective. This is not supported.");
                 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
                 
                 // Update the objective bounds with what the reward unfolding can compute

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

@@ -25,7 +25,7 @@ namespace storm {
                 typedef typename SparseMdpModelType::ValueType ValueType;
                 typedef typename SparseMdpModelType::RewardModelType RewardModelType;
             
-                RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult);
+                RewardBoundedMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult);
 
                 virtual ~RewardBoundedMdpPcaaWeightVectorChecker();
 

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

@@ -18,8 +18,8 @@ namespace storm {
             
             
             template <class SparseModelType, typename GeometryValueType>
-            SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
-                STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
+            SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::SparsePcaaAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+                STORM_LOG_ASSERT(preprocessorResult.queryType==preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
                 initializeThresholdData();
                 
                 // Set the precision of the weight vector checker. Will be refined during the computation

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

@@ -23,7 +23,7 @@ namespace storm {
                  * Creates a new query for the Pareto curve approximation algorithm (Pcaa)
                  * @param preprocessorResult the result from preprocessing
                  */
-                SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
+                SparsePcaaAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
                 
                 virtual ~SparsePcaaAchievabilityQuery() = default;
 

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

@@ -14,8 +14,8 @@ namespace storm {
         namespace multiobjective {
             
             template <class SparseModelType, typename GeometryValueType>
-            SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
-                STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, "Invalid query Type");
+            SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::SparsePcaaParetoQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+                STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, "Invalid query Type");
             }
             
             template <class SparseModelType, typename GeometryValueType>

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

@@ -23,7 +23,7 @@ namespace storm {
                  * Creates a new query for the Pareto curve approximation algorithm (Pcaa)
                  * @param preprocessorResult the result from preprocessing
                  */
-                SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
+                SparsePcaaParetoQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
                 
                 virtual ~SparsePcaaParetoQuery() = default;
 

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

@@ -18,8 +18,8 @@ namespace storm {
             
             
             template <class SparseModelType, typename GeometryValueType>
-            SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
-                STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative, "Invalid query Type");
+            SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::SparsePcaaQuantitativeQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+                STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative, "Invalid query Type");
                 
                 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                     if (!this->objectives[objIndex].formula->hasBound()) {

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

@@ -23,7 +23,7 @@ namespace storm {
                  * Creates a new query for the Pareto curve approximation algorithm (Pcaa)
                  * @param preprocessorResult the result from preprocessing
                  */
-                SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
+                SparsePcaaQuantitativeQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
                 
                 virtual ~SparsePcaaQuantitativeQuery() = default;
 

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

@@ -19,7 +19,7 @@ namespace storm {
             
             
             template <class SparseModelType, typename GeometryValueType>
-            SparsePcaaQuery<SparseModelType, GeometryValueType>::SparsePcaaQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) :
+            SparsePcaaQuery<SparseModelType, GeometryValueType>::SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) :
                 originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), objectives(preprocessorResult.objectives) {
 
                 this->weightVectorChecker = WeightVectorCheckerFactory<SparseModelType>::create(preprocessorResult);

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

@@ -2,7 +2,7 @@
 #define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_
 
 #include "storm/modelchecker/results/CheckResult.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
 #include "storm/storage/geometry/Polytope.h"
 
@@ -55,7 +55,7 @@ namespace storm {
                  * Creates a new query for the Pareto curve approximation algorithm (Pcaa)
                  * @param preprocessorResult the result from preprocessing
                  */
-                SparsePcaaQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
+                SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
                 
                 /*
                  * Returns a weight vector w that separates the under approximation from the given point p, i.e.,

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

@@ -23,7 +23,7 @@ namespace storm {
             
             
             template <class SparseMaModelType>
-            StandardMaPcaaWeightVectorChecker<SparseMaModelType>::StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMaModelType> const& preprocessorResult) :
+            StandardMaPcaaWeightVectorChecker<SparseMaModelType>::StandardMaPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMaModelType> const& preprocessorResult) :
             StandardPcaaWeightVectorChecker<SparseMaModelType>(preprocessorResult) {
                 this->initialize(preprocessorResult);
             }

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

@@ -24,7 +24,7 @@ namespace storm {
             public:
                 typedef typename SparseMaModelType::ValueType ValueType;
                 
-                StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMaModelType> const& preprocessorResult);
+                StandardMaPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMaModelType> const& preprocessorResult);
                 
                 virtual ~StandardMaPcaaWeightVectorChecker() = default;
 

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

@@ -21,7 +21,7 @@ namespace storm {
         namespace multiobjective {
             
             template <class SparseMdpModelType>
-            StandardMdpPcaaWeightVectorChecker<SparseMdpModelType>::StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) :
+            StandardMdpPcaaWeightVectorChecker<SparseMdpModelType>::StandardMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) :
                 StandardPcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult) {
                 this->initialize(preprocessorResult);
             }

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

@@ -32,7 +32,7 @@ namespace storm {
                  *
                  */
                 
-                StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult);
+                StandardMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult);
 
                 virtual ~StandardMdpPcaaWeightVectorChecker() = default;
 

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

@@ -10,6 +10,7 @@
 #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
 #include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
 #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/macros.h"
@@ -29,28 +30,29 @@ namespace storm {
             
 
             template <class SparseModelType>
-            StandardPcaaWeightVectorChecker<SparseModelType>::StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) :
+            StandardPcaaWeightVectorChecker<SparseModelType>::StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) :
                     PcaaWeightVectorChecker<SparseModelType>(preprocessorResult.objectives) {
+                // Intantionally left empty
+            }
             
-                STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult<SparseModelType>::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
-                STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
+            template <class SparseModelType>
+            void StandardPcaaWeightVectorChecker<SparseModelType>::initialize(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) {
+                auto rewardAnalysis = preprocessing::SparseMultiObjectiveRewardAnalysis<SparseModelType>::analyze(preprocessorResult);
+                STORM_LOG_THROW(rewardAnalysis.rewardFinitenessType != preprocessing::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
+                STORM_LOG_THROW(rewardAnalysis.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
                 STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
                 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
 
-            }
-            
-            template <class SparseModelType>
-            void StandardPcaaWeightVectorChecker<SparseModelType>::initialize(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult) {
                 // 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());
+                storm::storage::BitVector maybeStates = rewardAnalysis.rewardLessInfinityEStates.get() & ~rewardAnalysis.reward0AStates;
+                storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(rewardAnalysis.rewardLessInfinityEStates.get(), rewardAnalysis.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()), finiteRewardChoices);
+                auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.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);
@@ -58,7 +60,7 @@ namespace storm {
                 // Initilize general data of the model
                 transitionMatrix = std::move(mergerResult.model->getTransitionMatrix());
                 initialState = *mergerResult.model->getInitialStates().begin();
-                reward0EStates = preprocessorResult.reward0EStates % maybeStates;
+                reward0EStates = rewardAnalysis.reward0EStates % maybeStates;
                 if (mergerResult.targetState) {
                     // There is an additional state in the result
                     reward0EStates.resize(reward0EStates.size() + 1, true);

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

@@ -7,7 +7,7 @@
 #include "storm/transformer/EndComponentEliminator.h"
 #include "storm/modelchecker/multiobjective/Objective.h"
 #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
+#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 #include "storm/utility/vector.h"
 
 namespace storm {
@@ -35,7 +35,7 @@ namespace storm {
                  *
                  */
                 
-                StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
+                StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
                 
                 /*!
                  * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives
@@ -63,7 +63,7 @@ namespace storm {
                 
             protected:
                 
-                void initialize(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
+                void initialize(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
                 virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0;
 
                 /*!