Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MultiObjectiveModelChecking.cpp
Go to the documentation of this file.
1#include "storm/modelchecker/multiobjective/MultiObjectiveModelChecking.h"
2
3#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
4#include "storm/exceptions/InvalidArgumentException.h"
5#include "storm/exceptions/InvalidEnvironmentException.h"
6#include "storm/exceptions/NotImplementedException.h"
7#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
8#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
9#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h"
10#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h"
11#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
12#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
13#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
14#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h"
15#include "storm/modelchecker/results/CheckResult.h"
16#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
17#include "storm/models/sparse/MarkovAutomaton.h"
18#include "storm/models/sparse/Mdp.h"
19#include "storm/settings/SettingsManager.h"
20#include "storm/settings/modules/CoreSettings.h"
21#include "storm/utility/Stopwatch.h"
22#include "storm/utility/macros.h"
23
24namespace storm {
25namespace modelchecker {
26namespace multiobjective {
27
28template<typename SparseModelType>
29std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment const& env, SparseModelType const& model,
30 storm::logic::MultiObjectiveFormula const& formula, bool produceScheduler) {
31 storm::utility::Stopwatch swTotal(true);
32 storm::utility::Stopwatch swPreprocessing(true);
33 STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1,
34 "Multi-objective Model checking on model with multiple initial states is not supported.");
35
36 // If we consider an MA, ensure that it is closed
37 if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
38 STORM_LOG_THROW(dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const*>(&model)->isClosed(),
39 storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton.");
40 }
41
42 // Preprocess the model
43 auto preprocessorResult = preprocessing::SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(env, model, formula, produceScheduler);
44 swPreprocessing.stop();
45 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
46 STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds.\n"
47 << " Result: " << preprocessorResult << '\n');
48 } else {
49 STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds.\n"
50 << " Result: " << preprocessorResult << '\n');
51 }
52
53 // Invoke the analysis
54 storm::utility::Stopwatch swAnalysis(true);
55 std::unique_ptr<CheckResult> result;
56 MultiObjectiveMethod method = env.modelchecker().multi().getMethod();
57 switch (method) {
58 case MultiObjectiveMethod::Pcaa: {
59 if (env.modelchecker().multi().isSchedulerRestrictionSet()) {
60 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException,
61 "Scheduler computation is not implement for queries with restricted scheduler classes.");
62 if (preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability ||
63 preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative) {
64 auto achChecker = DeterministicSchedsAchievabilityChecker<SparseModelType, storm::RationalNumber>(preprocessorResult);
65 result = achChecker.check(env);
66 } else {
67 STORM_LOG_THROW(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto,
68 storm::exceptions::NotImplementedException, "The query type is not implemented with scheduler restrictions.");
69 auto explorer = DeterministicSchedsParetoExplorer<SparseModelType, storm::RationalNumber>(preprocessorResult);
70 result = explorer.check(env);
71 if (env.modelchecker().multi().isExportPlotSet()) {
72 explorer.exportPlotOfCurrentApproximation(env);
73 }
74 }
75 } else {
76 std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query;
77 switch (preprocessorResult.queryType) {
78 case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
79 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
80 new SparsePcaaAchievabilityQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
81 break;
82 case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative:
83 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
84 new SparsePcaaQuantitativeQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
85 break;
86 case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto:
87 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
88 new SparsePcaaParetoQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
89 break;
90 default:
91 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException,
92 "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'.");
93 break;
94 }
95
96 result = query->check(env, produceScheduler);
97 if (produceScheduler) {
98 STORM_LOG_THROW(result->isExplicitParetoCurveCheckResult(), storm::exceptions::UnexpectedException,
99 "Scheduler computation is not implement for the produced result type.");
100 auto& paretoRes = result->template asExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>();
101 STORM_LOG_ASSERT(paretoRes.hasScheduler(), "Scheduler requested but none was produced.");
102 if (preprocessorResult.memoryIncorporationReverseData) {
103 // we have information to post-process schedulers
104 transformObjectiveSchedulersToOriginal(preprocessorResult.memoryIncorporationReverseData.value(), paretoRes.getSchedulers());
105 }
106 }
107
108 if (env.modelchecker().multi().isExportPlotSet()) {
109 query->exportPlotOfCurrentApproximation(env);
110 }
111 }
112 break;
113 }
114 case MultiObjectiveMethod::ConstraintBased: {
115 STORM_LOG_THROW(!env.modelchecker().multi().isSchedulerRestrictionSet(), storm::exceptions::InvalidEnvironmentException,
116 "The selected multi-objective model checking method does not support scheduler restrictions.");
117 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException,
118 "Scheduler computation is not implement for constraint-based multi objective solving.");
119 std::unique_ptr<SparseCbQuery<SparseModelType>> query;
120 switch (preprocessorResult.queryType) {
121 case preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
122 query = std::unique_ptr<SparseCbQuery<SparseModelType>>(new SparseCbAchievabilityQuery<SparseModelType>(preprocessorResult));
123 break;
124 default:
125 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException,
126 "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'.");
127 break;
128 }
129
130 result = query->check(env);
131
132 if (env.modelchecker().multi().isExportPlotSet()) {
133 STORM_LOG_ERROR("Can not export plot for the constrained based solver.");
134 }
135 break;
136 }
137 default:
138 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException,
139 "The multi-objective solution method '" << toString(method) << "' is not supported.");
140 }
141 swAnalysis.stop();
142
143 swTotal.stop();
144 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
145 STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing
146 << " seconds for preprocessing and " << swAnalysis
147 << " seconds for analyzing the preprocessed model).\n");
148 }
149
150 return result;
151}
152
153template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<double>>(Environment const& env,
154 storm::models::sparse::Mdp<double> const& model,
155 storm::logic::MultiObjectiveFormula const& formula,
156 bool produceScheduler);
157template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<double>>(
158 Environment const& env, storm::models::sparse::MarkovAutomaton<double> const& model, storm::logic::MultiObjectiveFormula const& formula,
159 bool produceScheduler);
160template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::Mdp<storm::RationalNumber>>(
161 Environment const& env, storm::models::sparse::Mdp<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula,
162 bool produceScheduler);
163template std::unique_ptr<CheckResult> performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(
164 Environment const& env, storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, storm::logic::MultiObjectiveFormula const& formula,
165 bool produceScheduler);
166
167} // namespace multiobjective
168} // namespace modelchecker
169} // namespace storm
storm::Environment::modelchecker
ModelCheckerEnvironment & modelchecker()
Definition Environment.cpp:33
storm::ModelCheckerEnvironment::multi
MultiObjectiveModelCheckerEnvironment & multi()
Definition ModelCheckerEnvironment.cpp:46
storm::MultiObjectiveModelCheckerEnvironment::getMethod
storm::modelchecker::multiobjective::MultiObjectiveMethod const & getMethod() const
Definition MultiObjectiveModelCheckerEnvironment.cpp:58
storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor::preprocess
static ReturnType preprocess(Environment const &env, SparseModelType const &originalModel, storm::logic::MultiObjectiveFormula const &originalFormula, bool produceScheduler)
Preprocesses the given model w.r.t.
Definition SparseMultiObjectivePreprocessor.cpp:34
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:14
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::utility::Stopwatch
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
storm::utility::Stopwatch::stop
void stop()
Stop stopwatch and add measured time to total time.
Definition Stopwatch.cpp:42
STORM_LOG_INFO
#define STORM_LOG_INFO(message)
Definition logging.h:24
STORM_LOG_ERROR
#define STORM_LOG_ERROR(message)
Definition logging.h:26
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
STORM_PRINT_AND_LOG
#define STORM_PRINT_AND_LOG(message)
Definition macros.h:68
storm::modelchecker::multiobjective::transformObjectiveSchedulersToOriginal
void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const &reverseData, std::vector< storm::storage::Scheduler< ValueType > > &schedulers)
Definition MultiObjectivePostprocessing.cpp:74
storm::modelchecker::multiobjective::performMultiObjectiveModelChecking
std::unique_ptr< CheckResult > performMultiObjectiveModelChecking(Environment const &env, SparseModelType const &model, storm::logic::MultiObjectiveFormula const &formula, bool produceScheduler)
Definition MultiObjectiveModelChecking.cpp:29