64 boost::optional<storm::storage::SymbolicModelDescription>
model;
74 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
81 boost::optional<std::vector<std::string>> propertyFilter;
86 propertyFilter = boost::none;
89 propertyFilter = std::vector<std::string>();
92 input.
model = std::move(janiInput.first);
94 input.
properties = std::move(janiInput.second);
97 modelParsingWatch.
stop();
98 STORM_PRINT(
"Time for model input parsing: " << modelParsingWatch <<
".\n\n");
103 boost::optional<std::set<std::string>>
const& propertyFilter) {
105 std::vector<storm::jani::Property> newProperties;
123 input.
model = std::move(janiInput.first);
124 input.
properties = std::move(janiInput.second);
125 modelParsingWatch.
stop();
126 STORM_PRINT(
"Time for model input parsing: " << modelParsingWatch <<
".\n\n");
134 input.
model = input.
model.get().preprocess(constantDefinitions);
143 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
144 if (ioSettings.isQvbsInputSet()) {
184 auto hints = storm::settings::getModule<storm::settings::modules::HintSettings>();
186 STORM_LOG_THROW(input.
model.is_initialized(), storm::exceptions::InvalidArgumentException,
"Automatic engine requires a JANI input model.");
187 STORM_LOG_THROW(input.
model->isJaniModel(), storm::exceptions::InvalidArgumentException,
"Automatic engine requires a JANI input model.");
188 std::vector<storm::jani::Property>
const& properties =
190 STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException,
"Automatic engine requires a property.");
192 "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered.");
195 if (hints.isNumberStatesSet()) {
196 as.
predict(input.
model->asJaniModel(), properties.front(), hints.getNumberStates());
198 as.
predict(input.
model->asJaniModel(), properties.front());
219 std::shared_ptr<SymbolicInput>
const& transformedJaniInput =
nullptr) {
221 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
222 auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
223 auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
224 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
227 mpi.
engine = coreSettings.getEngine();
233 if (generalSettings.isParametricSet()) {
235 }
else if (generalSettings.isExactSet()) {
245 if (input.
model->isJaniModel()) {
256 janiInput.
model = modelAndProperties.first;
257 if (!modelAndProperties.second.empty()) {
263 if (transformedJaniInput) {
265 *transformedJaniInput = std::move(janiInput);
272 auto checkCompatibleSettings = [&mpi, &input] {
291 STORM_LOG_WARN(
"The settings picked by the automatic engine (engine="
293 <<
") are incompatible with this model. Falling back to default settings.");
313 "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.");
319 if (bisimulationSettings.useExactArithmeticInDdBisimulation()) {
325 STORM_LOG_WARN(
"Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied.");
330 mpi.
ddType = coreSettings.getDdLibraryType();
334 STORM_LOG_INFO(
"Switching to DD library sylvan to allow for rational arithmetic.");
341auto castAndApply(std::shared_ptr<storm::models::ModelBase>
const& model,
auto const& callback) {
345 auto castAndApplyImpl = [&model, &callback]<
typename TargetModelType> {
346 auto res = model->template as<TargetModelType>();
348 return callback(res);
352 auto castAndApplyVT = [&]<
typename ValueType> {
353 if (model->isSparseModel()) {
357 STORM_LOG_ASSERT(model->isSymbolicModel() && ddType.has_value(),
"Unexpected model representation");
358 if constexpr (storm::IsIntervalType<ValueType>) {
360 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Symbolic interval models are currently not supported.");
363 if (*ddType == CUDD) {
364 if constexpr (std::is_same_v<ValueType, double>) {
375 if (model->supportsParameters()) {
377 }
else if (model->isExact()) {
378 return castAndApplyVT.template operator()<storm::RationalNumber>();
379 }
else if (model->supportsUncertainty()) {
382 return castAndApplyVT.template operator()<
double>();
389 case FinitePrecision:
390 return callback.template operator()<
double>();
392 return callback.template operator()<storm::RationalNumber>();
396 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException,
"Unexpected value type.");
404 STORM_LOG_THROW(vt == FinitePrecision, storm::exceptions::UnexpectedException,
"Unexpected value type for DD library Cudd.");
405 return callback.template operator()<CUDD,
double>();
408 case FinitePrecision:
409 return callback.template operator()<
Sylvan,
double>();
411 return callback.template operator()<
Sylvan, storm::RationalNumber>();
416 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException,
"Unexpected DDType or value type.");
421 for (
auto const& property : properties) {
422 std::set<storm::expressions::Variable> usedUndefinedConstants =
property.getUndefinedConstants();
423 if (!usedUndefinedConstants.empty()) {
424 std::vector<std::string> undefinedConstantsNames;
425 for (
auto const& constant : usedUndefinedConstants) {
426 undefinedConstantsNames.emplace_back(constant.getName());
429 false, storm::exceptions::InvalidArgumentException,
430 "The property '" << property <<
" still refers to the undefined constants " << boost::algorithm::join(undefinedConstantsNames,
",") <<
".");
436 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
441 if (ioSettings.isPropertiesAsMultiSet()) {
443 "Can not translate properties to multi-objective formula because no properties were specified.");
448 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
449 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
451 constantDefinitions = output.
model.get().parseConstantDefinitions(constantDefinitionString);
452 output.
model = output.
model.get().preprocess(constantDefinitions);
458 auto transformedJani = std::make_shared<SymbolicInput>();
462 if (output.
model && output.
model.get().isPrismProgram()) {
464 if (transformedJani->model) {
466 output = std::move(*transformedJani);
471 output.
model = modelAndProperties.first;
473 if (!modelAndProperties.second.empty()) {
480 if (output.
model && output.
model.get().isJaniModel()) {
484 const auto& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
485 if (buildSettings.isLocationEliminationSet()) {
486 auto locationHeuristic = buildSettings.getLocationEliminationLocationHeuristic();
487 auto edgesHeuristic = buildSettings.getLocationEliminationEdgesHeuristic();
489 locationHeuristic, edgesHeuristic));
493 return {output, mpi};
497 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
498 if (input.
model && input.
model.get().isJaniModel()) {
500 if (ioSettings.isExportJaniDotSet()) {
506inline std::vector<std::shared_ptr<storm::logic::Formula const>>
createFormulasToRespect(std::vector<storm::jani::Property>
const& properties) {
509 for (
auto const& property : properties) {
510 if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
511 result.push_back(property.getFilter().getStatesFormula());
518template<storm::dd::DdType DdType,
typename ValueType>
521 auto numThreads = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads();
524 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
526 !buildSettings.isApplyNoMaximumProgressAssumptionSet());
530 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
538 auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
539 if (counterexampleGeneratorSettings.isCounterexampleSet()) {
540 buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet();
545 if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) {
549 if (buildSettings.isExplorationChecksSet()) {
555 if (buildSettings.isBuildFullModelSet()) {
562 if (buildSettings.isAddOverlappingGuardsLabelSet()) {
566 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
567 if (ioSettings.isComputeExpectedVisitingTimesSet() || ioSettings.isComputeSteadyStateDistributionSet()) {
573template<
typename ValueType>
576 if (!storm::IsIntervalType<ValueType> && input.
model.is_initialized() && input.
model->isPrismProgram() &&
577 input.
model->asPrismProgram().hasIntervalUpdates()) {
579 "Can not build interval model for the provided value type.");
580 return storm::api::buildSparseModel<storm::Interval>(input.
model.get(), options);
582 return storm::api::buildSparseModel<ValueType>(input.
model.get(), options);
586template<
typename ValueType>
589 std::shared_ptr<storm::models::ModelBase> result;
591 result = storm::api::buildExplicitModel<ValueType>(
611 std::shared_ptr<storm::models::ModelBase> result;
618 auto options = createBuildOptionsSparseFromSettings(input);
619 return buildModelSparse<VT>(input, options);
624 "Can only use sparse engine with explicit input.");
626 return buildModelExplicit<VT>(ioSettings, storm::settings::getModule<storm::settings::modules::BuildSettings>());
630 modelBuildingWatch.
stop();
632 STORM_PRINT(
"Time for model construction: " << modelBuildingWatch <<
".\n\n");
638template<
typename ValueType>
641 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
642 auto debugSettings = storm::settings::getModule<storm::settings::modules::DebugSettings>();
644 std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
647 "MA contains a Zeno cycle. Model checking results cannot be trusted.");
649 if (model->isConvertibleToCtmc()) {
651 result = model->convertToCtmc();
654 if (transformationSettings.isChainEliminationSet()) {
655 if constexpr (storm::IsIntervalType<ValueType>) {
657 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Chain elimination not supported for interval models.");
661 transformationSettings.getLabelBehavior())
669template<
typename ValueType>
682template<
typename ValueType>
686 "Converting value types for sparse engine is not supported.");
687 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
688 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
689 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
691 std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>,
bool> result = std::make_pair(model,
false);
693 if (
auto order = transformationSettings.getModelPermutation(); order.has_value()) {
694 auto seed = transformationSettings.getModelPermutationSeed();
696 << (seed.has_value() ?
" with seed " + std::to_string(seed.value()) :
"") <<
".\n");
698 result.second =
true;
699 STORM_PRINT_AND_LOG(
"Transition matrix hash after permuting: " << result.first->getTransitionMatrix().hash() <<
".\n");
704 result.second =
true;
708 if constexpr (storm::IsIntervalType<ValueType>) {
709 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Bisimulation not supported for interval models.");
712 result.second =
true;
716 if (transformationSettings.isToDiscreteTimeModelSet()) {
717 if constexpr (storm::IsIntervalType<ValueType>) {
718 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Transformation to discrete time model not supported for interval models.");
722 !model->hasRewardModel(
"_time"),
723 "Scheduled transformation to discrete time model, but a reward model named '_time' is already present in this model. We might take "
724 "the wrong reward model later.");
728 result.second =
true;
732 if (transformationSettings.isToNondeterministicModelSet()) {
733 result.first = storm::api::transformToNondeterministicModel<ValueType>(std::move(*result.first));
734 result.second =
true;
740template<
typename ValueType>
742 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
744 if (ioSettings.isExportBuildSet()) {
745 switch (ioSettings.getExportBuildFormat()) {
751 input.
model ? input.
model.get().getParameterNames() : std::vector<std::string>(),
752 !ioSettings.isExplicitExportPlaceholdersDisabled());
759 "Exporting sparse models in " <<
storm::io::toString(ioSettings.getExportBuildFormat()) <<
" format is not supported.");
765 if (ioSettings.isExportExplicitSet()) {
767 input.
model ? input.
model.get().getParameterNames() : std::vector<std::string>(),
768 !ioSettings.isExplicitExportPlaceholdersDisabled());
771 if (ioSettings.isExportDdSet()) {
772 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Exporting in drdd format is only supported for DDs.");
775 if (ioSettings.isExportDotSet()) {
780template<storm::dd::DdType DdType,
typename ValueType>
782 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
784 if (ioSettings.isExportBuildSet()) {
785 switch (ioSettings.getExportBuildFormat()) {
794 "Exporting symbolic models in " <<
storm::io::toString(ioSettings.getExportBuildFormat()) <<
" format is not supported.");
800 if (ioSettings.isExportExplicitSet()) {
801 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Exporting in drn format is only supported for sparse models.");
804 if (ioSettings.isExportDdSet()) {
808 if (ioSettings.isExportDotSet()) {
813template<storm::dd::DdType DdType,
typename ValueType>
814typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
819template<storm::dd::DdType DdType,
typename ValueType>
820typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type
822 auto ma = model->template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
823 if (!ma->isClosed()) {
824 return std::make_shared<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(ma->close());
830template<storm::dd::DdType DdType,
typename ValueType,
typename ExportValueType = ValueType>
835 "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
840 STORM_LOG_INFO(
"Setting bisimulation quotient format to 'sparse'.");
844 return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(
848template<
typename ExportValueType, storm::dd::DdType DdType,
typename ValueType>
851 auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
852 std::pair<std::shared_ptr<storm::models::Model<ValueType>>,
bool> intermediateResult = std::make_pair(model,
false);
856 intermediateResult.second =
true;
859 std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>,
bool>> result;
860 auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
862 std::shared_ptr<storm::models::Model<ExportValueType>> newModel =
863 preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings, mpi);
864 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>,
bool>>(newModel,
true);
866 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>,
bool>>(
867 symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
872 result->second =
true;
874 std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel =
875 result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
876 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
877 for (
auto const& property : input.
properties) {
878 formulas.emplace_back(property.getRawFormula());
881 STORM_LOG_THROW(result, storm::exceptions::NotSupportedException,
"The translation to a sparse model is not supported for the given model type.");
887template<storm::dd::DdType DdType,
typename ValueType>
892 if constexpr (std::is_same_v<ValueType, VT> ||
893 (DdType == storm::dd::DdType::Sylvan && std::is_same_v<ValueType, storm::RationalNumber> && std::is_same_v<VT, double>)) {
894 return preprocessDdModelImpl<VT>(model, input, mpi);
896 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
897 "Unexpected combination of DD library, build value type, and verification value type.");
907 if (counterexample) {
910 STORM_PRINT(
"Time for computation: " << *watch <<
".\n");
917template<
typename ModelType>
918 requires(!std::derived_from<ModelType, storm::models::sparse::Model<double>>)
920 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Counterexample generation is not supported for this data-type.");
923template<
typename ModelType>
924 requires(std::derived_from<ModelType, storm::models::sparse::Model<double>>)
926 using ValueType =
typename ModelType::ValueType;
928 for (
auto& rewModel : sparseModel->getRewardModels()) {
929 rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(),
true);
933 storm::exceptions::NotSupportedException,
"Counterexample is currently only supported for discrete-time models.");
935 auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
936 if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
937 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
938 for (
auto const& property : input.
properties) {
939 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
944 "Counterexample generation using MILP is currently only supported for MDPs.");
949 storm::exceptions::NotSupportedException,
950 "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
963 }
else if (counterexampleSettings.isShortestPathGenerationSet()) {
964 for (
auto const& property : input.
properties) {
965 std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
969 "Counterexample generation using shortest paths is currently only supported for DTMCs.");
971 property.getRawFormula(), counterexampleSettings.getShortestPathMaxK());
976 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The selected counterexample formalism is unsupported.");
980template<
typename ValueType>
981 requires(!storm::IsIntervalType<ValueType>)
983 if (result->isQuantitative()) {
987 ValueType resultValue;
990 resultValue = result->asQuantitativeCheckResult<ValueType>().sum();
993 resultValue = result->asQuantitativeCheckResult<ValueType>().average();
996 resultValue = result->asQuantitativeCheckResult<ValueType>().getMin();
999 resultValue = result->asQuantitativeCheckResult<ValueType>().getMax();
1003 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Outputting states is not supported.");
1007 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"Filter type only defined for qualitative results.");
1009 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"Unhandled filter type.");
1012 STORM_PRINT(resultValue <<
" (approx. " << storm::utility::convertNumber<double>(resultValue) <<
")");
1023 STORM_PRINT(result->asQualitativeCheckResult().existsTrue());
1026 STORM_PRINT(result->asQualitativeCheckResult().forallTrue());
1029 STORM_PRINT(result->asQualitativeCheckResult().count());
1033 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Outputting states is not supported.");
1038 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"Filter type only defined for quantitative results.");
1048template<
typename ValueType>
1049 requires(!storm::IsIntervalType<ValueType>)
1053 std::stringstream ss;
1054 ss <<
"'" << filterStatesFormula <<
"'";
1056 <<
" (for " << (filterStatesFormula.isInitialFormula() ?
"initial" : ss.str()) <<
" states): ");
1057 printFilteredResult<ValueType>(result, filterType);
1059 STORM_PRINT(
"Time for model checking: " << *watch <<
".\n");
1062 STORM_LOG_ERROR(
"Property is unsupported by selected engine/settings.\n");
1066template<
typename ValueType>
1072using VerificationCallbackType = std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const>
const& formula,
1073 std::shared_ptr<storm::logic::Formula const>
const& states)>;
1077 void operator()(std::unique_ptr<storm::modelchecker::CheckResult>
const&) {
1088template<
typename ValueType>
1089std::unique_ptr<storm::modelchecker::CheckResult>
verifyProperty(std::shared_ptr<storm::logic::Formula const>
const& formula,
1090 std::shared_ptr<storm::logic::Formula const>
const& statesFilter,
1092 auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
1095 if constexpr (storm::IsIntervalType<ValueType>) {
1096 STORM_LOG_ASSERT(!transformationSettings.isChainEliminationSet() && !transformationSettings.isToNondeterministicModelSet(),
1097 "Unsupported transformation has been invoked.");
1098 return verificationCallback(formula, statesFilter);
1101 STORM_LOG_WARN(
"Property is not preserved by elimination of non-markovian states.");
1102 }
else if (transformationSettings.isToDiscreteTimeModelSet()) {
1103 auto transformedFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*formula);
1104 auto transformedStatesFilter = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*statesFilter);
1105 if (transformedFormula && transformedStatesFilter) {
1107 return verificationCallback(transformedFormula, transformedStatesFilter);
1109 STORM_LOG_WARN(
"Property is not preserved by transformation to discrete time model.");
1113 return verificationCallback(formula, statesFilter);
1127template<
typename ValueType>
1131 for (
auto const& property : properties) {
1134 auto result = verifyProperty<ValueType>(property.getRawFormula(), property.getFilter().getStatesFormula(), verificationCallback);
1137 postprocessingCallback(result);
1139 printResult<storm::IntervalBaseType<ValueType>>(result, property, &watch);
1152template<
typename ValueType>
1153void computeStateValues(std::string
const& description, std::function<std::unique_ptr<storm::modelchecker::CheckResult>()>
const& computationCallback,
1158 STORM_PRINT(
"\nComputing " << description <<
" ...\n");
1159 std::unique_ptr<storm::modelchecker::CheckResult> result;
1161 result = computationCallback();
1172 postprocessingCallback(result);
1177 for (uint64_t propertyIndex = 0; propertyIndex < properties.size(); ++propertyIndex) {
1178 auto const&
property = properties[propertyIndex];
1180 if (!property.getRawFormula()->hasQualitativeResult()) {
1182 <<
"' can not be used for filtering states as it does not have a qualitative result.");
1189 if (propertyFilter) {
1191 std::unique_ptr<storm::modelchecker::CheckResult> filteredResult = result->clone();
1192 filteredResult->filter(propertyFilter->asQualitativeCheckResult());
1193 postprocessingCallback(filteredResult);
1194 printResult<ValueType>(filteredResult, *property.getRawFormula(), property.getFilter().getFilterType(),
1195 propertyIndex == properties.size() - 1 ? &watch :
nullptr);
1202 std::string
const& constraintsString) {
1203 std::vector<storm::expressions::Expression> constraints;
1205 std::vector<std::string> constraintsAsStrings;
1206 boost::split(constraintsAsStrings, constraintsString, boost::is_any_of(
","));
1209 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1210 for (
auto const& variableTypePair : expressionManager) {
1211 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1215 for (
auto const& constraintString : constraintsAsStrings) {
1216 if (constraintString.empty()) {
1221 STORM_LOG_TRACE(
"Adding special (user-provided) constraint " << constraint <<
".");
1222 constraints.emplace_back(constraint);
1230 std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
1233 std::unordered_map<std::string, storm::expressions::Expression> variableMapping;
1234 for (
auto const& variableTypePair : expressionManager) {
1235 variableMapping[variableTypePair.first.getName()] = variableTypePair.first;
1239 std::vector<std::string> predicateGroupsAsStrings;
1240 boost::split(predicateGroupsAsStrings, refinementPredicatesString, boost::is_any_of(
";"));
1242 if (!predicateGroupsAsStrings.empty()) {
1243 for (
auto const& predicateGroupString : predicateGroupsAsStrings) {
1244 if (predicateGroupString.empty()) {
1248 std::vector<std::string> predicatesAsStrings;
1249 boost::split(predicatesAsStrings, predicateGroupString, boost::is_any_of(
":"));
1251 if (!predicatesAsStrings.empty()) {
1252 injectedRefinementPredicates.emplace_back();
1253 for (
auto const& predicateString : predicatesAsStrings) {
1255 STORM_LOG_TRACE(
"Adding special (user-provided) refinement predicate " << predicateString <<
".");
1256 injectedRefinementPredicates.back().emplace_back(predicate);
1259 STORM_LOG_THROW(!injectedRefinementPredicates.back().empty(), storm::exceptions::InvalidArgumentException,
1260 "Expecting non-empty list of predicates to inject for each (mentioned) refinement step.");
1263 std::reverse(injectedRefinementPredicates.back().begin(), injectedRefinementPredicates.back().end());
1268 std::reverse(injectedRefinementPredicates.begin(), injectedRefinementPredicates.end());
1271 return injectedRefinementPredicates;
1274template<storm::dd::DdType DdType,
typename ValueType>
1282 verifyProperties<ValueType>(input, [&input, &options, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula,
1283 std::shared_ptr<storm::logic::Formula const>
const& states) {
1284 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException,
"Abstraction-refinement can only filter initial states.");
1285 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.
env, input.
model.get(),
1286 storm::api::createTask<ValueType>(formula,
true), options);
1290template<
typename ValueType>
1293 STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException,
1294 "Exploration does not support other data-types than floating points.");
1295 verifyProperties<ValueType>(
1296 input, [&input, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula, std::shared_ptr<storm::logic::Formula const>
const& states) {
1297 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException,
"Exploration can only filter initial states.");
1298 return storm::api::verifyWithExplorationEngine<ValueType>(mpi.
env, input.
model.get(), storm::api::createTask<ValueType>(formula,
true));
1302template<
typename ValueType>
1305 auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
1306 auto verificationCallback = [&sparseModel, &ioSettings, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula,
1307 std::shared_ptr<storm::logic::Formula const>
const& states) {
1308 bool filterForInitialStates = states->isInitialFormula();
1309 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1310 if (ioSettings.isExportSchedulerSet()) {
1311 task.setProduceSchedulers(
true);
1313 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(mpi.
env, sparseModel, task);
1315 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1316 if (filterForInitialStates) {
1317 filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
1318 }
else if (!states->isTrueFormula()) {
1319 filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.
env, sparseModel, storm::api::createTask<ValueType>(states,
false));
1321 if (result && filter) {
1322 result->filter(filter->asQualitativeCheckResult());
1326 uint64_t exportCount = 0;
1327 auto postprocessingCallback = [&sparseModel, &ioSettings, &input, &exportCount](std::unique_ptr<storm::modelchecker::CheckResult>
const& result) {
1329 STORM_LOG_WARN_COND(!ioSettings.isExportSchedulerSet() || result->hasScheduler(),
"Scheduler requested but could not be generated.");
1330 if (ioSettings.isExportSchedulerSet() && result->hasScheduler()) {
1331 std::filesystem::path schedulerExportPath = ioSettings.getExportSchedulerFilename();
1332 if (exportCount > 0) {
1333 STORM_LOG_WARN(
"Prepending " << exportCount <<
" to scheduler file name for this property because there are multiple properties.");
1334 schedulerExportPath.replace_filename(std::to_string(exportCount) + schedulerExportPath.filename().string());
1339 "No information of state valuations available. The scheduler output will use internal state ids. You might be "
1340 "interested in building the model with state valuations using --buildstateval.");
1342 sparseModel->hasChoiceLabeling() || sparseModel->hasChoiceOrigins(),
1343 "No symbolic choice information is available. The scheduler output will use internal choice ids. You might be interested in "
1344 "building the model with choice labels or choice origins using --buildchoicelab or --buildchoiceorig.");
1346 "Only partial choice information is available. You might want to build the model with choice origins using "
1347 "--buildchoicelab or --buildchoiceorig.");
1349 if (result->isExplicitQuantitativeCheckResult()) {
1350 if constexpr (storm::IsIntervalType<ValueType>) {
1351 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Scheduler export for interval models is not supported.");
1354 schedulerExportPath.string());
1356 }
else if (result->isExplicitParetoCurveCheckResult()) {
1357 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
1358 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Scheduler export for models of this value type is not supported.");
1360 auto const& paretoRes = result->template asExplicitParetoCurveCheckResult<ValueType>();
1364 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Scheduler export not supported for this value type.");
1369 if (ioSettings.isExportCheckResultSet()) {
1370 if constexpr (storm::IsIntervalType<ValueType>) {
1371 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Result export for interval models is not supported.");
1373 std::filesystem::path resultExportPath = ioSettings.getExportCheckResultFilename();
1374 if (exportCount > 0) {
1375 STORM_LOG_WARN(
"Prepending " << exportCount <<
" to result file name for this property because there are multiple properties.");
1376 resultExportPath.replace_filename(std::to_string(exportCount) + resultExportPath.filename().string());
1379 "No information of state valuations available. The result output will use internal state ids. You might be interested in "
1380 "building the model with state valuations using --buildstateval.");
1386 if (!(ioSettings.isComputeSteadyStateDistributionSet() || ioSettings.isComputeExpectedVisitingTimesSet())) {
1387 verifyProperties<ValueType>(input, verificationCallback, postprocessingCallback);
1389 if (ioSettings.isComputeSteadyStateDistributionSet()) {
1390 if constexpr (storm::IsIntervalType<ValueType>) {
1391 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Computing steady state distribution is not supported for interval models.");
1393 computeStateValues<ValueType>(
1394 "steady-state probabilities",
1395 [&mpi, &sparseModel]() {
return storm::api::computeSteadyStateDistributionWithSparseEngine<ValueType>(mpi.
env, sparseModel); }, input,
1396 verificationCallback, postprocessingCallback);
1399 if (ioSettings.isComputeExpectedVisitingTimesSet()) {
1400 if constexpr (storm::IsIntervalType<ValueType>) {
1401 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Computing expected visiting times is not supported for interval models.");
1403 computeStateValues<ValueType>(
1404 "expected visiting times",
1405 [&mpi, &sparseModel]() {
return storm::api::computeExpectedVisitingTimesWithSparseEngine<ValueType>(mpi.
env, sparseModel); }, input,
1406 verificationCallback, postprocessingCallback);
1411template<storm::dd::DdType DdType,
typename ValueType>
1414 verifyProperties<ValueType>(
1415 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula, std::shared_ptr<storm::logic::Formula const>
const& states) {
1416 bool filterForInitialStates = states->isInitialFormula();
1417 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1419 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.
env, symbolicModel, task);
1421 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1422 if (filterForInitialStates) {
1423 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1424 symbolicModel->getInitialStates());
1425 }
else if (!states->isTrueFormula()) {
1426 filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(states,
false));
1428 if (result && filter) {
1429 result->filter(filter->asQualitativeCheckResult());
1435template<storm::dd::DdType DdType,
typename ValueType>
1438 verifyProperties<ValueType>(
1439 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula, std::shared_ptr<storm::logic::Formula const>
const& states) {
1440 bool filterForInitialStates = states->isInitialFormula();
1441 auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
1443 std::unique_ptr<storm::modelchecker::CheckResult> result =
1444 storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(formula,
true));
1446 std::unique_ptr<storm::modelchecker::CheckResult> filter;
1447 if (filterForInitialStates) {
1448 filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(),
1449 symbolicModel->getInitialStates());
1450 }
else if (!states->isTrueFormula()) {
1451 filter = storm::api::verifyWithDdEngine<DdType, ValueType>(mpi.
env, symbolicModel, storm::api::createTask<ValueType>(states,
false));
1453 if (result && filter) {
1454 result->filter(filter->asQualitativeCheckResult());
1460template<storm::dd::DdType DdType,
typename ValueType>
1463 verifyProperties<ValueType>(
1464 input, [&symbolicModel, &mpi](std::shared_ptr<storm::logic::Formula const>
const& formula, std::shared_ptr<storm::logic::Formula const>
const& states) {
1465 STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException,
"Abstraction-refinement can only filter initial states.");
1466 return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.
env, symbolicModel,
1467 storm::api::createTask<ValueType>(formula,
true));
1471template<storm::dd::DdType DdType,
typename ValueType>
1472typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value,
void>::type
verifyModel(
1476 verifyWithHybridEngine<DdType, ValueType>(symbolicModel, input, mpi);
1478 verifyWithDdEngine<DdType, ValueType>(symbolicModel, input, mpi);
1480 verifyWithAbstractionRefinementEngine<DdType, ValueType>(symbolicModel, input, mpi);
1484template<storm::dd::DdType DdType,
typename ValueType>
1485typename std::enable_if<DdType == storm::dd::DdType::CUDD && !std::is_same<ValueType, double>::value,
void>::type
verifySymbolicModel(
1487 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"CUDD does not support the selected data-type.");
1491 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
1492 auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
1494 std::shared_ptr<storm::models::ModelBase> model;
1495 if (!buildSettings.isNoBuildModelSet()) {
1502 model->printModelInformationToStream(std::cout);
1506 preprocessingWatch.
stop();
1507 if (preprocessingResult.second) {
1508 STORM_PRINT(
"\nTime for model preprocessing: " << preprocessingWatch <<
".\n\n");
1509 model = preprocessingResult.first;
1510 model->printModelInformationToStream(std::cout);
1525 auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
1526 auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
1532 [&input, &mpi]<
storm::dd::DdType DD,
typename VT>() { verifyWithAbstractionRefinementEngine<DD, VT>(input, mpi); });
1538 if (counterexampleSettings.isCounterexampleSet()) {
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 std::optional< storm::dd::DdType > getDdType() const
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)
void exportParetoScheduler(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< PointType > const &points, std::vector< storm::storage::Scheduler< ValueType > > const &schedulers, std::string const &baseFilenameStr)
std::vector< storm::jani::Property > substituteConstantsInProperties(std::vector< storm::jani::Property > const &properties, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)
void exportModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
void exportSymbolicInput(SymbolicInput const &input)
void parseSymbolicModelDescription(storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input)
void verifyWithAbstractionRefinementEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > buildModelExplicit(storm::settings::modules::IOSettings const &ioSettings, storm::settings::modules::BuildSettings const &buildSettings)
std::enable_if< DdType==storm::dd::DdType::CUDD &&!std::is_same< ValueType, double >::value, void >::type verifySymbolicModel(std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &, ModelProcessingInformation const &)
void verifyModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &sparseModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
auto castAndApply(std::shared_ptr< storm::models::ModelBase > const &model, auto const &callback)
SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const &ioSettings)
void getModelProcessingInformationAutomatic(SymbolicInput const &input, ModelProcessingInformation &mpi)
void verifyWithExplorationEngine(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void printResult(std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::logic::Formula const &filterStatesFormula, storm::modelchecker::FilterType const &filterType, storm::utility::Stopwatch *watch=nullptr)
auto applyValueType(ModelProcessingInformation::ValueType vt, auto const &callback)
std::shared_ptr< storm::models::ModelBase > buildPreprocessExportModel(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void verifyProperties(SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
Verifies all (potentially preprocessed) properties given in input.
std::vector< storm::expressions::Expression > parseConstraints(storm::expressions::ExpressionManager const &expressionManager, std::string const &constraintsString)
std::vector< std::vector< storm::expressions::Expression > > parseInjectedRefinementPredicates(storm::expressions::ExpressionManager const &expressionManager, std::string const &refinementPredicatesString)
SymbolicInput parseSymbolicInput()
void verifyWithDdEngine(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &states)> VerificationCallbackType
std::shared_ptr< storm::models::ModelBase > buildModelSparse(SymbolicInput const &input, storm::builder::BuilderOptions const &options)
std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type preprocessDdMarkovAutomaton(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseMarkovAutomaton(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &model)
void printFilteredResult(std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::modelchecker::FilterType ft)
void computeStateValues(std::string const &description, std::function< std::unique_ptr< storm::modelchecker::CheckResult >()> const &computationCallback, SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
Computes values for each state (such as the steady-state probability distribution).
void printCounterexample(std::shared_ptr< storm::counterexamples::Counterexample > const &counterexample, storm::utility::Stopwatch *watch=nullptr)
std::pair< SymbolicInput, ModelProcessingInformation > preprocessSymbolicInput(SymbolicInput const &input)
std::shared_ptr< storm::models::ModelBase > buildModel(SymbolicInput const &input, storm::settings::modules::IOSettings const &ioSettings, ModelProcessingInformation const &mpi)
void printModelCheckingProperty(storm::jani::Property const &property)
void parseProperties(storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input, boost::optional< std::set< std::string > > const &propertyFilter)
void verifyWithHybridEngine(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
ModelProcessingInformation getModelProcessingInformation(SymbolicInput const &input, std::shared_ptr< SymbolicInput > const &transformedJaniInput=nullptr)
Sets the model processing information based on the given input.
void printComputingCounterexample(storm::jani::Property const &property)
std::shared_ptr< storm::models::Model< ExportValueType > > preprocessDdModelBisimulation(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings, ModelProcessingInformation const &mpi)
auto applyDdLibValueType(storm::dd::DdType dd, ModelProcessingInformation::ValueType vt, auto const &callback)
std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> PostprocessingCallbackType
std::shared_ptr< storm::models::ModelBase > buildPreprocessModel(SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::sparse::Model< ValueType > > preprocessSparseModelBisimulation(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings)
storm::builder::BuilderOptions createBuildOptionsSparseFromSettings(SymbolicInput const &input)
void processInput(SymbolicInput const &input, ModelProcessingInformation const &mpi)
void ensureNoUndefinedPropertyConstants(std::vector< storm::jani::Property > const &properties)
void generateCounterexamples(std::shared_ptr< ModelType > const &, SymbolicInput const &)
std::vector< std::shared_ptr< storm::logic::Formula const > > createFormulasToRespect(std::vector< storm::jani::Property > const &properties)
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessModel(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase > buildModelDd(SymbolicInput const &input)
std::pair< std::shared_ptr< storm::models::ModelBase >, bool > preprocessDdModelImpl(std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::unique_ptr< storm::modelchecker::CheckResult > verifyProperty(std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &statesFilter, VerificationCallbackType const &verificationCallback)
Verifies the given formula plus a filter formula to identify relevant states and warns the user in ca...
std::string toString(ModelExportFormat const &input)
SettingsManager const & manager()
Retrieves the settings manager.
std::string orderKindtoString(OrderKind order)
Converts the given order to a string.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
bool isConstant(ValueType const &)
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.
typename detail::IntervalMetaProgrammingHelper< ValueType >::BaseType IntervalBaseType
Helper to access the type in which interval boundaries are stored.
void operator()(std::unique_ptr< storm::modelchecker::CheckResult > const &)