35 "Multi-objective Model checking on model with multiple initial states is not supported.");
40 storm::exceptions::InvalidArgumentException,
"Unable to check multi-objective formula on non-closed Markov automaton.");
45 swPreprocessing.
stop();
46 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
48 <<
" Result: " << preprocessorResult <<
'\n');
50 STORM_LOG_INFO(
"Preprocessing done in " << swPreprocessing <<
" seconds.\n"
51 <<
" Result: " << preprocessorResult <<
'\n');
56 std::unique_ptr<CheckResult> result;
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);
69 storm::exceptions::NotImplementedException,
"The query type is not implemented with scheduler restrictions.");
71 result = explorer.check(env);
73 explorer.exportPlotOfCurrentApproximation(env);
77 std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query;
78 switch (preprocessorResult.queryType) {
80 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
84 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
88 query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>>(
93 "The multi-objective query type is not supported for the selected solution method '" <<
toString(method) <<
"'.");
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) {
110 query->exportPlotOfCurrentApproximation(env);
115 case MultiObjectiveMethod::ConstraintBased: {
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) {
127 "The multi-objective query type is not supported for the selected solution method '" <<
toString(method) <<
"'.");
131 result = query->check(env);
134 STORM_LOG_ERROR(
"Can not export plot for the constrained based solver.");
140 "The multi-objective solution method '" <<
toString(method) <<
"' is not supported.");
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");