diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 5a65bd502..7e95c1073 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -26,8 +26,8 @@ namespace storm { template - SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : SparseCbQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult::QueryType::Achievability, "Invalid query Type"); + SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : SparseCbQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Achievability, "Invalid query Type"); solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); } diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h index 215555835..f563ab921 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h @@ -19,7 +19,7 @@ namespace storm { typedef typename SparseModelType::ValueType ValueType; - SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + SparseCbAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual ~SparseCbAchievabilityQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp index 1494f5281..7d2d680a8 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp +++ b/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 - SparseCbQuery::SparseCbQuery(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + SparseCbQuery::SparseCbQuery(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), objectives(std::move(preprocessorResult.objectives)) { - STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult::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::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 relevantRewardModels; for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(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); diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h index 1e7f0879a..0a3c51529 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h @@ -3,7 +3,7 @@ #include #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 const& preprocessorResult); + SparseCbQuery(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); SparseModelType const& originalModel; storm::logic::MultiObjectiveFormula const& originalFormula; diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index bb18e9385..f85f7caf4 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/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 - std::unique_ptr performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection) { + std::unique_ptr 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::preprocess(model, formula); + auto preprocessorResult = preprocessing::SparseMultiObjectivePreprocessor::preprocess(model, formula); swPreprocessing.stop(); if (storm::settings::getModule().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().getMultiObjectiveMethod(); - } else { - method = convert(methodSelection); - } // Invoke the analysis storm::utility::Stopwatch swAnalysis(true); std::unique_ptr result; + MultiObjectiveMethod method = env.modelchecker().multi().getMethod(); switch (method) { case MultiObjectiveMethod::Pcaa: { std::unique_ptr> query; switch (preprocessorResult.queryType) { - case SparseMultiObjectivePreprocessorResult::QueryType::Achievability: + case preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Achievability: query = std::unique_ptr> (new SparsePcaaAchievabilityQuery(preprocessorResult)); break; - case SparseMultiObjectivePreprocessorResult::QueryType::Quantitative: + case preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Quantitative: query = std::unique_ptr> (new SparsePcaaQuantitativeQuery(preprocessorResult)); break; - case SparseMultiObjectivePreprocessorResult::QueryType::Pareto: + case preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Pareto: query = std::unique_ptr> (new SparsePcaaParetoQuery(preprocessorResult)); break; default: @@ -83,7 +76,7 @@ namespace storm { { std::unique_ptr> query; switch (preprocessorResult.queryType) { - case SparseMultiObjectivePreprocessorResult::QueryType::Achievability: + case preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Achievability: query = std::unique_ptr> (new SparseCbAchievabilityQuery(preprocessorResult)); break; default: @@ -93,7 +86,7 @@ namespace storm { result = query->check(env); - if(storm::settings::getModule().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 performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); - template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula); + template std::unique_ptr performMultiObjectiveModelChecking>(Environment const& env, storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); } } diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h index be0a7ef6e..868ba2a61 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h @@ -15,7 +15,7 @@ namespace storm { template - std::unique_ptr performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS); + std::unique_ptr performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp index 06e4cb85d..10a9554f2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp @@ -53,7 +53,7 @@ namespace storm { template template>::value, int>::type> - std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { + std::unique_ptr> WeightVectorCheckerFactory::create(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) { if (preprocessorResult.containsOnlyTrivialObjectives()) { return std::make_unique>(preprocessorResult); } else { @@ -64,7 +64,7 @@ namespace storm { template template>::value, int>::type> - std::unique_ptr> WeightVectorCheckerFactory::create(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { + std::unique_ptr> WeightVectorCheckerFactory::create(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) { return std::make_unique>(preprocessorResult); } @@ -78,10 +78,10 @@ namespace storm { template class WeightVectorCheckerFactory>; template class WeightVectorCheckerFactory>; - template std::unique_ptr>> WeightVectorCheckerFactory>::create(SparseMultiObjectivePreprocessorResult> const& preprocessorResult); - template std::unique_ptr>> WeightVectorCheckerFactory>::create(SparseMultiObjectivePreprocessorResult> const& preprocessorResult); - template std::unique_ptr>> WeightVectorCheckerFactory>::create(SparseMultiObjectivePreprocessorResult> const& preprocessorResult); - template std::unique_ptr>> WeightVectorCheckerFactory>::create(SparseMultiObjectivePreprocessorResult> const& preprocessorResult); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(preprocessing::SparseMultiObjectivePreprocessorResult> const& preprocessorResult); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(preprocessing::SparseMultiObjectivePreprocessorResult> const& preprocessorResult); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(preprocessing::SparseMultiObjectivePreprocessorResult> const& preprocessorResult); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(preprocessing::SparseMultiObjectivePreprocessorResult> const& preprocessorResult); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h index 4bdbe3dc3..0930af29c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h +++ b/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>::value, int>::type = 0> - static std::unique_ptr> create(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + static std::unique_ptr> create(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); template>::value, int>::type = 0> - static std::unique_ptr> create(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + static std::unique_ptr> create(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); }; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index f5137b0a7..ad70f9120 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/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 - RewardBoundedMdpPcaaWeightVectorChecker::RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) { + RewardBoundedMdpPcaaWeightVectorChecker::RewardBoundedMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) { - STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); + auto rewardAnalysis = preprocessing::SparseMultiObjectiveRewardAnalysis::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 diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h index 0013cdc3d..a7bf6c999 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h +++ b/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 const& preprocessorResult); + RewardBoundedMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual ~RewardBoundedMdpPcaaWeightVectorChecker(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index b8ac5fe2d..8f81dab76 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -18,8 +18,8 @@ namespace storm { template - SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult::QueryType::Achievability, "Invalid query Type"); + SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Achievability, "Invalid query Type"); initializeThresholdData(); // Set the precision of the weight vector checker. Will be refined during the computation diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h index c5f3ae1a6..aac980af8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h +++ b/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& preprocessorResult); + SparsePcaaAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); virtual ~SparsePcaaAchievabilityQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 93c04e527..efe7a42f9 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -14,8 +14,8 @@ namespace storm { namespace multiobjective { template - SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult::QueryType::Pareto, "Invalid query Type"); + SparsePcaaParetoQuery::SparsePcaaParetoQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Pareto, "Invalid query Type"); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index 5208f00cd..66c0fdb8e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/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& preprocessorResult); + SparsePcaaParetoQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); virtual ~SparsePcaaParetoQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 4df353cdd..afffc1f92 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -18,8 +18,8 @@ namespace storm { template - SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult::QueryType::Quantitative, "Invalid query Type"); + SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Quantitative, "Invalid query Type"); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { if (!this->objectives[objIndex].formula->hasBound()) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index 234e6f291..2244ca594 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/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& preprocessorResult); + SparsePcaaQuantitativeQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); virtual ~SparsePcaaQuantitativeQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index ef7e50d80..5f127579f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -19,7 +19,7 @@ namespace storm { template - SparsePcaaQuery::SparsePcaaQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : + SparsePcaaQuery::SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), objectives(preprocessorResult.objectives) { this->weightVectorChecker = WeightVectorCheckerFactory::create(preprocessorResult); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index 630503a08..b466241ae 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/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& preprocessorResult); + SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); /* * Returns a weight vector w that separates the under approximation from the given point p, i.e., diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index d43db0d5c..f5980166c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -23,7 +23,7 @@ namespace storm { template - StandardMaPcaaWeightVectorChecker::StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardMaPcaaWeightVectorChecker::StandardMaPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : StandardPcaaWeightVectorChecker(preprocessorResult) { this->initialize(preprocessorResult); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h index db62018d2..ee21f1b28 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h @@ -24,7 +24,7 @@ namespace storm { public: typedef typename SparseMaModelType::ValueType ValueType; - StandardMaPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + StandardMaPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual ~StandardMaPcaaWeightVectorChecker() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp index f744b0cee..96a7e1de6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.cpp @@ -21,7 +21,7 @@ namespace storm { namespace multiobjective { template - StandardMdpPcaaWeightVectorChecker::StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardMdpPcaaWeightVectorChecker::StandardMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : StandardPcaaWeightVectorChecker(preprocessorResult) { this->initialize(preprocessorResult); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h index 071f168a2..2482d0829 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h @@ -32,7 +32,7 @@ namespace storm { * */ - StandardMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); + StandardMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual ~StandardMdpPcaaWeightVectorChecker() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 3dd8e8988..23b256306 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/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 - StandardPcaaWeightVectorChecker::StandardPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult) : + StandardPcaaWeightVectorChecker::StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) : PcaaWeightVectorChecker(preprocessorResult.objectives) { - - STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult::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."); - 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."); - + // Intantionally left empty } template - void StandardPcaaWeightVectorChecker::initialize(SparseMultiObjectivePreprocessorResult const& preprocessorResult) { + void StandardPcaaWeightVectorChecker::initialize(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult) { + auto rewardAnalysis = preprocessing::SparseMultiObjectiveRewardAnalysis::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."); + // 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 relevantRewardModels; for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices); + auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(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); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index b28a80ac6..70da1049b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/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 const& preprocessorResult); + StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult 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 const& preprocessorResult); + void initialize(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; /*!