61 boost::optional<storm::storage::SymbolicModelDescription>
model;
78 boost::optional<std::vector<std::string>> propertyFilter;
83 propertyFilter = boost::none;
86 propertyFilter = std::vector<std::string>();
89 input.
model = std::move(janiInput.first);
91 input.
properties = std::move(janiInput.second);
94 modelParsingWatch.
stop();
95 STORM_PRINT(
"Time for model input parsing: " << modelParsingWatch <<
".\n\n");
100 boost::optional<std::set<std::string>>
const& propertyFilter) {
102 std::vector<storm::jani::Property> newProperties;
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");
131 input.
model = input.
model.get().preprocess(constantDefinitions);
141 if (ioSettings.isQvbsInputSet()) {
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 =
187 STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException,
"Automatic engine requires a property.");
189 "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered.");
192 if (hints.isNumberStatesSet()) {
193 as.
predict(input.
model->asJaniModel(), properties.front(), hints.getNumberStates());
195 as.
predict(input.
model->asJaniModel(), properties.front());
216 std::shared_ptr<SymbolicInput>
const& transformedJaniInput =
nullptr) {
224 mpi.
engine = coreSettings.getEngine();
230 if (generalSettings.isParametricSet()) {
232 }
else if (generalSettings.isExactSet()) {
242 if (input.
model->isJaniModel()) {
253 janiInput.
model = modelAndProperties.first;
254 if (!modelAndProperties.second.empty()) {
260 if (transformedJaniInput) {
262 *transformedJaniInput = std::move(janiInput);
269 auto checkCompatibleSettings = [&mpi, &input] {
288 STORM_LOG_WARN(
"The settings picked by the automatic engine (engine="
290 <<
") are incompatible with this model. Falling back to default settings.");
310 "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.");
316 if (bisimulationSettings.useExactArithmeticInDdBisimulation()) {
322 STORM_LOG_WARN(
"Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied.");
327 mpi.
ddType = coreSettings.getDdLibraryType();
331 STORM_LOG_INFO(
"Switching to DD library sylvan to allow for rational arithmetic.");
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());
348 false, storm::exceptions::InvalidArgumentException,
349 "The property '" << property <<
" still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames,
",") <<
".");
360 if (ioSettings.isPropertiesAsMultiSet()) {
362 "Can not translate properties to multi-objective formula because no properties were specified.");
367 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
368 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
370 constantDefinitions = output.
model.get().parseConstantDefinitions(constantDefinitionString);
371 output.
model = output.
model.get().preprocess(constantDefinitions);
377 auto transformedJani = std::make_shared<SymbolicInput>();
381 if (output.
model && output.
model.get().isPrismProgram()) {
383 if (transformedJani->model) {
385 output = std::move(*transformedJani);
390 output.
model = modelAndProperties.first;
392 if (!modelAndProperties.second.empty()) {
399 if (output.
model && output.
model.get().isJaniModel()) {
404 if (buildSettings.isLocationEliminationSet()) {
405 auto locationHeuristic = buildSettings.getLocationEliminationLocationHeuristic();
406 auto edgesHeuristic = buildSettings.getLocationEliminationEdgesHeuristic();
408 locationHeuristic, edgesHeuristic));
412 return {output, mpi};
417 if (input.
model && input.
model.get().isJaniModel()) {
419 if (ioSettings.isExportJaniDotSet()) {
425inline std::vector<std::shared_ptr<storm::logic::Formula const>>
createFormulasToRespect(std::vector<storm::jani::Property>
const& properties) {
428 for (
auto const& property : properties) {
429 if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
430 result.push_back(property.getFilter().getStatesFormula());
437template<storm::dd::DdType DdType,
typename ValueType>
445 !buildSettings.isApplyNoMaximumProgressAssumptionSet());
458 if (counterexampleGeneratorSettings.isCounterexampleSet()) {
459 buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet();
464 if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) {
468 if (buildSettings.isExplorationChecksSet()) {
474 if (buildSettings.isBuildFullModelSet()) {
481 if (buildSettings.isAddOverlappingGuardsLabelSet()) {
486 if (ioSettings.isComputeExpectedVisitingTimesSet() || ioSettings.isComputeSteadyStateDistributionSet()) {
492template<
typename ValueType>
494 return storm::api::buildSparseModel<ValueType>(input.
model.get(), options);
497template<
typename ValueType>
500 std::shared_ptr<storm::models::ModelBase> result;
502 result = storm::api::buildExplicitModel<ValueType>(
518template<storm::dd::DdType DdType,
typename ValueType>
523 std::shared_ptr<storm::models::ModelBase> result;
527 result = buildModelDd<DdType, ValueType>(input);
530 result = buildModelSparse<ValueType>(input, options);
534 "Can only use sparse engine with explicit input.");
538 modelBuildingWatch.
stop();
540 STORM_PRINT(
"Time for model construction: " << modelBuildingWatch <<
".\n\n");
546template<
typename ValueType>
552 std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
555 "MA contains a Zeno cycle. Model checking results cannot be trusted.");
557 if (model->isConvertibleToCtmc()) {
559 result = model->convertToCtmc();
562 if (transformationSettings.isChainEliminationSet()) {
565 transformationSettings.getLabelBehavior())
572template<
typename ValueType>
585template<
typename ValueType>
592 std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>,
bool> result = std::make_pair(model,
false);
594 if (
auto order = transformationSettings.getModelPermutation(); order.has_value()) {
595 auto seed = transformationSettings.getModelPermutationSeed();
597 << (seed.has_value() ?
" with seed " + std::to_string(seed.value()) :
"") <<
".\n");
599 result.second =
true;
600 STORM_PRINT_AND_LOG(
"Transition matrix hash after permuting: " << result.first->getTransitionMatrix().hash() <<
".\n");
605 result.second =
true;
610 result.second =
true;
613 if (transformationSettings.isToDiscreteTimeModelSet()) {
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.");
621 result.second =
true;
624 if (transformationSettings.isToNondeterministicModelSet()) {
625 result.first = storm::api::transformToNondeterministicModel<ValueType>(std::move(*result.first));
626 result.second =
true;
632template<
typename ValueType>
636 if (ioSettings.isExportBuildSet()) {
637 switch (ioSettings.getExportBuildFormat()) {
643 input.
model ? input.
model.get().getParameterNames() : std::vector<std::string>(),
644 !ioSettings.isExplicitExportPlaceholdersDisabled());
651 "Exporting sparse models in " <<
storm::io::toString(ioSettings.getExportBuildFormat()) <<
" format is not supported.");
657 if (ioSettings.isExportExplicitSet()) {
659 input.
model ? input.
model.get().getParameterNames() : std::vector<std::string>(),
660 !ioSettings.isExplicitExportPlaceholdersDisabled());
663 if (ioSettings.isExportDdSet()) {
664 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Exporting in drdd format is only supported for DDs.");
667 if (ioSettings.isExportDotSet()) {
672template<storm::dd::DdType DdType,
typename ValueType>
676 if (ioSettings.isExportBuildSet()) {
677 switch (ioSettings.getExportBuildFormat()) {
686 "Exporting symbolic models in " <<
storm::io::toString(ioSettings.getExportBuildFormat()) <<
" format is not supported.");
692 if (ioSettings.isExportExplicitSet()) {
693 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Exporting in drn format is only supported for sparse models.");
696 if (ioSettings.isExportDdSet()) {
700 if (ioSettings.isExportDotSet()) {
705template<storm::dd::DdType DdType,
typename ValueType>
707 if (model->isSparseModel()) {
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
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());
731template<storm::dd::DdType DdType,
typename ValueType,
typename ExportValueType = ValueType>
736 "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
741 STORM_LOG_INFO(
"Setting bisimulation quotient format to 'sparse'.");
745 return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(
749template<storm::dd::DdType DdType,
typename ValueType,
typename ExportValueType = ValueType>
753 std::pair<std::shared_ptr<storm::models::Model<ValueType>>,
bool> intermediateResult = std::make_pair(model,
false);
757 intermediateResult.second =
true;
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>>();
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);
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);
773 result->second =
true;
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());
782 STORM_LOG_THROW(result, storm::exceptions::NotSupportedException,
"The translation to a sparse model is not supported for the given model type.");
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,
793 std::pair<std::shared_ptr<storm::models::ModelBase>,
bool> result = std::make_pair(model,
false);
794 if (model->isSparseModel()) {
802 preprocessingWatch.
stop();
805 STORM_PRINT(
"\nTime for model preprocessing: " << preprocessingWatch <<
".\n\n");
815 if (counterexample) {
818 STORM_PRINT(
"Time for computation: " << *watch <<
".\n");
825template<
typename ValueType>
827 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Counterexample generation is not supported for this data-type.");
832 typedef double ValueType;
834 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException,
835 "Counterexample generation is currently only supported for sparse models.");
837 for (
auto& rewModel : sparseModel->getRewardModels()) {
842 storm::exceptions::NotSupportedException,
"Counterexample is currently only supported for discrete-time models.");
845 if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
846 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
847 for (
auto const& property : input.
properties) {
848 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
853 "Counterexample generation using MILP is currently only supported for MDPs.");
858 storm::exceptions::NotSupportedException,
859 "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
872 }
else if (counterexampleSettings.isShortestPathGenerationSet()) {
873 for (
auto const& property : input.
properties) {
874 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
878 "Counterexample generation using shortest paths is currently only supported for DTMCs.");
880 property.getRawFormula(), counterexampleSettings.getShortestPathMaxK());
885 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The selected counterexample formalism is unsupported.");
889template<
typename ValueType>
891 if (result->isQuantitative()) {
895 ValueType resultValue;
898 resultValue = result->asQuantitativeCheckResult<ValueType>().sum();
901 resultValue = result->asQuantitativeCheckResult<ValueType>().average();
904 resultValue = result->asQuantitativeCheckResult<ValueType>().getMin();
907 resultValue = result->asQuantitativeCheckResult<ValueType>().getMax();
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.");
917 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"Unhandled filter type.");
920 STORM_PRINT(resultValue <<
" (approx. " << storm::utility::convertNumber<double>(resultValue) <<
")");
931 STORM_PRINT(result->asQualitativeCheckResult().existsTrue());
934 STORM_PRINT(result->asQualitativeCheckResult().forallTrue());
937 STORM_PRINT(result->asQualitativeCheckResult().count());
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.");
956template<
typename ValueType>
960 std::stringstream ss;
961 ss <<
"'" << filterStatesFormula <<
"'";
963 <<
" (for " << (filterStatesFormula.isInitialFormula() ?
"initial" : ss.str()) <<
" states): ");
964 printFilteredResult<ValueType>(result, filterType);
966 STORM_PRINT(
"Time for model checking: " << *watch <<
".\n");
969 STORM_LOG_ERROR(
"Property is unsupported by selected engine/settings.\n");
973template<
typename ValueType>
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)>;
984 void operator()(std::unique_ptr<storm::modelchecker::CheckResult>
const&) {
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,
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) {
1009 return verificationCallback(transformedFormula, transformedStatesFilter);
1011 STORM_LOG_WARN(
"Property is not preserved by transformation to discrete time model.");
1015 return verificationCallback(formula, statesFilter);
1029template<
typename ValueType>
1033 for (
auto const& property : properties) {
1036 auto result = verifyProperty<ValueType>(property.getRawFormula(), property.getFilter().getStatesFormula(), verificationCallback);
1039 postprocessingCallback(result);
1041 printResult<ValueType>(result, property, &watch);
1054template<
typename ValueType>
1055void computeStateValues(std::string
const& description, std::function<std::unique_ptr<storm::modelchecker::CheckResult>()>
const& computationCallback,
1060 STORM_PRINT(
"\nComputing " << description <<
" ...\n");
1061 std::unique_ptr<storm::modelchecker::CheckResult> result;
1063 result = computationCallback();
1074 postprocessingCallback(result);
1079 for (uint64_t propertyIndex = 0; propertyIndex < properties.size(); ++propertyIndex) {
1080 auto const&
property = properties[propertyIndex];
1082 if (!property.getRawFormula()->hasQualitativeResult()) {
1084 <<
"' can not be used for filtering states as it does not have a qualitative result.");
1091 if (propertyFilter) {
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);
1104 std::string
const& constraintsString) {
1105 std::vector<storm::expressions::Expression> constraints;
1107 std::vector<std::string> constraintsAsStrings;
1108 boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(
","));
1111 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1112 for (
auto const& variableTypePair : expressionManager) {
1113 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1117 for (
auto const& constraintString : constraintsAsStrings) {
1118 if (constraintString.empty()) {
1123 STORM_LOG_TRACE(
"Adding special (user-provided) constraint " << constraint <<
".");
1124 constraints.emplace_back(constraint);
1132 std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
1135 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1136 for (
auto const& variableTypePair : expressionManager) {
1137 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1141 std::vector<std::string> predicateGroupsAsStrings;
1142 boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(
";"));
1144 if (!predicateGroupsAsStrings.empty()) {
1145 for (
auto const& predicateGroupString : predicateGroupsAsStrings) {
1146 if (predicateGroupString.empty()) {
1150 std::vector<std::string> predicatesAsStrings;
1151 boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(
":"));
1153 if (!predicatesAsStrings.empty()) {
1154 injectedRefinementPredicates.emplace_back();
1155 for (
auto const& predicateString : predicatesAsStrings) {
1157 STORM_LOG_TRACE(
"Adding special (user-provided) refinement predicate " << predicateString <<
".");
1158 injectedRefinementPredicates.back().emplace_back(predicate);
1161 STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException,
1162 "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
1165 std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
1170 std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
1173 return injectedRefinementPredicates;
1176template<storm::dd::DdType DdType,
typename ValueType>
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);
1192template<
typename ValueType>
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));
1204template<
typename 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);
1215 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(mpi.
env, sparseModel, task);
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()) {
1221 filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.
env, sparseModel, storm::api::createTask<ValueType>(states,
false));
1223 if (result && filter) {
1224 result->filter(filter->asQualitativeCheckResult());
1228 uint64_t exportCount = 0;
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();
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.");
1244 "Only partial choice information is available. You might want to build the model with choice origins using "
1245 "--buildchoicelab or --buildchoiceorig.");
1248 "Prepending " << exportCount <<
" to file name for this property because there are multiple properties.");
1250 (exportCount == 0 ? std::string(
"") : std::to_string(exportCount)) + ioSettings.getExportSchedulerFilename());
1255 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Scheduler export not supported for this property.");
1258 if (ioSettings.isExportCheckResultSet()) {
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.");
1264 (exportCount == 0 ? std::string(
"") : std::to_string(exportCount)) + ioSettings.getExportCheckResultFilename());
1268 if (!(ioSettings.isComputeSteadyStateDistributionSet() || ioSettings.isComputeExpectedVisitingTimesSet())) {
1269 verifyProperties<ValueType>(input, verificationCallback, postprocessingCallback);
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);
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);
1285template<storm::dd::DdType DdType,
typename ValueType>
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);
1293 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.
env, symbolicModel, task);
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()) {
1300 filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(states,
false));
1302 if (result && filter) {
1303 result->filter(filter->asQualitativeCheckResult());
1309template<storm::dd::DdType DdType,
typename ValueType>
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);
1317 std::unique_ptr<storm::modelchecker::CheckResult> result =
1318 storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(formula,
true));
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()) {
1325 filter = storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(states,
false));
1327 if (result && filter) {
1328 result->filter(filter->asQualitativeCheckResult());
1334template<storm::dd::DdType DdType,
typename ValueType>
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.");
1341 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.
env, symbolicModel,
1342 storm::api::createTask<ValueType>(formula,
true));
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(
1350 verifyWithHybridEngine<DdType, ValueType>(model, input, mpi);
1352 verifyWithDdEngine<DdType, ValueType>(model, input, mpi);
1354 verifyWithAbstractionRefinementEngine<DdType, ValueType>(model, input, mpi);
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(
1361 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"CUDD does not support the selected data-type.");
1364template<storm::dd::DdType DdType,
typename ValueType>
1366 if (model->isSparseModel()) {
1367 verifyWithSparseEngine<ValueType>(model, input, mpi);
1370 verifySymbolicModel<DdType, ValueType>(model, input, mpi);
1374template<storm::dd::DdType DdType,
typename BuildValueType,
typename VerificationValueType = BuildValueType>
1378 std::shared_ptr<storm::models::ModelBase> model;
1379 if (!buildSettings.isNoBuildModelSet()) {
1380 model = buildModel<DdType, BuildValueType>(input, ioSettings, mpi);
1384 model->printModelInformationToStream(std::cout);
1390 auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input, mpi);
1391 if (preprocessingResult.second) {
1392 model = preprocessingResult.first;
1393 model->printModelInformationToStream(std::cout);
1399template<storm::dd::DdType DdType,
typename BuildValueType,
typename VerificationValueType = BuildValueType>
1401 auto model = buildPreprocessModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
1403 exportModel<DdType, BuildValueType>(model, input);
1408template<storm::dd::DdType DdType,
typename BuildValueType,
typename VerificationValueType = BuildValueType>
1416 verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input, mpi);
1418 verifyWithExplorationEngine<VerificationValueType>(input, mpi);
1420 std::shared_ptr<storm::models::ModelBase> model =
1421 buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
1423 if (counterexampleSettings.isCounterexampleSet()) {
1424 generateCounterexamples<VerificationValueType>(model, input);
1426 verifyModel<DdType, VerificationValueType>(model, input, mpi);
1432template<
typename ValueType>
1437 "Unexpected value type for Dd library cudd.");
1438 processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input, mpi);
1442 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input, mpi);
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);
1451 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"Unexpected buildValueType.");
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.
void clearTerminalStates()
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?
bool isBuildStateValuationsSet() const
BuilderOptions & setBuildAllRewardModels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
bool isBuildChoiceLabelsSet() const
bool isBuildChoiceOriginsSet() const
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?
bool isBuildAllLabelsSet() const
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.
bool isBuildObservationValuationsSet() const
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
storm::modelchecker::FilterType getFilterType() const
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
std::string const & getName() const
Get the provided name.
FilterExpression const & getFilter() const
virtual void reduceToStateBasedRewards()=0
Converts the transition rewards of all reward models to state-based rewards.
This class represents a discrete-time Markov chain.
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
Base class for all sparse models.
Base class for all symbolic models.
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.
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.
static const std::string moduleName
This class represents the markov chain settings.
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://...
std::string const & getJaniFile(uint64_t instanceIndex=0) const
std::string getInfo(uint64_t instanceIndex=0, boost::optional< std::vector< std::string > > propertyFilter=boost::none) const
std::string const & getConstantDefinition(uint64_t instanceIndex=0) const
storm::jani::Model const & asJaniModel() const
bool enableBisimulation() const
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.
void stop()
Stop stopwatch and add measured time to total time.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ERROR(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_PRINT_AND_LOG(message)
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
void exportScheduler(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::storage::Scheduler< ValueType > const &scheduler, std::string const &filename)
void exportSymbolicModelAsDot(std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)
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)
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)
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)
void exportSparseModelAsDrn(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, std::vector< std::string > const ¶meterNames={}, bool allowPlaceholders=true)
void exportCheckResultToJson(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > const &checkResult, std::string const &filename)
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)
void exportSparseModelAsDot(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, size_t maxWidth=30)
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 &)
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)
Engine
An enumeration of all engines.
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.
void operator()(std::unique_ptr< storm::modelchecker::CheckResult > const &)