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