Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
model-handling.h
Go to the documentation of this file.
1#pragma once
2
3#include "storm/api/storm.h"
4
9
10#include "AutomaticSettings.h"
11#include "storm/io/file.h"
16
19
20#include <filesystem>
21#include <type_traits>
22
25
27
29
31
33
37
41
53#include "storm/storage/Qvbs.h"
56
58
59namespace storm {
60namespace cli {
61
63 // The symbolic model description.
64 boost::optional<storm::storage::SymbolicModelDescription> model;
65
66 // The original properties to check.
67 std::vector<storm::jani::Property> properties;
68
69 // The preprocessed properties to check (in case they needed amendment).
70 boost::optional<std::vector<storm::jani::Property>> preprocessedProperties;
71};
72
74 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
75 if (ioSettings.isPrismOrJaniInputSet()) {
76 storm::utility::Stopwatch modelParsingWatch(true);
77 if (ioSettings.isPrismInputSet()) {
78 input.model =
79 storm::api::parseProgram(ioSettings.getPrismInputFilename(), buildSettings.isPrismCompatibilityEnabled(), !buildSettings.isNoSimplifySet());
80 } else {
81 boost::optional<std::vector<std::string>> propertyFilter;
82 if (ioSettings.isJaniPropertiesSet()) {
83 if (ioSettings.areJaniPropertiesSelected()) {
84 propertyFilter = ioSettings.getSelectedJaniProperties();
85 } else {
86 propertyFilter = boost::none;
87 }
88 } else {
89 propertyFilter = std::vector<std::string>();
90 }
91 auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), propertyFilter);
92 input.model = std::move(janiInput.first);
93 if (ioSettings.isJaniPropertiesSet()) {
94 input.properties = std::move(janiInput.second);
95 }
96 }
97 modelParsingWatch.stop();
98 STORM_PRINT("Time for model input parsing: " << modelParsingWatch << ".\n\n");
99 }
100}
101
103 boost::optional<std::set<std::string>> const& propertyFilter) {
104 if (ioSettings.isPropertySet()) {
105 std::vector<storm::jani::Property> newProperties;
106 if (input.model) {
107 newProperties = storm::api::parsePropertiesForSymbolicModelDescription(ioSettings.getProperty(), input.model.get(), propertyFilter);
108 } else {
109 newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter);
110 }
111
112 input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end());
113 }
114}
115
117 // Parse the model input
118 SymbolicInput input;
119 storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName());
120 STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter()));
121 storm::utility::Stopwatch modelParsingWatch(true);
122 auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), ioSettings.getQvbsPropertyFilter());
123 input.model = std::move(janiInput.first);
124 input.properties = std::move(janiInput.second);
125 modelParsingWatch.stop();
126 STORM_PRINT("Time for model input parsing: " << modelParsingWatch << ".\n\n");
127
128 // Parse additional properties
129 boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
130 parseProperties(ioSettings, input, propertyFilter);
131
132 // Substitute constant definitions
133 auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex()));
134 input.model = input.model.get().preprocess(constantDefinitions);
135 if (!input.properties.empty()) {
136 input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions);
137 }
138
139 return input;
140}
141
143 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
144 if (ioSettings.isQvbsInputSet()) {
145 return parseSymbolicInputQvbs(ioSettings);
146 } else {
147 // Parse the property filter, if any is given.
148 boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
149
150 SymbolicInput input;
151 parseSymbolicModelDescription(ioSettings, input);
152 parseProperties(ioSettings, input, propertyFilter);
153 return input;
154 }
155}
156
158 // The engine to use
160
161 // If set, bisimulation will be applied.
163
164 // If set, a transformation to Jani will be enforced
166
167 // Which data type is to be used for numbers ...
169 ValueType buildValueType; // ... during model building
170 ValueType verificationValueType; // ... during model verification
171
172 // The Dd library to be used
174
175 // The environment used during model checking
177
178 // A flag which is set to true, if the settings were detected to be compatible.
179 // If this is false, it could be that the query can not be handled.
181};
182
184 auto hints = storm::settings::getModule<storm::settings::modules::HintSettings>();
185
186 STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model.");
187 STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model.");
188 std::vector<storm::jani::Property> const& properties =
189 input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties;
190 STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a property.");
191 STORM_LOG_WARN_COND(properties.size() == 1,
192 "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered.");
193
195 if (hints.isNumberStatesSet()) {
196 as.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates());
197 } else {
198 as.predict(input.model->asJaniModel(), properties.front());
199 }
200
201 mpi.engine = as.getEngine();
202 if (as.enableBisimulation()) {
203 mpi.applyBisimulation = true;
204 }
207 }
208 STORM_PRINT_AND_LOG("Automatic engine picked the following settings: \n"
209 << "\tengine=" << mpi.engine << std::boolalpha << "\t bisimulation=" << mpi.applyBisimulation
210 << "\t exact=" << (mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision) << std::noboolalpha << '\n');
211}
212
219 std::shared_ptr<SymbolicInput> const& transformedJaniInput = nullptr) {
221 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
222 auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
223 auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
224 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
225
226 // Set the engine.
227 mpi.engine = coreSettings.getEngine();
228
229 // Set whether bisimulation is to be used.
230 mpi.applyBisimulation = generalSettings.isBisimulationSet();
231
232 // Set the value type used for numeric values
233 if (generalSettings.isParametricSet()) {
235 } else if (generalSettings.isExactSet()) {
237 } else {
239 }
240 auto originalVerificationValueType = mpi.verificationValueType;
241
242 // Since the remaining settings could depend on the ones above, we need apply the automatic engine now.
243 bool useAutomatic = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Automatic;
244 if (useAutomatic) {
245 if (input.model->isJaniModel()) {
246 // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable
247 // bisimulation or disable exact arithmetic)
249 } else {
250 // Transform Prism to jani first
251 STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input.");
252 SymbolicInput janiInput;
253 janiInput.properties = input.properties;
254 storm::prism::Program const& prog = input.model.get().asPrismProgram();
255 auto modelAndProperties = prog.toJani(input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties);
256 janiInput.model = modelAndProperties.first;
257 if (!modelAndProperties.second.empty()) {
258 janiInput.preprocessedProperties = std::move(modelAndProperties.second);
259 }
260 // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable
261 // bisimulation or disable exact arithmetic)
263 if (transformedJaniInput) {
264 // We cache the transformation result.
265 *transformedJaniInput = std::move(janiInput);
266 }
267 }
268 }
269
270 // Check whether these settings are compatible with the provided input.
271 if (input.model) {
272 auto checkCompatibleSettings = [&mpi, &input] {
273 switch (mpi.verificationValueType) {
276 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
279 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
280 break;
283 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
284 }
285 return false;
286 };
287 mpi.isCompatible = checkCompatibleSettings();
288 if (!mpi.isCompatible) {
289 if (useAutomatic) {
291 STORM_LOG_WARN("The settings picked by the automatic engine (engine="
292 << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact
293 << ") are incompatible with this model. Falling back to default settings.");
295 mpi.applyBisimulation = false;
296 mpi.verificationValueType = originalVerificationValueType;
297 // Retry check with new settings
298 mpi.isCompatible = checkCompatibleSettings();
299 }
300 }
301 } else {
302 // If there is no input model, nothing has to be done, actually
303 mpi.isCompatible = true;
304 }
305
306 // Set whether a transformation to jani is required or necessary
307 mpi.transformToJani = ioSettings.isPrismToJaniSet();
308 if (input.model) {
309 auto builderType = storm::utility::getBuilderType(mpi.engine);
310 bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) &&
311 (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA) && (!input.model->isJaniModel());
312 STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA,
313 "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.");
314 mpi.transformToJani |= transformToJaniForDdMA;
315 }
316
317 // Set the Valuetype used during model building
319 if (bisimulationSettings.useExactArithmeticInDdBisimulation()) {
323 }
324 } else {
325 STORM_LOG_WARN("Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied.");
326 }
327 }
328
329 // Set the Dd library
330 mpi.ddType = coreSettings.getDdLibraryType();
331 if (mpi.ddType == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue()) {
334 STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
336 }
337 }
338 return mpi;
339}
340
341auto castAndApply(std::shared_ptr<storm::models::ModelBase> const& model, auto const& callback) {
342 STORM_LOG_ASSERT(model, "Tried to cast a model that does not exist.");
343
344 // Helper to actually perform the cast once value type and model representation type is known
345 auto castAndApplyImpl = [&model, &callback]<typename TargetModelType> {
346 auto res = model->template as<TargetModelType>();
347 STORM_LOG_ASSERT(res, "Casting model pointer failed unexpectedly.");
348 return callback(res);
349 };
350
351 // Helper to branch on type of model representation
352 auto castAndApplyVT = [&]<typename ValueType> {
353 if (model->isSparseModel()) {
354 return castAndApplyImpl.template operator()<storm::models::sparse::Model<ValueType>>();
355 } else {
356 auto ddType = model->getDdType();
357 STORM_LOG_ASSERT(model->isSymbolicModel() && ddType.has_value(), "Unexpected model representation");
358 if constexpr (storm::IsIntervalType<ValueType>) {
359 // Avoiding a couple of unnecessary template instantiations
360 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Symbolic interval models are currently not supported.");
361 } else {
362 using enum storm::dd::DdType;
363 if (*ddType == CUDD) {
364 if constexpr (std::is_same_v<ValueType, double>) {
365 return castAndApplyImpl.template operator()<storm::models::symbolic::Model<CUDD, ValueType>>();
366 }
367 }
368 STORM_LOG_ASSERT(*ddType == Sylvan, "Unexpected Dd type");
369 return castAndApplyImpl.template operator()<storm::models::symbolic::Model<Sylvan, ValueType>>();
370 }
371 }
372 };
373
374 // branch on type of value representation
375 if (model->supportsParameters()) {
376 return castAndApplyVT.template operator()<storm::RationalFunction>();
377 } else if (model->isExact()) {
378 return castAndApplyVT.template operator()<storm::RationalNumber>();
379 } else if (model->supportsUncertainty()) {
380 return castAndApplyVT.template operator()<storm::Interval>();
381 } else {
382 return castAndApplyVT.template operator()<double>();
383 }
384}
385
388 switch (vt) {
389 case FinitePrecision:
390 return callback.template operator()<double>();
391 case Exact:
392 return callback.template operator()<storm::RationalNumber>();
393 case Parametric:
394 return callback.template operator()<storm::RationalFunction>();
395 }
396 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected value type.");
397}
398
400 using enum storm::dd::DdType;
402 switch (dd) {
403 case CUDD:
404 STORM_LOG_THROW(vt == FinitePrecision, storm::exceptions::UnexpectedException, "Unexpected value type for DD library Cudd.");
405 return callback.template operator()<CUDD, double>();
406 case Sylvan:
407 switch (vt) {
408 case FinitePrecision:
409 return callback.template operator()<Sylvan, double>();
410 case Exact:
411 return callback.template operator()<Sylvan, storm::RationalNumber>();
412 case Parametric:
413 return callback.template operator()<Sylvan, storm::RationalFunction>();
414 }
415 }
416 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected DDType or value type.");
417}
418
419inline void ensureNoUndefinedPropertyConstants(std::vector<storm::jani::Property> const& properties) {
420 // Make sure there are no undefined constants remaining in any property.
421 for (auto const& property : properties) {
422 std::set<storm::expressions::Variable> usedUndefinedConstants = property.getUndefinedConstants();
423 if (!usedUndefinedConstants.empty()) {
424 std::vector<std::string> undefinedConstantsNames;
425 for (auto const& constant : usedUndefinedConstants) {
426 undefinedConstantsNames.emplace_back(constant.getName());
427 }
429 false, storm::exceptions::InvalidArgumentException,
430 "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << ".");
431 }
432 }
433}
434
435inline std::pair<SymbolicInput, ModelProcessingInformation> preprocessSymbolicInput(SymbolicInput const& input) {
436 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
437
438 SymbolicInput output = input;
439
440 // Preprocess properties (if requested)
441 if (ioSettings.isPropertiesAsMultiSet()) {
442 STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException,
443 "Can not translate properties to multi-objective formula because no properties were specified.");
445 }
446
447 // Substitute constant definitions in symbolic input.
448 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
449 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
450 if (output.model) {
451 constantDefinitions = output.model.get().parseConstantDefinitions(constantDefinitionString);
452 output.model = output.model.get().preprocess(constantDefinitions);
453 }
454 if (!output.properties.empty()) {
455 output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
456 }
458 auto transformedJani = std::make_shared<SymbolicInput>();
459 ModelProcessingInformation mpi = getModelProcessingInformation(output, transformedJani);
460
461 // Check whether conversion for PRISM to JANI is requested or necessary.
462 if (output.model && output.model.get().isPrismProgram()) {
463 if (mpi.transformToJani) {
464 if (transformedJani->model) {
465 // Use the cached transformation if possible
466 output = std::move(*transformedJani);
467 } else {
468 storm::prism::Program const& model = output.model.get().asPrismProgram();
469 auto modelAndProperties = model.toJani(output.properties);
470
471 output.model = modelAndProperties.first;
472
473 if (!modelAndProperties.second.empty()) {
474 output.preprocessedProperties = std::move(modelAndProperties.second);
475 }
476 }
477 }
478 }
479
480 if (output.model && output.model.get().isJaniModel()) {
482 storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures);
483
484 const auto& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
485 if (buildSettings.isLocationEliminationSet()) {
486 auto locationHeuristic = buildSettings.getLocationEliminationLocationHeuristic();
487 auto edgesHeuristic = buildSettings.getLocationEliminationEdgesHeuristic();
488 output.model->setModel(storm::jani::JaniLocalEliminator::eliminateAutomatically(output.model.get().asJaniModel(), output.properties,
489 locationHeuristic, edgesHeuristic));
490 }
491 }
492
493 return {output, mpi};
494}
495
496inline void exportSymbolicInput(SymbolicInput const& input) {
497 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
498 if (input.model && input.model.get().isJaniModel()) {
499 storm::storage::SymbolicModelDescription const& model = input.model.get();
500 if (ioSettings.isExportJaniDotSet()) {
501 storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename());
502 }
503 }
504}
505
506inline std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
507 std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);
508
509 for (auto const& property : properties) {
510 if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
511 result.push_back(property.getFilter().getStatesFormula());
512 }
513 }
514
515 return result;
516}
517
518template<storm::dd::DdType DdType, typename ValueType>
519std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
520 if (DdType == storm::dd::DdType::Sylvan) {
521 auto numThreads = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads();
522 STORM_PRINT_AND_LOG("Using Sylvan with " << numThreads << " parallel threads.\n");
523 }
524 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
525 return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(),
526 !buildSettings.isApplyNoMaximumProgressAssumptionSet());
527}
528
530 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
532 options.setBuildChoiceLabels(options.isBuildChoiceLabelsSet() || buildSettings.isBuildChoiceLabelsSet());
533 options.setBuildStateValuations(options.isBuildStateValuationsSet() || buildSettings.isBuildStateValuationsSet());
534 options.setBuildAllLabels(options.isBuildAllLabelsSet() || buildSettings.isBuildAllLabelsSet());
535 options.setBuildObservationValuations(options.isBuildObservationValuationsSet() || buildSettings.isBuildObservationValuationsSet());
536 bool buildChoiceOrigins = options.isBuildChoiceOriginsSet() || buildSettings.isBuildChoiceOriginsSet();
538 auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
539 if (counterexampleGeneratorSettings.isCounterexampleSet()) {
540 buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet();
541 }
542 }
543 options.setBuildChoiceOrigins(buildChoiceOrigins);
544
545 if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) {
547 }
548
549 if (buildSettings.isExplorationChecksSet()) {
550 options.setExplorationChecks();
551 }
552 options.setReservedBitsForUnboundedVariables(buildSettings.getBitsForUnboundedVariables());
553
554 options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet());
555 if (buildSettings.isBuildFullModelSet()) {
556 options.clearTerminalStates();
558 options.setBuildAllLabels(true);
559 options.setBuildAllRewardModels(true);
560 }
561
562 if (buildSettings.isAddOverlappingGuardsLabelSet()) {
563 options.setAddOverlappingGuardsLabel(true);
564 }
565
566 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
567 if (ioSettings.isComputeExpectedVisitingTimesSet() || ioSettings.isComputeSteadyStateDistributionSet()) {
568 options.clearTerminalStates();
569 }
570 return options;
571}
572
573template<typename ValueType>
574std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::builder::BuilderOptions const& options) {
575 // Adapt the ValueType if it does not support intervals and the input is an interval model
576 if (!storm::IsIntervalType<ValueType> && input.model.is_initialized() && input.model->isPrismProgram() &&
577 input.model->asPrismProgram().hasIntervalUpdates()) {
578 STORM_LOG_THROW((std::is_same_v<ValueType, storm::IntervalBaseType<storm::Interval>>), storm::exceptions::NotSupportedException,
579 "Can not build interval model for the provided value type.");
580 return storm::api::buildSparseModel<storm::Interval>(input.model.get(), options);
581 } else {
582 return storm::api::buildSparseModel<ValueType>(input.model.get(), options);
583 }
584}
585
586template<typename ValueType>
587std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings,
588 storm::settings::modules::BuildSettings const& buildSettings) {
589 std::shared_ptr<storm::models::ModelBase> result;
590 if (ioSettings.isExplicitSet()) {
591 result = storm::api::buildExplicitModel<ValueType>(
592 ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(),
593 ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none,
594 ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none,
595 ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
596 } else if (ioSettings.isExplicitDRNSet()) {
598 options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet();
599 result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename(), options);
600 } else {
601 STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
602 result = storm::api::buildExplicitIMCAModel<ValueType>(ioSettings.getExplicitIMCAFilename());
603 }
604 return result;
605}
606
607inline std::shared_ptr<storm::models::ModelBase> buildModel(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings,
608 ModelProcessingInformation const& mpi) {
609 storm::utility::Stopwatch modelBuildingWatch(true);
610
611 std::shared_ptr<storm::models::ModelBase> result;
612 if (input.model) {
613 auto builderType = storm::utility::getBuilderType(mpi.engine);
614 if (builderType == storm::builder::BuilderType::Dd) {
615 result = applyDdLibValueType(mpi.ddType, mpi.buildValueType, [&input]<storm::dd::DdType DD, typename VT>() { return buildModelDd<DD, VT>(input); });
616 } else if (builderType == storm::builder::BuilderType::Explicit) {
617 result = applyValueType(mpi.buildValueType, [&input]<typename VT>() {
618 auto options = createBuildOptionsSparseFromSettings(input);
619 return buildModelSparse<VT>(input, options);
620 });
621 }
622 } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
623 STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException,
624 "Can only use sparse engine with explicit input.");
625 result = applyValueType(mpi.buildValueType, [&ioSettings]<typename VT>() {
626 return buildModelExplicit<VT>(ioSettings, storm::settings::getModule<storm::settings::modules::BuildSettings>());
627 });
628 }
629
630 modelBuildingWatch.stop();
631 if (result) {
632 STORM_PRINT("Time for model construction: " << modelBuildingWatch << ".\n\n");
633 }
634
635 return result;
636}
637
638template<typename ValueType>
639std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovAutomaton(
640 std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& model) {
641 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
642 auto debugSettings = storm::settings::getModule<storm::settings::modules::DebugSettings>();
643
644 std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
645 model->close();
646 STORM_LOG_WARN_COND(!debugSettings.isAdditionalChecksSet() || !model->containsZenoCycle(),
647 "MA contains a Zeno cycle. Model checking results cannot be trusted.");
648
649 if (model->isConvertibleToCtmc()) {
650 STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead.");
651 result = model->convertToCtmc();
652 }
653
654 if (transformationSettings.isChainEliminationSet()) {
655 if constexpr (storm::IsIntervalType<ValueType>) {
656 // Currently not enabling this for interval models, as this would require a number of additional template instantiations.
657 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Chain elimination not supported for interval models.");
658 } else {
659 // TODO: we should also transform the properties at this point.
661 transformationSettings.getLabelBehavior())
662 .first;
663 }
664 }
665
666 return result;
667}
668
669template<typename ValueType>
670std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseModelBisimulation(
671 std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input,
672 storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
674 if (bisimulationSettings.isWeakBisimulationSet()) {
676 }
677
678 STORM_LOG_INFO("Performing bisimulation minimization...");
679 return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
680}
681
682template<typename ValueType>
683std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model,
684 SymbolicInput const& input, ModelProcessingInformation const& mpi) {
685 STORM_LOG_THROW(mpi.buildValueType == mpi.verificationValueType, storm::exceptions::NotSupportedException,
686 "Converting value types for sparse engine is not supported.");
687 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
688 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
689 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
690
691 std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
692
693 if (auto order = transformationSettings.getModelPermutation(); order.has_value()) {
694 auto seed = transformationSettings.getModelPermutationSeed();
695 STORM_PRINT_AND_LOG("Permuting model states using " << storm::utility::permutation::orderKindtoString(order.value()) << " order"
696 << (seed.has_value() ? " with seed " + std::to_string(seed.value()) : "") << ".\n");
697 result.first = storm::api::permuteModelStates(result.first, order.value(), seed);
698 result.second = true;
699 STORM_PRINT_AND_LOG("Transition matrix hash after permuting: " << result.first->getTransitionMatrix().hash() << ".\n");
700 }
701
702 if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
704 result.second = true;
705 }
706
707 if (mpi.applyBisimulation) {
708 if constexpr (storm::IsIntervalType<ValueType>) {
709 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Bisimulation not supported for interval models.");
710 } else {
711 result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
712 result.second = true;
713 }
714 }
715
716 if (transformationSettings.isToDiscreteTimeModelSet()) {
717 if constexpr (storm::IsIntervalType<ValueType>) {
718 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to discrete time model not supported for interval models.");
719 } else {
720 // TODO: we should also transform the properties at this point.
722 !model->hasRewardModel("_time"),
723 "Scheduled transformation to discrete time model, but a reward model named '_time' is already present in this model. We might take "
724 "the wrong reward model later.");
725 result.first =
727 .first;
728 result.second = true;
729 }
730 }
731
732 if (transformationSettings.isToNondeterministicModelSet()) {
733 result.first = storm::api::transformToNondeterministicModel<ValueType>(std::move(*result.first));
734 result.second = true;
735 }
736
737 return result;
738}
739
740template<typename ValueType>
741void exportModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
742 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
743
744 if (ioSettings.isExportBuildSet()) {
745 switch (ioSettings.getExportBuildFormat()) {
747 storm::api::exportSparseModelAsDot(model, ioSettings.getExportBuildFilename(), ioSettings.getExportDotMaxWidth());
748 break;
750 storm::api::exportSparseModelAsDrn(model, ioSettings.getExportBuildFilename(),
751 input.model ? input.model.get().getParameterNames() : std::vector<std::string>(),
752 !ioSettings.isExplicitExportPlaceholdersDisabled());
753 break;
755 storm::api::exportSparseModelAsJson(model, ioSettings.getExportBuildFilename());
756 break;
757 default:
758 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
759 "Exporting sparse models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
760 }
761 }
762
763 // TODO: The following options are depreciated and shall be removed at some point:
764
765 if (ioSettings.isExportExplicitSet()) {
766 storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(),
767 input.model ? input.model.get().getParameterNames() : std::vector<std::string>(),
768 !ioSettings.isExplicitExportPlaceholdersDisabled());
769 }
770
771 if (ioSettings.isExportDdSet()) {
772 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drdd format is only supported for DDs.");
773 }
774
775 if (ioSettings.isExportDotSet()) {
776 storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth());
777 }
778}
779
780template<storm::dd::DdType DdType, typename ValueType>
782 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
783
784 if (ioSettings.isExportBuildSet()) {
785 switch (ioSettings.getExportBuildFormat()) {
787 storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportBuildFilename());
788 break;
790 storm::api::exportSymbolicModelAsDrdd(model, ioSettings.getExportBuildFilename());
791 break;
792 default:
793 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
794 "Exporting symbolic models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
795 }
796 }
797
798 // TODO: The following options are depreciated and shall be removed at some point:
799
800 if (ioSettings.isExportExplicitSet()) {
801 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drn format is only supported for sparse models.");
802 }
803
804 if (ioSettings.isExportDdSet()) {
805 storm::api::exportSymbolicModelAsDrdd(model, ioSettings.getExportDdFilename());
806 }
807
808 if (ioSettings.isExportDotSet()) {
809 storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportDotFilename());
810 }
811}
812
813template<storm::dd::DdType DdType, typename ValueType>
814typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
816 return model;
817}
818
819template<storm::dd::DdType DdType, typename ValueType>
820typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
822 auto ma = model->template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
823 if (!ma->isClosed()) {
824 return std::make_shared<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(ma->close());
825 } else {
826 return model;
827 }
828}
829
830template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
831std::shared_ptr<storm::models::Model<ExportValueType>> preprocessDdModelBisimulation(
832 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input,
833 storm::settings::modules::BisimulationSettings const& bisimulationSettings, ModelProcessingInformation const& mpi) {
834 STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(),
835 "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
836
837 auto quotientFormat = bisimulationSettings.getQuotientFormat();
839 bisimulationSettings.isQuotientFormatSetFromDefaultValue()) {
840 STORM_LOG_INFO("Setting bisimulation quotient format to 'sparse'.");
842 }
843 STORM_LOG_INFO("Performing bisimulation minimization...");
844 return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(
845 model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode(), quotientFormat);
846}
847
848template<typename ExportValueType, storm::dd::DdType DdType, typename ValueType>
849std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModelImpl(
850 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
851 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
852 std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
853
854 if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
855 intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
856 intermediateResult.second = true;
857 }
858
859 std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>> result;
860 auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
861 if (mpi.applyBisimulation) {
862 std::shared_ptr<storm::models::Model<ExportValueType>> newModel =
863 preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings, mpi);
864 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(newModel, true);
865 } else {
866 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(
867 symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
868 }
869
870 if (result && result->first->isSymbolicModel() && mpi.engine == storm::utility::Engine::DdSparse) {
871 // Mark as changed.
872 result->second = true;
873
874 std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel =
875 result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
876 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
877 for (auto const& property : input.properties) {
878 formulas.emplace_back(property.getRawFormula());
879 }
880 result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas);
881 STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
882 }
883
884 return *result;
885}
886
887template<storm::dd::DdType DdType, typename ValueType>
888std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
889 SymbolicInput const& input, ModelProcessingInformation const& mpi) {
890 return applyValueType(mpi.verificationValueType, [&model, &input, &mpi]<typename VT>() -> std::pair<std::shared_ptr<storm::models::ModelBase>, bool> {
891 // To safe a few template instantiations, we only consider those combinations that actually occur in the CLI
892 if constexpr (std::is_same_v<ValueType, VT> ||
893 (DdType == storm::dd::DdType::Sylvan && std::is_same_v<ValueType, storm::RationalNumber> && std::is_same_v<VT, double>)) {
894 return preprocessDdModelImpl<VT>(model, input, mpi);
895 } else {
896 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
897 "Unexpected combination of DD library, build value type, and verification value type.");
898 }
899 });
900}
901
903 STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ...\n");
904}
905
906inline void printCounterexample(std::shared_ptr<storm::counterexamples::Counterexample> const& counterexample, storm::utility::Stopwatch* watch = nullptr) {
907 if (counterexample) {
908 STORM_PRINT(*counterexample << '\n');
909 if (watch) {
910 STORM_PRINT("Time for computation: " << *watch << ".\n");
911 }
912 } else {
913 STORM_PRINT(" failed.\n");
914 }
915}
916
917template<typename ModelType>
918 requires(!std::derived_from<ModelType, storm::models::sparse::Model<double>>)
919inline void generateCounterexamples(std::shared_ptr<ModelType> const&, SymbolicInput const&) {
920 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type.");
921}
922
923template<typename ModelType>
924 requires(std::derived_from<ModelType, storm::models::sparse::Model<double>>)
925inline void generateCounterexamples(std::shared_ptr<ModelType> const& sparseModel, SymbolicInput const& input) {
926 using ValueType = typename ModelType::ValueType;
927
928 for (auto& rewModel : sparseModel->getRewardModels()) {
929 rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(), true);
930 }
931
932 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp),
933 storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models.");
934
935 auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
936 if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
937 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
938 for (auto const& property : input.properties) {
939 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
941 storm::utility::Stopwatch watch(true);
942 if (useMilp) {
943 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException,
944 "Counterexample generation using MILP is currently only supported for MDPs.");
946 input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
947 } else {
948 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp),
949 storm::exceptions::NotSupportedException,
950 "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
951
952 if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) {
954 input.model.get(), sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
955 } else {
957 input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
958 }
959 }
960 watch.stop();
961 printCounterexample(counterexample, &watch);
962 }
963 } else if (counterexampleSettings.isShortestPathGenerationSet()) {
964 for (auto const& property : input.properties) {
965 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
967 storm::utility::Stopwatch watch(true);
968 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException,
969 "Counterexample generation using shortest paths is currently only supported for DTMCs.");
971 property.getRawFormula(), counterexampleSettings.getShortestPathMaxK());
972 watch.stop();
973 printCounterexample(counterexample, &watch);
974 }
975 } else {
976 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported.");
977 }
978}
979
980template<typename ValueType>
981 requires(!storm::IsIntervalType<ValueType>)
982void printFilteredResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) {
983 if (result->isQuantitative()) {
985 STORM_PRINT(*result);
986 } else {
987 ValueType resultValue;
988 switch (ft) {
990 resultValue = result->asQuantitativeCheckResult<ValueType>().sum();
991 break;
993 resultValue = result->asQuantitativeCheckResult<ValueType>().average();
994 break;
996 resultValue = result->asQuantitativeCheckResult<ValueType>().getMin();
997 break;
999 resultValue = result->asQuantitativeCheckResult<ValueType>().getMax();
1000 break;
1003 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
1007 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results.");
1008 default:
1009 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unhandled filter type.");
1010 }
1012 STORM_PRINT(resultValue << " (approx. " << storm::utility::convertNumber<double>(resultValue) << ")");
1013 } else {
1014 STORM_PRINT(resultValue);
1015 }
1016 }
1017 } else {
1018 switch (ft) {
1020 STORM_PRINT(*result << '\n');
1021 break;
1023 STORM_PRINT(result->asQualitativeCheckResult().existsTrue());
1024 break;
1026 STORM_PRINT(result->asQualitativeCheckResult().forallTrue());
1027 break;
1029 STORM_PRINT(result->asQualitativeCheckResult().count());
1030 break;
1033 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
1038 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results.");
1039 }
1040 }
1041 STORM_PRINT('\n');
1042}
1043
1045 STORM_PRINT("\nModel checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ...\n");
1046}
1047
1048template<typename ValueType>
1049 requires(!storm::IsIntervalType<ValueType>)
1050void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::logic::Formula const& filterStatesFormula,
1051 storm::modelchecker::FilterType const& filterType, storm::utility::Stopwatch* watch = nullptr) {
1052 if (result) {
1053 std::stringstream ss;
1054 ss << "'" << filterStatesFormula << "'";
1055 STORM_PRINT((storm::utility::resources::isTerminate() ? "Result till abort" : "Result")
1056 << " (for " << (filterStatesFormula.isInitialFormula() ? "initial" : ss.str()) << " states): ");
1057 printFilteredResult<ValueType>(result, filterType);
1058 if (watch) {
1059 STORM_PRINT("Time for model checking: " << *watch << ".\n");
1060 }
1061 } else {
1062 STORM_LOG_ERROR("Property is unsupported by selected engine/settings.\n");
1063 }
1064}
1065
1066template<typename ValueType>
1067void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property,
1068 storm::utility::Stopwatch* watch = nullptr) {
1069 printResult<ValueType>(result, *property.getFilter().getStatesFormula(), property.getFilter().getFilterType(), watch);
1070}
1071
1072using VerificationCallbackType = std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula,
1073 std::shared_ptr<storm::logic::Formula const> const& states)>;
1074using PostprocessingCallbackType = std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)>;
1075
1077 void operator()(std::unique_ptr<storm::modelchecker::CheckResult> const&) {
1078 // Intentionally left empty.
1079 }
1080};
1081
1088template<typename ValueType>
1089std::unique_ptr<storm::modelchecker::CheckResult> verifyProperty(std::shared_ptr<storm::logic::Formula const> const& formula,
1090 std::shared_ptr<storm::logic::Formula const> const& statesFilter,
1091 VerificationCallbackType const& verificationCallback) {
1092 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
1093
1094 try {
1095 if constexpr (storm::IsIntervalType<ValueType>) {
1096 STORM_LOG_ASSERT(!transformationSettings.isChainEliminationSet() && !transformationSettings.isToNondeterministicModelSet(),
1097 "Unsupported transformation has been invoked.");
1098 return verificationCallback(formula, statesFilter);
1099 }
1100 if (transformationSettings.isChainEliminationSet() && !storm::transformer::NonMarkovianChainTransformer<ValueType>::preservesFormula(*formula)) {
1101 STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states.");
1102 } else if (transformationSettings.isToDiscreteTimeModelSet()) {
1103 auto transformedFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*formula);
1104 auto transformedStatesFilter = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*statesFilter);
1105 if (transformedFormula && transformedStatesFilter) {
1106 // invoke verification algorithm on transformed formulas
1107 return verificationCallback(transformedFormula, transformedStatesFilter);
1108 } else {
1109 STORM_LOG_WARN("Property is not preserved by transformation to discrete time model.");
1110 }
1111 } else {
1112 // invoke verification algorithm on given formulas
1113 return verificationCallback(formula, statesFilter);
1114 }
1115 } catch (storm::exceptions::BaseException const& ex) {
1116 STORM_LOG_WARN("Cannot handle property: " << ex.what());
1117 }
1118 return nullptr;
1119}
1120
1127template<typename ValueType>
1128void verifyProperties(SymbolicInput const& input, VerificationCallbackType const& verificationCallback,
1129 PostprocessingCallbackType const& postprocessingCallback = PostprocessingIdentity()) {
1130 auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
1131 for (auto const& property : properties) {
1133 storm::utility::Stopwatch watch(true);
1134 auto result = verifyProperty<ValueType>(property.getRawFormula(), property.getFilter().getStatesFormula(), verificationCallback);
1135 watch.stop();
1136 if (result) {
1137 postprocessingCallback(result);
1138 }
1139 printResult<storm::IntervalBaseType<ValueType>>(result, property, &watch);
1140 }
1141}
1142
1152template<typename ValueType>
1153void computeStateValues(std::string const& description, std::function<std::unique_ptr<storm::modelchecker::CheckResult>()> const& computationCallback,
1154 SymbolicInput const& input, VerificationCallbackType const& verificationCallback,
1155 PostprocessingCallbackType const& postprocessingCallback = PostprocessingIdentity()) {
1156 // First compute the state values for all the states by invoking the computationCallback
1157 storm::utility::Stopwatch watch(true);
1158 STORM_PRINT("\nComputing " << description << " ...\n");
1159 std::unique_ptr<storm::modelchecker::CheckResult> result;
1160 try {
1161 result = computationCallback();
1162 } catch (storm::exceptions::BaseException const& ex) {
1163 STORM_LOG_ERROR("Cannot compute " << description << ": " << ex.what());
1164 }
1165 if (!result) {
1166 STORM_LOG_ERROR("Computation had no result.");
1167 return;
1168 }
1169 // Now process the (potentially filtered) result
1170 if (input.properties.empty()) {
1171 // Do not apply any filtering, consider result for *all* states
1172 postprocessingCallback(result);
1173 printResult<ValueType>(result, *storm::logic::Formula::getTrueFormula(), storm::modelchecker::FilterType::VALUES, &watch);
1174 } else {
1175 // Each property identifies a subset of states to which we restrict (aka filter) the state-value result to
1176 auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
1177 for (uint64_t propertyIndex = 0; propertyIndex < properties.size(); ++propertyIndex) {
1178 auto const& property = properties[propertyIndex];
1179 // As the property serves as filter, it should (a) be qualitative and should (b) not consider a filter itself.
1180 if (!property.getRawFormula()->hasQualitativeResult()) {
1181 STORM_LOG_ERROR("Property '" << *property.getRawFormula()
1182 << "' can not be used for filtering states as it does not have a qualitative result.");
1183 continue;
1184 }
1185
1186 // Invoke verification algorithm on filtering property
1187 auto propertyFilter = verifyProperty<ValueType>(property.getRawFormula(), storm::logic::Formula::getTrueFormula(), verificationCallback);
1188
1189 if (propertyFilter) {
1190 // Filter and process result
1191 std::unique_ptr<storm::modelchecker::CheckResult> filteredResult = result->clone();
1192 filteredResult->filter(propertyFilter->asQualitativeCheckResult());
1193 postprocessingCallback(filteredResult);
1194 printResult<ValueType>(filteredResult, *property.getRawFormula(), property.getFilter().getFilterType(),
1195 propertyIndex == properties.size() - 1 ? &watch : nullptr);
1196 }
1197 }
1198 }
1199}
1200
1201inline std::vector<storm::expressions::Expression> parseConstraints(storm::expressions::ExpressionManager const& expressionManager,
1202 std::string const& constraintsString) {
1203 std::vector<storm::expressions::Expression> constraints;
1204
1205 std::vector<std::string> constraintsAsStrings;
1206 boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(","));
1207
1208 storm::parser::ExpressionParser expressionParser(expressionManager);
1209 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1210 for (auto const& variableTypePair : expressionManager) {
1211 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1212 }
1213 expressionParser.setIdentifierMapping(variableMapping);
1214
1215 for (auto const& constraintString : constraintsAsStrings) {
1216 if (constraintString.empty()) {
1217 continue;
1218 }
1219
1220 storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString);
1221 STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << ".");
1222 constraints.emplace_back(constraint);
1223 }
1224
1225 return constraints;
1226}
1227
1228inline std::vector<std::vector<storm::expressions::Expression>> parseInjectedRefinementPredicates(
1229 storm::expressions::ExpressionManager const& expressionManager, std::string const& refinementPredicatesString) {
1230 std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
1231
1232 storm::parser::ExpressionParser expressionParser(expressionManager);
1233 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1234 for (auto const& variableTypePair : expressionManager) {
1235 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1236 }
1237 expressionParser.setIdentifierMapping(variableMapping);
1238
1239 std::vector<std::string> predicateGroupsAsStrings;
1240 boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";"));
1241
1242 if (!predicateGroupsAsStrings.empty()) {
1243 for (auto const& predicateGroupString : predicateGroupsAsStrings) {
1244 if (predicateGroupString.empty()) {
1245 continue;
1246 }
1247
1248 std::vector<std::string> predicatesAsStrings;
1249 boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
1250
1251 if (!predicatesAsStrings.empty()) {
1252 injectedRefinementPredicates.emplace_back();
1253 for (auto const& predicateString : predicatesAsStrings) {
1254 storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
1255 STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
1256 injectedRefinementPredicates.back().emplace_back(predicate);
1257 }
1258
1259 STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException,
1260 "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
1261
1262 // Finally reverse the list, because we take the predicates from the back.
1263 std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
1264 }
1265 }
1266
1267 // Finally reverse the list, because we take the predicates from the back.
1268 std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
1269 }
1270
1271 return injectedRefinementPredicates;
1272}
1273
1274template<storm::dd::DdType DdType, typename ValueType>
1276 STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
1277 storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
1279 parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()),
1280 parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
1281
1282 verifyProperties<ValueType>(input, [&input, &options, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
1283 std::shared_ptr<storm::logic::Formula const> const& states) {
1284 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
1285 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, input.model.get(),
1286 storm::api::createTask<ValueType>(formula, true), options);
1287 });
1288}
1289
1290template<typename ValueType>
1292 STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
1293 STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException,
1294 "Exploration does not support other data-types than floating points.");
1295 verifyProperties<ValueType>(
1296 input, [&input, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1297 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
1298 return storm::api::verifyWithExplorationEngine<ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true));
1299 });
1300}
1301
1302template<typename ValueType>
1303void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& sparseModel, SymbolicInput const& input,
1304 ModelProcessingInformation const& mpi) {
1305 auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
1306 auto verificationCallback = [&sparseModel, &ioSettings, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
1307 std::shared_ptr<storm::logic::Formula const> const& states) {
1308 bool filterForInitialStates = states->isInitialFormula();
1309 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1310 if (ioSettings.isExportSchedulerSet()) {
1311 task.setProduceSchedulers(true);
1312 }
1313 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, task);
1314
1315 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1316 if (filterForInitialStates) {
1317 filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
1318 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1319 filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, storm::api::createTask<ValueType>(states, false));
1320 }
1321 if (result && filter) {
1322 result->filter(filter->asQualitativeCheckResult());
1323 }
1324 return result;
1325 };
1326 uint64_t exportCount = 0; // this number will be prepended to the export file name of schedulers and/or check results in case of multiple properties.
1327 auto postprocessingCallback = [&sparseModel, &ioSettings, &input, &exportCount](std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
1328 // Scheduler export
1329 STORM_LOG_WARN_COND(!ioSettings.isExportSchedulerSet() || result->hasScheduler(), "Scheduler requested but could not be generated.");
1330 if (ioSettings.isExportSchedulerSet() && result->hasScheduler()) {
1331 std::filesystem::path schedulerExportPath = ioSettings.getExportSchedulerFilename();
1332 if (exportCount > 0) {
1333 STORM_LOG_WARN("Prepending " << exportCount << " to scheduler file name for this property because there are multiple properties.");
1334 schedulerExportPath.replace_filename(std::to_string(exportCount) + schedulerExportPath.filename().string());
1335 }
1336 STORM_PRINT_AND_LOG("Exporting scheduler ... ");
1337 if (input.model) {
1338 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(),
1339 "No information of state valuations available. The scheduler output will use internal state ids. You might be "
1340 "interested in building the model with state valuations using --buildstateval.");
1342 sparseModel->hasChoiceLabeling() || sparseModel->hasChoiceOrigins(),
1343 "No symbolic choice information is available. The scheduler output will use internal choice ids. You might be interested in "
1344 "building the model with choice labels or choice origins using --buildchoicelab or --buildchoiceorig.");
1345 STORM_LOG_WARN_COND(sparseModel->hasChoiceLabeling() && !sparseModel->hasChoiceOrigins(),
1346 "Only partial choice information is available. You might want to build the model with choice origins using "
1347 "--buildchoicelab or --buildchoiceorig.");
1348 }
1349 if (result->isExplicitQuantitativeCheckResult()) {
1350 if constexpr (storm::IsIntervalType<ValueType>) {
1351 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for interval models is not supported.");
1352 } else {
1353 storm::api::exportScheduler(sparseModel, result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler(),
1354 schedulerExportPath.string());
1355 }
1356 } else if (result->isExplicitParetoCurveCheckResult()) {
1357 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
1358 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for models of this value type is not supported.");
1359 } else {
1360 auto const& paretoRes = result->template asExplicitParetoCurveCheckResult<ValueType>();
1361 storm::api::exportParetoScheduler(sparseModel, paretoRes.getPoints(), paretoRes.getSchedulers(), schedulerExportPath.string());
1362 }
1363 } else {
1364 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this value type.");
1365 }
1366 }
1367
1368 // Result export
1369 if (ioSettings.isExportCheckResultSet()) {
1370 if constexpr (storm::IsIntervalType<ValueType>) {
1371 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Result export for interval models is not supported.");
1372 } else {
1373 std::filesystem::path resultExportPath = ioSettings.getExportCheckResultFilename();
1374 if (exportCount > 0) {
1375 STORM_LOG_WARN("Prepending " << exportCount << " to result file name for this property because there are multiple properties.");
1376 resultExportPath.replace_filename(std::to_string(exportCount) + resultExportPath.filename().string());
1377 }
1378 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(),
1379 "No information of state valuations available. The result output will use internal state ids. You might be interested in "
1380 "building the model with state valuations using --buildstateval.");
1381 storm::api::exportCheckResultToJson(sparseModel, result, resultExportPath);
1382 }
1383 }
1384 ++exportCount;
1385 };
1386 if (!(ioSettings.isComputeSteadyStateDistributionSet() || ioSettings.isComputeExpectedVisitingTimesSet())) {
1387 verifyProperties<ValueType>(input, verificationCallback, postprocessingCallback);
1388 }
1389 if (ioSettings.isComputeSteadyStateDistributionSet()) {
1390 if constexpr (storm::IsIntervalType<ValueType>) {
1391 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing steady state distribution is not supported for interval models.");
1392 } else {
1393 computeStateValues<ValueType>(
1394 "steady-state probabilities",
1395 [&mpi, &sparseModel]() { return storm::api::computeSteadyStateDistributionWithSparseEngine<ValueType>(mpi.env, sparseModel); }, input,
1396 verificationCallback, postprocessingCallback);
1397 }
1398 }
1399 if (ioSettings.isComputeExpectedVisitingTimesSet()) {
1400 if constexpr (storm::IsIntervalType<ValueType>) {
1401 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing expected visiting times is not supported for interval models.");
1402 } else {
1403 computeStateValues<ValueType>(
1404 "expected visiting times",
1405 [&mpi, &sparseModel]() { return storm::api::computeExpectedVisitingTimesWithSparseEngine<ValueType>(mpi.env, sparseModel); }, input,
1406 verificationCallback, postprocessingCallback);
1407 }
1408 }
1409}
1410
1411template<storm::dd::DdType DdType, typename ValueType>
1412void verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& symbolicModel, SymbolicInput const& input,
1413 ModelProcessingInformation const& mpi) {
1414 verifyProperties<ValueType>(
1415 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1416 bool filterForInitialStates = states->isInitialFormula();
1417 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1418
1419 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.env, symbolicModel, task);
1420
1421 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1422 if (filterForInitialStates) {
1423 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1424 symbolicModel->getInitialStates());
1425 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1426 filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(states, false));
1427 }
1428 if (result && filter) {
1429 result->filter(filter->asQualitativeCheckResult());
1430 }
1431 return result;
1432 });
1433}
1434
1435template<storm::dd::DdType DdType, typename ValueType>
1436void verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& symbolicModel, SymbolicInput const& input,
1437 ModelProcessingInformation const& mpi) {
1438 verifyProperties<ValueType>(
1439 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1440 bool filterForInitialStates = states->isInitialFormula();
1441 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1442
1443 std::unique_ptr<storm::modelchecker::CheckResult> result =
1444 storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(formula, true));
1445
1446 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1447 if (filterForInitialStates) {
1448 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1449 symbolicModel->getInitialStates());
1450 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1451 filter = storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(states, false));
1452 }
1453 if (result && filter) {
1454 result->filter(filter->asQualitativeCheckResult());
1455 }
1456 return result;
1457 });
1458}
1459
1460template<storm::dd::DdType DdType, typename ValueType>
1462 ModelProcessingInformation const& mpi) {
1463 verifyProperties<ValueType>(
1464 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1465 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
1466 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, symbolicModel,
1467 storm::api::createTask<ValueType>(formula, true));
1468 });
1469}
1470
1471template<storm::dd::DdType DdType, typename ValueType>
1472typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifyModel(
1473 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& symbolicModel, SymbolicInput const& input,
1474 ModelProcessingInformation const& mpi) {
1476 verifyWithHybridEngine<DdType, ValueType>(symbolicModel, input, mpi);
1477 } else if (mpi.engine == storm::utility::Engine::Dd) {
1478 verifyWithDdEngine<DdType, ValueType>(symbolicModel, input, mpi);
1479 } else {
1480 verifyWithAbstractionRefinementEngine<DdType, ValueType>(symbolicModel, input, mpi);
1481 }
1482}
1483
1484template<storm::dd::DdType DdType, typename ValueType>
1485typename std::enable_if<DdType == storm::dd::DdType::CUDD && !std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(
1486 std::shared_ptr<storm::models::ModelBase> const&, SymbolicInput const&, ModelProcessingInformation const&) {
1487 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type.");
1488}
1489
1490inline std::shared_ptr<storm::models::ModelBase> buildPreprocessModel(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1491 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
1492 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
1493
1494 std::shared_ptr<storm::models::ModelBase> model;
1495 if (!buildSettings.isNoBuildModelSet()) {
1496 model = buildModel(input, ioSettings, mpi);
1497 }
1498 if (!model) {
1499 STORM_LOG_THROW(input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
1500 return nullptr;
1501 }
1502 model->printModelInformationToStream(std::cout);
1503
1504 storm::utility::Stopwatch preprocessingWatch(true);
1505 auto preprocessingResult = castAndApply(model, [&input, &mpi](auto const& m) { return preprocessModel(m, input, mpi); });
1506 preprocessingWatch.stop();
1507 if (preprocessingResult.second) {
1508 STORM_PRINT("\nTime for model preprocessing: " << preprocessingWatch << ".\n\n");
1509 model = preprocessingResult.first;
1510 model->printModelInformationToStream(std::cout);
1511 }
1512
1513 return model;
1514}
1515
1516inline std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModel(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1517 auto model = buildPreprocessModel(input, mpi);
1518 if (model) {
1519 castAndApply(model, [&input](auto const& m) { exportModel(m, input); });
1520 }
1521 return model;
1522}
1523
1524inline void processInput(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1525 auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
1526 auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
1527
1528 // For several engines, no model building step is performed, but the verification is started right away.
1530 abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
1532 [&input, &mpi]<storm::dd::DdType DD, typename VT>() { verifyWithAbstractionRefinementEngine<DD, VT>(input, mpi); });
1533 } else if (mpi.engine == storm::utility::Engine::Exploration) {
1534 applyValueType(mpi.verificationValueType, [&input, &mpi]<typename VT>() { verifyWithExplorationEngine<VT>(input, mpi); });
1535 } else {
1536 std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModel(input, mpi);
1537 if (model) {
1538 if (counterexampleSettings.isCounterexampleSet()) {
1539 castAndApply(model, [&input](auto const& m) { generateCounterexamples(m, input); });
1540 } else {
1541 castAndApply(model, [&input, &mpi](auto const& m) { verifyModel(m, input, mpi); });
1542 }
1543 }
1544 }
1545}
1546} // namespace cli
1547} // namespace storm
BuilderOptions & setBuildAllLabels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
BuilderOptions & setExplorationChecks(bool newValue=true)
Should extra checks be performed during exploration.
BuilderOptions & setAddOutOfBoundsState(bool newValue=true)
Should a state for out of bounds be constructed.
BuilderOptions & setReservedBitsForUnboundedVariables(uint64_t value)
Sets the number of bits that will be reserved for unbounded integer variables.
BuilderOptions & setBuildChoiceLabels(bool newValue=true)
Should the choice labels be built?
BuilderOptions & setBuildAllRewardModels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
BuilderOptions & setBuildChoiceOrigins(bool newValue=true)
Should the origins the different choices be built?
BuilderOptions & setBuildStateValuations(bool newValue=true)
Should the state valuation mapping be built?
BuilderOptions & setApplyMaximalProgressAssumption(bool newValue=true)
Should the maximal progress assumption be applied when building a Markov Automaton?
BuilderOptions & setBuildObservationValuations(bool newValue=true)
Should a observation valuation mapping be built?
BuilderOptions & setAddOverlappingGuardsLabel(bool newValue=true)
Should a state be labelled for overlapping guards.
This class represents the base class of all exception classes.
virtual const char * what() const noexcept override
Retrieves the message associated with this exception.
This class is responsible for managing a set of typed variables and all expressions using these varia...
std::shared_ptr< storm::logic::Formula const > const & getStatesFormula() const
Definition Property.h:52
storm::modelchecker::FilterType getFilterType() const
Definition Property.h:56
static Model eliminateAutomatically(const Model &model, std::vector< jani::Property > properties, uint64_t locationHeuristic, uint64_t edgesHeuristic)
std::shared_ptr< storm::logic::Formula const > getRawFormula() const
Definition Property.cpp:92
std::string const & getName() const
Get the provided name.
Definition Property.cpp:23
FilterExpression const & getFilter() const
Definition Property.cpp:88
static std::shared_ptr< Formula const > getTrueFormula()
Definition Formula.cpp:205
virtual std::optional< storm::dd::DdType > getDdType() const
Definition ModelBase.cpp:19
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
Base class for all sparse models.
Definition Model.h:32
Base class for all symbolic models.
Definition Model.h:45
storm::expressions::Expression parseFromString(std::string const &expressionString, bool ignoreError=false) const
Parses an expression from the given string.
void setIdentifierMapping(qi::symbols< char, storm::expressions::Expression > const *identifiers_)
Sets an identifier mapping that is used to determine valid variables in the expression.
storm::jani::Model toJani(bool allVariablesGlobal=true, std::string suffix="") const
Converts the PRISM model into an equivalent JANI model.
Definition Program.cpp:2340
This class represents the settings for the abstraction procedures.
std::string getInjectedRefinementPredicates() const
Retrieves a string containing refinement predicates to inject (if there are any).
std::string getConstraintString() const
Retrieves the string that specifies additional constraints.
This class represents the bisimulation settings.
storm::dd::bisimulation::QuotientFormat getQuotientFormat() const
Retrieves the format in which the quotient is to be extracted.
storm::dd::bisimulation::SignatureMode getSignatureMode() const
Retrieves the mode to compute signatures.
bool isQuotientFormatSetFromDefaultValue() const
Retrieves whether the format in which the quotient is to be extracted has been set from its default v...
bool isWeakBisimulationSet() const
Retrieves whether weak bisimulation is to be used.
bool isBuildChoiceLabelsSet() const
Retrieves whether the choice labels should be build.
This class represents the markov chain settings.
Definition IOSettings.h:19
bool isJaniPropertiesSet() const
Retrieves whether the jani-property option was set.
std::string getExplicitIMCAFilename() const
Retrieves the name of the file that contains the model in the IMCA format.
bool areJaniPropertiesSelected() const
Retrieves whether one or more jani-properties have been selected.
std::string getChoiceLabelingFilename() const
Retrieves the name of the file that contains the choice labeling if the model was given using the exp...
bool isStateRewardsSet() const
Retrieves whether the state reward option was set.
std::string getProperty() const
Retrieves the property specified with the property option.
std::string getJaniInputFilename() const
Retrieves the name of the file that contains the JANI model specification if the model was given usin...
bool isChoiceLabelingSet() const
Retrieves whether the choice labeling option was set.
bool isPrismOrJaniInputSet() const
Retrieves whether the JANI or PRISM input option was set.
std::string getPropertyFilter() const
Retrieves the property filter.
std::string getPrismInputFilename() const
Retrieves the name of the file that contains the PRISM model specification if the model was given usi...
bool isExplicitDRNSet() const
Retrieves whether the explicit option with DRN was set.
std::string getExplicitDRNFilename() const
Retrieves the name of the file that contains the model in the DRN format.
std::string getLabelingFilename() const
Retrieves the name of the file that contains the state labeling if the model was given using the expl...
boost::optional< std::vector< std::string > > getQvbsPropertyFilter() const
Retrieves the selected property names.
std::string getStateRewardsFilename() const
Retrieves the name of the file that contains the state rewards if the model was given using the expli...
std::string getTransitionRewardsFilename() const
Retrieves the name of the file that contains the transition rewards if the model was given using the ...
bool isPropertySet() const
Retrieves whether the property option was set.
std::string getQvbsModelName() const
Retrieves the specified model (short-)name of the QVBS.
std::vector< std::string > getSelectedJaniProperties() const
std::string getTransitionFilename() const
Retrieves the name of the file that contains the transitions if the model was given using the explici...
uint64_t getQvbsInstanceIndex() const
Retrieves the selected model instance (file + open parameters of the model)
bool isExplicitIMCASet() const
Retrieves whether the explicit option with IMCA was set.
bool isPrismInputSet() const
Retrieves whether the PRISM language option was set.
bool isTransitionRewardsSet() const
Retrieves whether the transition reward option was set.
bool isExplicitSet() const
Retrieves whether the explicit option was set.
This class provides easy access to a benchmark of the Quantitative Verification Benchmark Set http://...
Definition Qvbs.h:17
std::string const & getJaniFile(uint64_t instanceIndex=0) const
Definition Qvbs.cpp:107
std::string getInfo(uint64_t instanceIndex=0, boost::optional< std::vector< std::string > > propertyFilter=boost::none) const
Definition Qvbs.cpp:118
std::string const & getConstantDefinition(uint64_t instanceIndex=0) const
Definition Qvbs.cpp:112
storm::jani::Model const & asJaniModel() const
Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to th...
storm::utility::Engine getEngine() const
Retrieve "good" settings after calling predict.
void predict(storm::jani::Model const &model, storm::jani::Property const &property)
Predicts "good" settings for the provided model checking query.
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_WARN(message)
Definition logging.h:25
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
#define STORM_PRINT_AND_LOG(message)
Definition macros.h:68
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
Definition macros.h:62
void exportScheduler(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::storage::Scheduler< ValueType > const &scheduler, std::string const &filename)
Definition export.h:66
void exportSymbolicModelAsDot(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)
Definition export.h:61
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
std::shared_ptr< storm::models::sparse::Model< ValueType > > permuteModelStates(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::utility::permutation::OrderKind order, std::optional< uint64_t > seed=std::nullopt)
Permutes the order of the states of the model according to the given order.
std::shared_ptr< storm::counterexamples::Counterexample > computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Mdp< double > > mdp, std::shared_ptr< storm::logic::Formula const > const &formula)
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > eliminateNonMarkovianChains(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior)
Eliminates chains of non-Markovian states from a given Markov Automaton.
storm::jani::Property createMultiObjectiveProperty(std::vector< storm::jani::Property > const &properties)
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > parseJaniModel(std::string const &filename, boost::optional< std::vector< std::string > > const &propertyFilter)
void exportJaniModelAsDot(storm::jani::Model const &model, std::string const &filename)
Definition export.cpp:7
std::vector< storm::jani::Property > parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
std::shared_ptr< storm::models::sparse::Model< ValueType > > transformSymbolicToSparseModel(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &symbolicModel, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas=std::vector< std::shared_ptr< storm::logic::Formula const > >())
Transforms the given symbolic model to a sparse model.
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > transformContinuousToDiscreteTimeSparseModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
Transforms the given continuous model to a discrete time model.
void exportSymbolicModelAsDrdd(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)
Definition export.h:40
std::shared_ptr< storm::counterexamples::Counterexample > computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula)
std::vector< storm::jani::Property > parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::set< std::string > > const &propertyFilter)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
void simplifyJaniModel(storm::jani::Model &model, std::vector< storm::jani::Property > &properties, storm::jani::ModelFeatures const &supportedFeatures)
boost::optional< std::set< std::string > > parsePropertyFilter(std::string const &propertyFilter)
storm::jani::ModelFeatures getSupportedJaniFeatures(storm::builder::BuilderType const &builderType)
Definition builder.h:31
void exportSparseModelAsDrn(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, std::vector< std::string > const &parameterNames={}, bool allowPlaceholders=true)
Definition export.h:29
void exportCheckResultToJson(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > const &checkResult, std::string const &filename)
Definition export.h:113
std::shared_ptr< storm::counterexamples::Counterexample > computeKShortestPathCounterexample(std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, size_t maxK)
void exportSparseModelAsJson(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename)
Definition export.h:53
void exportSparseModelAsDot(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, size_t maxWidth=30)
Definition export.h:45
void exportParetoScheduler(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< PointType > const &points, std::vector< storm::storage::Scheduler< ValueType > > const &schedulers, std::string const &baseFilenameStr)
Definition export.h:80
std::vector< storm::jani::Property > substituteConstantsInProperties(std::vector< storm::jani::Property > const &properties, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)
void exportModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
void exportSymbolicInput(SymbolicInput const &input)
void parseSymbolicModelDescription(storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input)
void verifyWithAbstractionRefinementEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > buildModelExplicit(storm::settings::modules::IOSettings const &ioSettings, storm::settings::modules::BuildSettings const &buildSettings)
std::enable_if< DdType==storm::dd::DdType::CUDD &&!std::is_same< ValueType, double >::value, void >::type verifySymbolicModel(std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &, ModelProcessingInformation const &)
void verifyModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &sparseModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
auto castAndApply(std::shared_ptr< storm::models::ModelBase > const &model, auto const &callback)
SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const &ioSettings)
void getModelProcessingInformationAutomatic(SymbolicInput const &input, ModelProcessingInformation &mpi)
void verifyWithExplorationEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void printResult(std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::logic::Formula const &filterStatesFormula, storm::modelchecker::FilterType const &filterType, storm::utility::Stopwatch *watch=nullptr)
auto applyValueType(ModelProcessingInformation::ValueType vt, auto const &callback)
std::shared_ptr< storm::models::ModelBase > buildPreprocessExportModel(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void verifyProperties(SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
Verifies all (potentially preprocessed) properties given in input.
std::vector< storm::expressions::Expression > parseConstraints(storm::expressions::ExpressionManager const &expressionManager, std::string const &constraintsString)
std::vector< std::vector< storm::expressions::Expression > > parseInjectedRefinementPredicates(storm::expressions::ExpressionManager const &expressionManager, std::string const &refinementPredicatesString)
SymbolicInput parseSymbolicInput()
void verifyWithDdEngine(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &states)> VerificationCallbackType
std::shared_ptr< storm::models::ModelBase > buildModelSparse(SymbolicInput const &input, storm::builder::BuilderOptions const &options)
std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type preprocessDdMarkovAutomaton(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseMarkovAutomaton(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &model)
void printFilteredResult(std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::modelchecker::FilterType ft)
void computeStateValues(std::string const &description, std::function< std::unique_ptr< storm::modelchecker::CheckResult >()> const &computationCallback, SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
Computes values for each state (such as the steady-state probability distribution).
void printCounterexample(std::shared_ptr< storm::counterexamples::Counterexample > const &counterexample, storm::utility::Stopwatch *watch=nullptr)
std::pair< SymbolicInput, ModelProcessingInformation > preprocessSymbolicInput(SymbolicInput const &input)
std::shared_ptr< storm::models::ModelBase > buildModel(SymbolicInput const &input, storm::settings::modules::IOSettings const &ioSettings, ModelProcessingInformation const &mpi)
void printModelCheckingProperty(storm::jani::Property const &property)
void parseProperties(storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input, boost::optional< std::set< std::string > > const &propertyFilter)
void verifyWithHybridEngine(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
ModelProcessingInformation getModelProcessingInformation(SymbolicInput const &input, std::shared_ptr< SymbolicInput > const &transformedJaniInput=nullptr)
Sets the model processing information based on the given input.
void printComputingCounterexample(storm::jani::Property const &property)
std::shared_ptr< storm::models::Model< ExportValueType > > preprocessDdModelBisimulation(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings, ModelProcessingInformation const &mpi)
auto applyDdLibValueType(storm::dd::DdType dd, ModelProcessingInformation::ValueType vt, auto const &callback)
std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> PostprocessingCallbackType
std::shared_ptr< storm::models::ModelBase > buildPreprocessModel(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseModelBisimulation(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings)
storm::builder::BuilderOptions createBuildOptionsSparseFromSettings(SymbolicInput const &input)
void processInput(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void ensureNoUndefinedPropertyConstants(std::vector< storm::jani::Property > const &properties)
void generateCounterexamples(std::shared_ptr< ModelType > const &, SymbolicInput const &)
std::vector< std::shared_ptr< storm::logic::Formula const > > createFormulasToRespect(std::vector< storm::jani::Property > const &properties)
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > buildModelDd(SymbolicInput const &input)
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessDdModelImpl(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::unique_ptr< storm::modelchecker::CheckResult > verifyProperty(std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &statesFilter, VerificationCallbackType const &verificationCallback)
Verifies the given formula plus a filter formula to identify relevant states and warns the user in ca...
std::string toString(ModelExportFormat const &input)
SettingsManager const & manager()
Retrieves the settings manager.
std::string orderKindtoString(OrderKind order)
Converts the given order to a string.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
bool isConstant(ValueType const &)
Definition constants.cpp:66
bool canHandle< storm::RationalFunction >(storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &checkTask)
Definition Engine.cpp:202
Engine
An enumeration of all engines.
Definition Engine.h:31
template bool canHandle< storm::RationalNumber >(storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
template bool canHandle< double >(storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
storm::builder::BuilderType getBuilderType(Engine const &engine)
Returns the builder type used for the given engine.
Definition Engine.cpp:84
LabParser.cpp.
typename detail::IntervalMetaProgrammingHelper< ValueType >::BaseType IntervalBaseType
Helper to access the type in which interval boundaries are stored.
void operator()(std::unique_ptr< storm::modelchecker::CheckResult > const &)
std::vector< storm::jani::Property > properties
boost::optional< storm::storage::SymbolicModelDescription > model
boost::optional< std::vector< storm::jani::Property > > preprocessedProperties