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 "storm/io/file.h"
16
19
20#include <type_traits>
21
24
26
28
30
32
34
38
50#include "storm/storage/Qvbs.h"
53
55
56namespace storm {
57namespace cli {
58
60 // The symbolic model description.
61 boost::optional<storm::storage::SymbolicModelDescription> model;
62
63 // The original properties to check.
64 std::vector<storm::jani::Property> properties;
65
66 // The preprocessed properties to check (in case they needed amendment).
67 boost::optional<std::vector<storm::jani::Property>> preprocessedProperties;
68};
69
72 if (ioSettings.isPrismOrJaniInputSet()) {
73 storm::utility::Stopwatch modelParsingWatch(true);
74 if (ioSettings.isPrismInputSet()) {
75 input.model =
76 storm::api::parseProgram(ioSettings.getPrismInputFilename(), buildSettings.isPrismCompatibilityEnabled(), !buildSettings.isNoSimplifySet());
77 } else {
78 boost::optional<std::vector<std::string>> propertyFilter;
79 if (ioSettings.isJaniPropertiesSet()) {
80 if (ioSettings.areJaniPropertiesSelected()) {
81 propertyFilter = ioSettings.getSelectedJaniProperties();
82 } else {
83 propertyFilter = boost::none;
84 }
85 } else {
86 propertyFilter = std::vector<std::string>();
87 }
88 auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), propertyFilter);
89 input.model = std::move(janiInput.first);
90 if (ioSettings.isJaniPropertiesSet()) {
91 input.properties = std::move(janiInput.second);
92 }
93 }
94 modelParsingWatch.stop();
95 STORM_PRINT("Time for model input parsing: " << modelParsingWatch << ".\n\n");
96 }
97}
98
100 boost::optional<std::set<std::string>> const& propertyFilter) {
101 if (ioSettings.isPropertySet()) {
102 std::vector<storm::jani::Property> newProperties;
103 if (input.model) {
104 newProperties = storm::api::parsePropertiesForSymbolicModelDescription(ioSettings.getProperty(), input.model.get(), propertyFilter);
105 } else {
106 newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter);
107 }
108
109 input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end());
110 }
111}
112
114 // Parse the model input
115 SymbolicInput input;
116 storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName());
117 STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter()));
118 storm::utility::Stopwatch modelParsingWatch(true);
119 auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), ioSettings.getQvbsPropertyFilter());
120 input.model = std::move(janiInput.first);
121 input.properties = std::move(janiInput.second);
122 modelParsingWatch.stop();
123 STORM_PRINT("Time for model input parsing: " << modelParsingWatch << ".\n\n");
124
125 // Parse additional properties
126 boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
127 parseProperties(ioSettings, input, propertyFilter);
128
129 // Substitute constant definitions
130 auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex()));
131 input.model = input.model.get().preprocess(constantDefinitions);
132 if (!input.properties.empty()) {
133 input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions);
134 }
135
136 return input;
137}
138
141 if (ioSettings.isQvbsInputSet()) {
142 return parseSymbolicInputQvbs(ioSettings);
143 } else {
144 // Parse the property filter, if any is given.
145 boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
146
147 SymbolicInput input;
148 parseSymbolicModelDescription(ioSettings, input);
149 parseProperties(ioSettings, input, propertyFilter);
150 return input;
151 }
152}
153
155 // The engine to use
157
158 // If set, bisimulation will be applied.
160
161 // If set, a transformation to Jani will be enforced
163
164 // Which data type is to be used for numbers ...
166 ValueType buildValueType; // ... during model building
167 ValueType verificationValueType; // ... during model verification
168
169 // The Dd library to be used
171
172 // The environment used during model checking
174
175 // A flag which is set to true, if the settings were detected to be compatible.
176 // If this is false, it could be that the query can not be handled.
178};
179
182
183 STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model.");
184 STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model.");
185 std::vector<storm::jani::Property> const& properties =
186 input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties;
187 STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a property.");
188 STORM_LOG_WARN_COND(properties.size() == 1,
189 "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered.");
190
192 if (hints.isNumberStatesSet()) {
193 as.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates());
194 } else {
195 as.predict(input.model->asJaniModel(), properties.front());
196 }
197
198 mpi.engine = as.getEngine();
199 if (as.enableBisimulation()) {
200 mpi.applyBisimulation = true;
201 }
204 }
205 STORM_PRINT_AND_LOG("Automatic engine picked the following settings: \n"
206 << "\tengine=" << mpi.engine << std::boolalpha << "\t bisimulation=" << mpi.applyBisimulation
207 << "\t exact=" << (mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision) << std::noboolalpha << '\n');
208}
209
216 std::shared_ptr<SymbolicInput> const& transformedJaniInput = nullptr) {
222
223 // Set the engine.
224 mpi.engine = coreSettings.getEngine();
225
226 // Set whether bisimulation is to be used.
227 mpi.applyBisimulation = generalSettings.isBisimulationSet();
228
229 // Set the value type used for numeric values
230 if (generalSettings.isParametricSet()) {
232 } else if (generalSettings.isExactSet()) {
234 } else {
236 }
237 auto originalVerificationValueType = mpi.verificationValueType;
238
239 // Since the remaining settings could depend on the ones above, we need apply the automatic engine now.
240 bool useAutomatic = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Automatic;
241 if (useAutomatic) {
242 if (input.model->isJaniModel()) {
243 // 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
244 // bisimulation or disable exact arithmetic)
246 } else {
247 // Transform Prism to jani first
248 STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input.");
249 SymbolicInput janiInput;
250 janiInput.properties = input.properties;
251 storm::prism::Program const& prog = input.model.get().asPrismProgram();
252 auto modelAndProperties = prog.toJani(input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties);
253 janiInput.model = modelAndProperties.first;
254 if (!modelAndProperties.second.empty()) {
255 janiInput.preprocessedProperties = std::move(modelAndProperties.second);
256 }
257 // 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
258 // bisimulation or disable exact arithmetic)
260 if (transformedJaniInput) {
261 // We cache the transformation result.
262 *transformedJaniInput = std::move(janiInput);
263 }
264 }
265 }
266
267 // Check whether these settings are compatible with the provided input.
268 if (input.model) {
269 auto checkCompatibleSettings = [&mpi, &input] {
270 switch (mpi.verificationValueType) {
273 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
276 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
277 break;
280 mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
281 }
282 return false;
283 };
284 mpi.isCompatible = checkCompatibleSettings();
285 if (!mpi.isCompatible) {
286 if (useAutomatic) {
288 STORM_LOG_WARN("The settings picked by the automatic engine (engine="
289 << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact
290 << ") are incompatible with this model. Falling back to default settings.");
292 mpi.applyBisimulation = false;
293 mpi.verificationValueType = originalVerificationValueType;
294 // Retry check with new settings
295 mpi.isCompatible = checkCompatibleSettings();
296 }
297 }
298 } else {
299 // If there is no input model, nothing has to be done, actually
300 mpi.isCompatible = true;
301 }
302
303 // Set whether a transformation to jani is required or necessary
304 mpi.transformToJani = ioSettings.isPrismToJaniSet();
305 if (input.model) {
306 auto builderType = storm::utility::getBuilderType(mpi.engine);
307 bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) &&
308 (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA) && (!input.model->isJaniModel());
309 STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA,
310 "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.");
311 mpi.transformToJani |= transformToJaniForDdMA;
312 }
313
314 // Set the Valuetype used during model building
316 if (bisimulationSettings.useExactArithmeticInDdBisimulation()) {
320 }
321 } else {
322 STORM_LOG_WARN("Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied.");
323 }
324 }
325
326 // Set the Dd library
327 mpi.ddType = coreSettings.getDdLibraryType();
328 if (mpi.ddType == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue()) {
331 STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
333 }
334 }
335 return mpi;
336}
337
338inline void ensureNoUndefinedPropertyConstants(std::vector<storm::jani::Property> const& properties) {
339 // Make sure there are no undefined constants remaining in any property.
340 for (auto const& property : properties) {
341 std::set<storm::expressions::Variable> usedUndefinedConstants = property.getUndefinedConstants();
342 if (!usedUndefinedConstants.empty()) {
343 std::vector<std::string> undefinedConstantsNames;
344 for (auto const& constant : usedUndefinedConstants) {
345 undefinedConstantsNames.emplace_back(constant.getName());
346 }
348 false, storm::exceptions::InvalidArgumentException,
349 "The property '" << property << " still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames, ",") << ".");
350 }
351 }
352}
353
354inline std::pair<SymbolicInput, ModelProcessingInformation> preprocessSymbolicInput(SymbolicInput const& input) {
356
357 SymbolicInput output = input;
358
359 // Preprocess properties (if requested)
360 if (ioSettings.isPropertiesAsMultiSet()) {
361 STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException,
362 "Can not translate properties to multi-objective formula because no properties were specified.");
364 }
365
366 // Substitute constant definitions in symbolic input.
367 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
368 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
369 if (output.model) {
370 constantDefinitions = output.model.get().parseConstantDefinitions(constantDefinitionString);
371 output.model = output.model.get().preprocess(constantDefinitions);
372 }
373 if (!output.properties.empty()) {
374 output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
375 }
377 auto transformedJani = std::make_shared<SymbolicInput>();
378 ModelProcessingInformation mpi = getModelProcessingInformation(output, transformedJani);
379
380 // Check whether conversion for PRISM to JANI is requested or necessary.
381 if (output.model && output.model.get().isPrismProgram()) {
382 if (mpi.transformToJani) {
383 if (transformedJani->model) {
384 // Use the cached transformation if possible
385 output = std::move(*transformedJani);
386 } else {
387 storm::prism::Program const& model = output.model.get().asPrismProgram();
388 auto modelAndProperties = model.toJani(output.properties);
389
390 output.model = modelAndProperties.first;
391
392 if (!modelAndProperties.second.empty()) {
393 output.preprocessedProperties = std::move(modelAndProperties.second);
394 }
395 }
396 }
397 }
398
399 if (output.model && output.model.get().isJaniModel()) {
401 storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures);
402
404 if (buildSettings.isLocationEliminationSet()) {
405 auto locationHeuristic = buildSettings.getLocationEliminationLocationHeuristic();
406 auto edgesHeuristic = buildSettings.getLocationEliminationEdgesHeuristic();
407 output.model->setModel(storm::jani::JaniLocalEliminator::eliminateAutomatically(output.model.get().asJaniModel(), output.properties,
408 locationHeuristic, edgesHeuristic));
409 }
410 }
411
412 return {output, mpi};
413}
414
415inline void exportSymbolicInput(SymbolicInput const& input) {
417 if (input.model && input.model.get().isJaniModel()) {
418 storm::storage::SymbolicModelDescription const& model = input.model.get();
419 if (ioSettings.isExportJaniDotSet()) {
420 storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename());
421 }
422 }
423}
424
425inline std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
426 std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);
427
428 for (auto const& property : properties) {
429 if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
430 result.push_back(property.getFilter().getStatesFormula());
431 }
432 }
433
434 return result;
435}
436
437template<storm::dd::DdType DdType, typename ValueType>
438std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
439 if (DdType == storm::dd::DdType::Sylvan) {
440 auto numThreads = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads();
441 STORM_PRINT_AND_LOG("Using Sylvan with " << numThreads << " parallel threads.\n");
442 }
444 return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(),
445 !buildSettings.isApplyNoMaximumProgressAssumptionSet());
446}
447
451 options.setBuildChoiceLabels(options.isBuildChoiceLabelsSet() || buildSettings.isBuildChoiceLabelsSet());
452 options.setBuildStateValuations(options.isBuildStateValuationsSet() || buildSettings.isBuildStateValuationsSet());
453 options.setBuildAllLabels(options.isBuildAllLabelsSet() || buildSettings.isBuildAllLabelsSet());
454 options.setBuildObservationValuations(options.isBuildObservationValuationsSet() || buildSettings.isBuildObservationValuationsSet());
455 bool buildChoiceOrigins = options.isBuildChoiceOriginsSet() || buildSettings.isBuildChoiceOriginsSet();
458 if (counterexampleGeneratorSettings.isCounterexampleSet()) {
459 buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet();
460 }
461 }
462 options.setBuildChoiceOrigins(buildChoiceOrigins);
463
464 if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) {
466 }
467
468 if (buildSettings.isExplorationChecksSet()) {
469 options.setExplorationChecks();
470 }
471 options.setReservedBitsForUnboundedVariables(buildSettings.getBitsForUnboundedVariables());
472
473 options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet());
474 if (buildSettings.isBuildFullModelSet()) {
475 options.clearTerminalStates();
477 options.setBuildAllLabels(true);
478 options.setBuildAllRewardModels(true);
479 }
480
481 if (buildSettings.isAddOverlappingGuardsLabelSet()) {
482 options.setAddOverlappingGuardsLabel(true);
483 }
484
486 if (ioSettings.isComputeExpectedVisitingTimesSet() || ioSettings.isComputeSteadyStateDistributionSet()) {
487 options.clearTerminalStates();
488 }
489 return options;
490}
491
492template<typename ValueType>
493std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::builder::BuilderOptions const& options) {
494 return storm::api::buildSparseModel<ValueType>(input.model.get(), options);
495}
496
497template<typename ValueType>
498std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings,
499 storm::settings::modules::BuildSettings const& buildSettings) {
500 std::shared_ptr<storm::models::ModelBase> result;
501 if (ioSettings.isExplicitSet()) {
502 result = storm::api::buildExplicitModel<ValueType>(
503 ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(),
504 ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none,
505 ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none,
506 ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
507 } else if (ioSettings.isExplicitDRNSet()) {
509 options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet();
510 result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename(), options);
511 } else {
512 STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
513 result = storm::api::buildExplicitIMCAModel<ValueType>(ioSettings.getExplicitIMCAFilename());
514 }
515 return result;
516}
517
518template<storm::dd::DdType DdType, typename ValueType>
519std::shared_ptr<storm::models::ModelBase> buildModel(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings,
520 ModelProcessingInformation const& mpi) {
521 storm::utility::Stopwatch modelBuildingWatch(true);
522
523 std::shared_ptr<storm::models::ModelBase> result;
524 if (input.model) {
525 auto builderType = storm::utility::getBuilderType(mpi.engine);
526 if (builderType == storm::builder::BuilderType::Dd) {
527 result = buildModelDd<DdType, ValueType>(input);
528 } else if (builderType == storm::builder::BuilderType::Explicit) {
529 auto options = createBuildOptionsSparseFromSettings(input);
530 result = buildModelSparse<ValueType>(input, options);
531 }
532 } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
533 STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException,
534 "Can only use sparse engine with explicit input.");
535 result = buildModelExplicit<ValueType>(ioSettings, storm::settings::getModule<storm::settings::modules::BuildSettings>());
536 }
537
538 modelBuildingWatch.stop();
539 if (result) {
540 STORM_PRINT("Time for model construction: " << modelBuildingWatch << ".\n\n");
541 }
542
543 return result;
544}
545
546template<typename ValueType>
547std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovAutomaton(
548 std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& model) {
551
552 std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
553 model->close();
554 STORM_LOG_WARN_COND(!debugSettings.isAdditionalChecksSet() || !model->containsZenoCycle(),
555 "MA contains a Zeno cycle. Model checking results cannot be trusted.");
556
557 if (model->isConvertibleToCtmc()) {
558 STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead.");
559 result = model->convertToCtmc();
560 }
561
562 if (transformationSettings.isChainEliminationSet()) {
563 // TODO: we should also transform the properties at this point.
565 transformationSettings.getLabelBehavior())
566 .first;
567 }
568
569 return result;
570}
571
572template<typename ValueType>
573std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseModelBisimulation(
574 std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input,
575 storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
577 if (bisimulationSettings.isWeakBisimulationSet()) {
579 }
580
581 STORM_LOG_INFO("Performing bisimulation minimization...");
582 return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
583}
584
585template<typename ValueType>
586std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> preprocessSparseModel(
587 std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
591
592 std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
593
594 if (auto order = transformationSettings.getModelPermutation(); order.has_value()) {
595 auto seed = transformationSettings.getModelPermutationSeed();
596 STORM_PRINT_AND_LOG("Permuting model states using " << storm::utility::permutation::orderKindtoString(order.value()) << " order"
597 << (seed.has_value() ? " with seed " + std::to_string(seed.value()) : "") << ".\n");
598 result.first = storm::api::permuteModelStates(result.first, order.value(), seed);
599 result.second = true;
600 STORM_PRINT_AND_LOG("Transition matrix hash after permuting: " << result.first->getTransitionMatrix().hash() << ".\n");
601 }
602
603 if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
605 result.second = true;
606 }
607
608 if (mpi.applyBisimulation) {
609 result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
610 result.second = true;
611 }
612
613 if (transformationSettings.isToDiscreteTimeModelSet()) {
614 // TODO: we should also transform the properties at this point.
615 STORM_LOG_WARN_COND(!model->hasRewardModel("_time"),
616 "Scheduled transformation to discrete time model, but a reward model named '_time' is already present in this model. We might take "
617 "the wrong reward model later.");
618 result.first =
620 .first;
621 result.second = true;
622 }
623
624 if (transformationSettings.isToNondeterministicModelSet()) {
625 result.first = storm::api::transformToNondeterministicModel<ValueType>(std::move(*result.first));
626 result.second = true;
627 }
628
629 return result;
630}
631
632template<typename ValueType>
633void exportSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
635
636 if (ioSettings.isExportBuildSet()) {
637 switch (ioSettings.getExportBuildFormat()) {
639 storm::api::exportSparseModelAsDot(model, ioSettings.getExportBuildFilename(), ioSettings.getExportDotMaxWidth());
640 break;
642 storm::api::exportSparseModelAsDrn(model, ioSettings.getExportBuildFilename(),
643 input.model ? input.model.get().getParameterNames() : std::vector<std::string>(),
644 !ioSettings.isExplicitExportPlaceholdersDisabled());
645 break;
647 storm::api::exportSparseModelAsJson(model, ioSettings.getExportBuildFilename());
648 break;
649 default:
650 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
651 "Exporting sparse models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
652 }
653 }
654
655 // TODO: The following options are depreciated and shall be removed at some point:
656
657 if (ioSettings.isExportExplicitSet()) {
658 storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(),
659 input.model ? input.model.get().getParameterNames() : std::vector<std::string>(),
660 !ioSettings.isExplicitExportPlaceholdersDisabled());
661 }
662
663 if (ioSettings.isExportDdSet()) {
664 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drdd format is only supported for DDs.");
665 }
666
667 if (ioSettings.isExportDotSet()) {
668 storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth());
669 }
670}
671
672template<storm::dd::DdType DdType, typename ValueType>
675
676 if (ioSettings.isExportBuildSet()) {
677 switch (ioSettings.getExportBuildFormat()) {
679 storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportBuildFilename());
680 break;
682 storm::api::exportSymbolicModelAsDrdd(model, ioSettings.getExportBuildFilename());
683 break;
684 default:
685 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
686 "Exporting symbolic models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
687 }
688 }
689
690 // TODO: The following options are depreciated and shall be removed at some point:
691
692 if (ioSettings.isExportExplicitSet()) {
693 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drn format is only supported for sparse models.");
694 }
695
696 if (ioSettings.isExportDdSet()) {
697 storm::api::exportSymbolicModelAsDrdd(model, ioSettings.getExportDdFilename());
698 }
699
700 if (ioSettings.isExportDotSet()) {
701 storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportDotFilename());
702 }
703}
704
705template<storm::dd::DdType DdType, typename ValueType>
706void exportModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
707 if (model->isSparseModel()) {
708 exportSparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input);
709 } else {
710 exportDdModel<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
711 }
712}
713
714template<storm::dd::DdType DdType, typename ValueType>
715typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
717 return model;
718}
719
720template<storm::dd::DdType DdType, typename ValueType>
721typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
723 auto ma = model->template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
724 if (!ma->isClosed()) {
725 return std::make_shared<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(ma->close());
726 } else {
727 return model;
728 }
729}
730
731template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
732std::shared_ptr<storm::models::Model<ExportValueType>> preprocessDdModelBisimulation(
733 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input,
734 storm::settings::modules::BisimulationSettings const& bisimulationSettings, ModelProcessingInformation const& mpi) {
735 STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(),
736 "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
737
738 auto quotientFormat = bisimulationSettings.getQuotientFormat();
740 bisimulationSettings.isQuotientFormatSetFromDefaultValue()) {
741 STORM_LOG_INFO("Setting bisimulation quotient format to 'sparse'.");
743 }
744 STORM_LOG_INFO("Performing bisimulation minimization...");
745 return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(
746 model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode(), quotientFormat);
747}
748
749template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
750std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
751 SymbolicInput const& input, ModelProcessingInformation const& mpi) {
753 std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
754
755 if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
756 intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
757 intermediateResult.second = true;
758 }
759
760 std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>> result;
761 auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
762 if (mpi.applyBisimulation) {
763 std::shared_ptr<storm::models::Model<ExportValueType>> newModel =
764 preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings, mpi);
765 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(newModel, true);
766 } else {
767 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(
768 symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
769 }
770
771 if (result && result->first->isSymbolicModel() && mpi.engine == storm::utility::Engine::DdSparse) {
772 // Mark as changed.
773 result->second = true;
774
775 std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel =
776 result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
777 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
778 for (auto const& property : input.properties) {
779 formulas.emplace_back(property.getRawFormula());
780 }
781 result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas);
782 STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
783 }
784
785 return *result;
786}
787
788template<storm::dd::DdType DdType, typename BuildValueType, typename ExportValueType = BuildValueType>
789std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input,
790 ModelProcessingInformation const& mpi) {
791 storm::utility::Stopwatch preprocessingWatch(true);
792
793 std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
794 if (model->isSparseModel()) {
795 result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input, mpi);
796 } else {
797 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
798 result =
799 preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input, mpi);
800 }
801
802 preprocessingWatch.stop();
803
804 if (result.second) {
805 STORM_PRINT("\nTime for model preprocessing: " << preprocessingWatch << ".\n\n");
806 }
807 return result;
808}
809
811 STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ...\n");
812}
813
814inline void printCounterexample(std::shared_ptr<storm::counterexamples::Counterexample> const& counterexample, storm::utility::Stopwatch* watch = nullptr) {
815 if (counterexample) {
816 STORM_PRINT(*counterexample << '\n');
817 if (watch) {
818 STORM_PRINT("Time for computation: " << *watch << ".\n");
819 }
820 } else {
821 STORM_PRINT(" failed.\n");
822 }
823}
824
825template<typename ValueType>
826void generateCounterexamples(std::shared_ptr<storm::models::ModelBase> const&, SymbolicInput const&) {
827 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type.");
828}
829
830template<>
831inline void generateCounterexamples<double>(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
832 typedef double ValueType;
833
834 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException,
835 "Counterexample generation is currently only supported for sparse models.");
836 auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
837 for (auto& rewModel : sparseModel->getRewardModels()) {
838 rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(), true);
839 }
840
841 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp),
842 storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models.");
843
845 if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
846 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
847 for (auto const& property : input.properties) {
848 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
850 storm::utility::Stopwatch watch(true);
851 if (useMilp) {
852 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException,
853 "Counterexample generation using MILP is currently only supported for MDPs.");
855 input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
856 } else {
857 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp),
858 storm::exceptions::NotSupportedException,
859 "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
860
861 if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) {
863 input.model.get(), sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
864 } else {
866 input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
867 }
868 }
869 watch.stop();
870 printCounterexample(counterexample, &watch);
871 }
872 } else if (counterexampleSettings.isShortestPathGenerationSet()) {
873 for (auto const& property : input.properties) {
874 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
876 storm::utility::Stopwatch watch(true);
877 STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException,
878 "Counterexample generation using shortest paths is currently only supported for DTMCs.");
880 property.getRawFormula(), counterexampleSettings.getShortestPathMaxK());
881 watch.stop();
882 printCounterexample(counterexample, &watch);
883 }
884 } else {
885 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported.");
886 }
887}
888
889template<typename ValueType>
890void printFilteredResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) {
891 if (result->isQuantitative()) {
893 STORM_PRINT(*result);
894 } else {
895 ValueType resultValue;
896 switch (ft) {
898 resultValue = result->asQuantitativeCheckResult<ValueType>().sum();
899 break;
901 resultValue = result->asQuantitativeCheckResult<ValueType>().average();
902 break;
904 resultValue = result->asQuantitativeCheckResult<ValueType>().getMin();
905 break;
907 resultValue = result->asQuantitativeCheckResult<ValueType>().getMax();
908 break;
911 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
915 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results.");
916 default:
917 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unhandled filter type.");
918 }
920 STORM_PRINT(resultValue << " (approx. " << storm::utility::convertNumber<double>(resultValue) << ")");
921 } else {
922 STORM_PRINT(resultValue);
923 }
924 }
925 } else {
926 switch (ft) {
928 STORM_PRINT(*result << '\n');
929 break;
931 STORM_PRINT(result->asQualitativeCheckResult().existsTrue());
932 break;
934 STORM_PRINT(result->asQualitativeCheckResult().forallTrue());
935 break;
937 STORM_PRINT(result->asQualitativeCheckResult().count());
938 break;
941 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported.");
946 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results.");
947 }
948 }
949 STORM_PRINT('\n');
950}
951
953 STORM_PRINT("\nModel checking property \"" << property.getName() << "\": " << *property.getRawFormula() << " ...\n");
954}
955
956template<typename ValueType>
957void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::logic::Formula const& filterStatesFormula,
958 storm::modelchecker::FilterType const& filterType, storm::utility::Stopwatch* watch = nullptr) {
959 if (result) {
960 std::stringstream ss;
961 ss << "'" << filterStatesFormula << "'";
962 STORM_PRINT((storm::utility::resources::isTerminate() ? "Result till abort" : "Result")
963 << " (for " << (filterStatesFormula.isInitialFormula() ? "initial" : ss.str()) << " states): ");
964 printFilteredResult<ValueType>(result, filterType);
965 if (watch) {
966 STORM_PRINT("Time for model checking: " << *watch << ".\n");
967 }
968 } else {
969 STORM_LOG_ERROR("Property is unsupported by selected engine/settings.\n");
970 }
971}
972
973template<typename ValueType>
974void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property,
975 storm::utility::Stopwatch* watch = nullptr) {
976 printResult<ValueType>(result, *property.getFilter().getStatesFormula(), property.getFilter().getFilterType(), watch);
977}
978
979using VerificationCallbackType = std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula,
980 std::shared_ptr<storm::logic::Formula const> const& states)>;
981using PostprocessingCallbackType = std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)>;
982
984 void operator()(std::unique_ptr<storm::modelchecker::CheckResult> const&) {
985 // Intentionally left empty.
986 }
987};
988
995template<typename ValueType>
996std::unique_ptr<storm::modelchecker::CheckResult> verifyProperty(std::shared_ptr<storm::logic::Formula const> const& formula,
997 std::shared_ptr<storm::logic::Formula const> const& statesFilter,
998 VerificationCallbackType const& verificationCallback) {
1000
1001 try {
1002 if (transformationSettings.isChainEliminationSet() && !storm::transformer::NonMarkovianChainTransformer<ValueType>::preservesFormula(*formula)) {
1003 STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states.");
1004 } else if (transformationSettings.isToDiscreteTimeModelSet()) {
1005 auto transformedFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*formula);
1006 auto transformedStatesFilter = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*statesFilter);
1007 if (transformedFormula && transformedStatesFilter) {
1008 // invoke verification algorithm on transformed formulas
1009 return verificationCallback(transformedFormula, transformedStatesFilter);
1010 } else {
1011 STORM_LOG_WARN("Property is not preserved by transformation to discrete time model.");
1012 }
1013 } else {
1014 // invoke verification algorithm on given formulas
1015 return verificationCallback(formula, statesFilter);
1016 }
1017 } catch (storm::exceptions::BaseException const& ex) {
1018 STORM_LOG_WARN("Cannot handle property: " << ex.what());
1019 }
1020 return nullptr;
1021}
1022
1029template<typename ValueType>
1030void verifyProperties(SymbolicInput const& input, VerificationCallbackType const& verificationCallback,
1031 PostprocessingCallbackType const& postprocessingCallback = PostprocessingIdentity()) {
1032 auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
1033 for (auto const& property : properties) {
1035 storm::utility::Stopwatch watch(true);
1036 auto result = verifyProperty<ValueType>(property.getRawFormula(), property.getFilter().getStatesFormula(), verificationCallback);
1037 watch.stop();
1038 if (result) {
1039 postprocessingCallback(result);
1040 }
1041 printResult<ValueType>(result, property, &watch);
1042 }
1043}
1044
1054template<typename ValueType>
1055void computeStateValues(std::string const& description, std::function<std::unique_ptr<storm::modelchecker::CheckResult>()> const& computationCallback,
1056 SymbolicInput const& input, VerificationCallbackType const& verificationCallback,
1057 PostprocessingCallbackType const& postprocessingCallback = PostprocessingIdentity()) {
1058 // First compute the state values for all the states by invoking the computationCallback
1059 storm::utility::Stopwatch watch(true);
1060 STORM_PRINT("\nComputing " << description << " ...\n");
1061 std::unique_ptr<storm::modelchecker::CheckResult> result;
1062 try {
1063 result = computationCallback();
1064 } catch (storm::exceptions::BaseException const& ex) {
1065 STORM_LOG_ERROR("Cannot compute " << description << ": " << ex.what());
1066 }
1067 if (!result) {
1068 STORM_LOG_ERROR("Computation had no result.");
1069 return;
1070 }
1071 // Now process the (potentially filtered) result
1072 if (input.properties.empty()) {
1073 // Do not apply any filtering, consider result for *all* states
1074 postprocessingCallback(result);
1075 printResult<ValueType>(result, *storm::logic::Formula::getTrueFormula(), storm::modelchecker::FilterType::VALUES, &watch);
1076 } else {
1077 // Each property identifies a subset of states to which we restrict (aka filter) the state-value result to
1078 auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
1079 for (uint64_t propertyIndex = 0; propertyIndex < properties.size(); ++propertyIndex) {
1080 auto const& property = properties[propertyIndex];
1081 // As the property serves as filter, it should (a) be qualitative and should (b) not consider a filter itself.
1082 if (!property.getRawFormula()->hasQualitativeResult()) {
1083 STORM_LOG_ERROR("Property '" << *property.getRawFormula()
1084 << "' can not be used for filtering states as it does not have a qualitative result.");
1085 continue;
1086 }
1087
1088 // Invoke verification algorithm on filtering property
1089 auto propertyFilter = verifyProperty<ValueType>(property.getRawFormula(), storm::logic::Formula::getTrueFormula(), verificationCallback);
1090
1091 if (propertyFilter) {
1092 // Filter and process result
1093 std::unique_ptr<storm::modelchecker::CheckResult> filteredResult = result->clone();
1094 filteredResult->filter(propertyFilter->asQualitativeCheckResult());
1095 postprocessingCallback(filteredResult);
1096 printResult<ValueType>(filteredResult, *property.getRawFormula(), property.getFilter().getFilterType(),
1097 propertyIndex == properties.size() - 1 ? &watch : nullptr);
1098 }
1099 }
1100 }
1101}
1102
1103inline std::vector<storm::expressions::Expression> parseConstraints(storm::expressions::ExpressionManager const& expressionManager,
1104 std::string const& constraintsString) {
1105 std::vector<storm::expressions::Expression> constraints;
1106
1107 std::vector<std::string> constraintsAsStrings;
1108 boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(","));
1109
1110 storm::parser::ExpressionParser expressionParser(expressionManager);
1111 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1112 for (auto const& variableTypePair : expressionManager) {
1113 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1114 }
1115 expressionParser.setIdentifierMapping(variableMapping);
1116
1117 for (auto const& constraintString : constraintsAsStrings) {
1118 if (constraintString.empty()) {
1119 continue;
1120 }
1121
1122 storm::expressions::Expression constraint = expressionParser.parseFromString(constraintString);
1123 STORM_LOG_TRACE("Adding special (user-provided) constraint " << constraint << ".");
1124 constraints.emplace_back(constraint);
1125 }
1126
1127 return constraints;
1128}
1129
1130inline std::vector<std::vector<storm::expressions::Expression>> parseInjectedRefinementPredicates(
1131 storm::expressions::ExpressionManager const& expressionManager, std::string const& refinementPredicatesString) {
1132 std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
1133
1134 storm::parser::ExpressionParser expressionParser(expressionManager);
1135 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1136 for (auto const& variableTypePair : expressionManager) {
1137 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1138 }
1139 expressionParser.setIdentifierMapping(variableMapping);
1140
1141 std::vector<std::string> predicateGroupsAsStrings;
1142 boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(";"));
1143
1144 if (!predicateGroupsAsStrings.empty()) {
1145 for (auto const& predicateGroupString : predicateGroupsAsStrings) {
1146 if (predicateGroupString.empty()) {
1147 continue;
1148 }
1149
1150 std::vector<std::string> predicatesAsStrings;
1151 boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(":"));
1152
1153 if (!predicatesAsStrings.empty()) {
1154 injectedRefinementPredicates.emplace_back();
1155 for (auto const& predicateString : predicatesAsStrings) {
1156 storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString);
1157 STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << ".");
1158 injectedRefinementPredicates.back().emplace_back(predicate);
1159 }
1160
1161 STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException,
1162 "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
1163
1164 // Finally reverse the list, because we take the predicates from the back.
1165 std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
1166 }
1167 }
1168
1169 // Finally reverse the list, because we take the predicates from the back.
1170 std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
1171 }
1172
1173 return injectedRefinementPredicates;
1174}
1175
1176template<storm::dd::DdType DdType, typename ValueType>
1178 STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
1181 parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()),
1182 parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
1183
1184 verifyProperties<ValueType>(input, [&input, &options, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
1185 std::shared_ptr<storm::logic::Formula const> const& states) {
1186 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
1187 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, input.model.get(),
1188 storm::api::createTask<ValueType>(formula, true), options);
1189 });
1190}
1191
1192template<typename ValueType>
1194 STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
1195 STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException,
1196 "Exploration does not support other data-types than floating points.");
1197 verifyProperties<ValueType>(
1198 input, [&input, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1199 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
1200 return storm::api::verifyWithExplorationEngine<ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true));
1201 });
1202}
1203
1204template<typename ValueType>
1205void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1206 auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
1208 auto verificationCallback = [&sparseModel, &ioSettings, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
1209 std::shared_ptr<storm::logic::Formula const> const& states) {
1210 bool filterForInitialStates = states->isInitialFormula();
1211 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1212 if (ioSettings.isExportSchedulerSet()) {
1213 task.setProduceSchedulers(true);
1214 }
1215 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, task);
1216
1217 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1218 if (filterForInitialStates) {
1219 filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
1220 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1221 filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, storm::api::createTask<ValueType>(states, false));
1222 }
1223 if (result && filter) {
1224 result->filter(filter->asQualitativeCheckResult());
1225 }
1226 return result;
1227 };
1228 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.
1229 auto postprocessingCallback = [&sparseModel, &ioSettings, &input, &exportCount](std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
1230 if (ioSettings.isExportSchedulerSet()) {
1231 if (result->isExplicitQuantitativeCheckResult()) {
1232 if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
1233 auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
1234 STORM_PRINT_AND_LOG("Exporting scheduler ... ");
1235 if (input.model) {
1236 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(),
1237 "No information of state valuations available. The scheduler output will use internal state ids. You might be "
1238 "interested in building the model with state valuations using --buildstateval.");
1240 sparseModel->hasChoiceLabeling() || sparseModel->hasChoiceOrigins(),
1241 "No symbolic choice information is available. The scheduler output will use internal choice ids. You might be interested in "
1242 "building the model with choice labels or choice origins using --buildchoicelab or --buildchoiceorig.");
1243 STORM_LOG_WARN_COND(sparseModel->hasChoiceLabeling() && !sparseModel->hasChoiceOrigins(),
1244 "Only partial choice information is available. You might want to build the model with choice origins using "
1245 "--buildchoicelab or --buildchoiceorig.");
1246 }
1247 STORM_LOG_WARN_COND(exportCount == 0,
1248 "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
1249 storm::api::exportScheduler(sparseModel, scheduler,
1250 (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportSchedulerFilename());
1251 } else {
1252 STORM_LOG_ERROR("Scheduler requested but could not be generated.");
1253 }
1254 } else {
1255 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
1256 }
1257 }
1258 if (ioSettings.isExportCheckResultSet()) {
1259 STORM_LOG_WARN_COND(sparseModel->hasStateValuations(),
1260 "No information of state valuations available. The result output will use internal state ids. You might be interested in "
1261 "building the model with state valuations using --buildstateval.");
1262 STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
1263 storm::api::exportCheckResultToJson(sparseModel, result,
1264 (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportCheckResultFilename());
1265 }
1266 ++exportCount;
1267 };
1268 if (!(ioSettings.isComputeSteadyStateDistributionSet() || ioSettings.isComputeExpectedVisitingTimesSet())) {
1269 verifyProperties<ValueType>(input, verificationCallback, postprocessingCallback);
1270 }
1271 if (ioSettings.isComputeSteadyStateDistributionSet()) {
1272 computeStateValues<ValueType>(
1273 "steady-state probabilities",
1274 [&mpi, &sparseModel]() { return storm::api::computeSteadyStateDistributionWithSparseEngine<ValueType>(mpi.env, sparseModel); }, input,
1275 verificationCallback, postprocessingCallback);
1276 }
1277 if (ioSettings.isComputeExpectedVisitingTimesSet()) {
1278 computeStateValues<ValueType>(
1279 "expected visiting times",
1280 [&mpi, &sparseModel]() { return storm::api::computeExpectedVisitingTimesWithSparseEngine<ValueType>(mpi.env, sparseModel); }, input,
1281 verificationCallback, postprocessingCallback);
1282 }
1283}
1284
1285template<storm::dd::DdType DdType, typename ValueType>
1286void verifyWithHybridEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1287 verifyProperties<ValueType>(
1288 input, [&model, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1289 bool filterForInitialStates = states->isInitialFormula();
1290 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1291
1292 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
1293 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.env, symbolicModel, task);
1294
1295 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1296 if (filterForInitialStates) {
1297 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1298 symbolicModel->getInitialStates());
1299 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1300 filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(states, false));
1301 }
1302 if (result && filter) {
1303 result->filter(filter->asQualitativeCheckResult());
1304 }
1305 return result;
1306 });
1307}
1308
1309template<storm::dd::DdType DdType, typename ValueType>
1310void verifyWithDdEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1311 verifyProperties<ValueType>(
1312 input, [&model, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1313 bool filterForInitialStates = states->isInitialFormula();
1314 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1315
1316 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
1317 std::unique_ptr<storm::modelchecker::CheckResult> result =
1318 storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(formula, true));
1319
1320 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1321 if (filterForInitialStates) {
1322 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1323 symbolicModel->getInitialStates());
1324 } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
1325 filter = storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.env, symbolicModel, storm::api::createTask<ValueType>(states, false));
1326 }
1327 if (result && filter) {
1328 result->filter(filter->asQualitativeCheckResult());
1329 }
1330 return result;
1331 });
1332}
1333
1334template<storm::dd::DdType DdType, typename ValueType>
1335void verifyWithAbstractionRefinementEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input,
1336 ModelProcessingInformation const& mpi) {
1337 verifyProperties<ValueType>(
1338 input, [&model, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
1339 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
1340 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
1341 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, symbolicModel,
1342 storm::api::createTask<ValueType>(formula, true));
1343 });
1344}
1345
1346template<storm::dd::DdType DdType, typename ValueType>
1347typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(
1348 std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1350 verifyWithHybridEngine<DdType, ValueType>(model, input, mpi);
1351 } else if (mpi.engine == storm::utility::Engine::Dd) {
1352 verifyWithDdEngine<DdType, ValueType>(model, input, mpi);
1353 } else {
1354 verifyWithAbstractionRefinementEngine<DdType, ValueType>(model, input, mpi);
1355 }
1356}
1357
1358template<storm::dd::DdType DdType, typename ValueType>
1359typename std::enable_if<DdType == storm::dd::DdType::CUDD && !std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(
1360 std::shared_ptr<storm::models::ModelBase> const&, SymbolicInput const&, ModelProcessingInformation const&) {
1361 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type.");
1362}
1363
1364template<storm::dd::DdType DdType, typename ValueType>
1365void verifyModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1366 if (model->isSparseModel()) {
1367 verifyWithSparseEngine<ValueType>(model, input, mpi);
1368 } else {
1369 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
1370 verifySymbolicModel<DdType, ValueType>(model, input, mpi);
1371 }
1372}
1373
1374template<storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
1375std::shared_ptr<storm::models::ModelBase> buildPreprocessModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1378 std::shared_ptr<storm::models::ModelBase> model;
1379 if (!buildSettings.isNoBuildModelSet()) {
1380 model = buildModel<DdType, BuildValueType>(input, ioSettings, mpi);
1381 }
1382
1383 if (model) {
1384 model->printModelInformationToStream(std::cout);
1385 }
1386
1387 STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
1388
1389 if (model) {
1390 auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input, mpi);
1391 if (preprocessingResult.second) {
1392 model = preprocessingResult.first;
1393 model->printModelInformationToStream(std::cout);
1394 }
1395 }
1396 return model;
1397}
1398
1399template<storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
1400std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
1401 auto model = buildPreprocessModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
1402 if (model) {
1403 exportModel<DdType, BuildValueType>(model, input);
1404 }
1405 return model;
1406}
1407
1408template<storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
1412
1413 // For several engines, no model building step is performed, but the verification is started right away.
1415 abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
1416 verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input, mpi);
1417 } else if (mpi.engine == storm::utility::Engine::Exploration) {
1418 verifyWithExplorationEngine<VerificationValueType>(input, mpi);
1419 } else {
1420 std::shared_ptr<storm::models::ModelBase> model =
1421 buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
1422 if (model) {
1423 if (counterexampleSettings.isCounterexampleSet()) {
1424 generateCounterexamples<VerificationValueType>(model, input);
1425 } else {
1426 verifyModel<DdType, VerificationValueType>(model, input, mpi);
1427 }
1428 }
1429 }
1430}
1431
1432template<typename ValueType>
1434 if (mpi.ddType == storm::dd::DdType::CUDD) {
1436 mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && (std::is_same<ValueType, double>::value),
1437 "Unexpected value type for Dd library cudd.");
1438 processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input, mpi);
1439 } else {
1440 STORM_LOG_ASSERT(mpi.ddType == storm::dd::DdType::Sylvan, "Unknown DD library.");
1441 if (mpi.buildValueType == mpi.verificationValueType) {
1442 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input, mpi);
1443 } else {
1444 // Right now, we only require (buildType == Exact and verificationType == FinitePrecision).
1445 // We exclude all other combinations to safe a few template instantiations.
1446 STORM_LOG_THROW((std::is_same<ValueType, double>::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact,
1447 storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType");
1448#ifdef STORM_HAVE_CARL
1449 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input, mpi);
1450#else
1451 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unexpected buildValueType.");
1452#endif
1453 }
1454 }
1455}
1456} // namespace cli
1457} // 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 void reduceToStateBasedRewards()=0
Converts the transition rewards of all reward models to state-based rewards.
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:33
Base class for all symbolic models.
Definition Model.h:46
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:2321
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:29
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_ERROR(message)
Definition logging.h:31
#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:62
void exportSymbolicModelAsDot(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)
Definition export.h:57
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:36
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:25
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:76
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:49
void exportSparseModelAsDot(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, size_t maxWidth=30)
Definition export.h:41
std::vector< storm::jani::Property > substituteConstantsInProperties(std::vector< storm::jani::Property > const &properties, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)
void exportSymbolicInput(SymbolicInput const &input)
void parseSymbolicModelDescription(storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input)
void verifyWithAbstractionRefinementEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void generateCounterexamples< double >(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)
std::shared_ptr< storm::models::ModelBase > buildModelExplicit(storm::settings::modules::IOSettings const &ioSettings, storm::settings::modules::BuildSettings const &buildSettings)
std::shared_ptr< storm::models::ModelBase > buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > buildPreprocessModelWithValueTypeAndDdlib(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void verifyModel(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const &ioSettings)
void getModelProcessingInformationAutomatic(SymbolicInput const &input, ModelProcessingInformation &mpi)
void verifyWithExplorationEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void exportModel(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)
void verifyProperties(SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
Verifies all (potentially preprocessed) properties given in input.
void printFilteredResult(std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::modelchecker::FilterType ft)
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()
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessDdModel(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
void verifyWithSparseEngine(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
void exportSparseModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
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::ModelBase > buildModel(SymbolicInput const &input, storm::settings::modules::IOSettings const &ioSettings, ModelProcessingInformation const &mpi)
void processInputWithValueType(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseMarkovAutomaton(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &model)
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)
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)
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::ModelBase > const &model, 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)
void processInputWithValueTypeAndDdlib(SymbolicInput const &input, ModelProcessingInformation const &mpi)
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)
std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> PostprocessingCallbackType
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, bool > preprocessSparseModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::enable_if< DdType!=storm::dd::DdType::CUDD||std::is_same< ValueType, double >::value, void >::type verifySymbolicModel(std::shared_ptr< storm::models::ModelBase > const &model, 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)
void generateCounterexamples(std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &)
void exportDdModel(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &)
storm::builder::BuilderOptions createBuildOptionsSparseFromSettings(SymbolicInput const &input)
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessModel(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
void ensureNoUndefinedPropertyConstants(std::vector< storm::jani::Property > const &properties)
std::vector< std::shared_ptr< storm::logic::Formula const > > createFormulasToRespect(std::vector< storm::jani::Property > const &properties)
std::shared_ptr< storm::models::ModelBase > buildModelDd(SymbolicInput const &input)
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...
void verifyWithDdEngine(std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::string toString(ModelExportFormat const &input)
SettingsType const & getModule()
Get module.
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.
Definition cli.cpp:18
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