From 1574f4444a0cf2138336f1aa5f7d92b2187ab112 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 18 Feb 2020 09:05:14 +0100 Subject: [PATCH] CLI: Introduced ModelProcessingInformation which allows to set certain settings (regardinge model building and model verification) in an on-the-fly manner. --- src/storm-cli-utilities/cli.cpp | 40 ++-- src/storm-cli-utilities/model-handling.h | 224 +++++++++++++++-------- 2 files changed, 168 insertions(+), 96 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index ccacbc749..df10dcbf1 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -245,33 +245,31 @@ namespace storm { // Parse symbolic input (PRISM, JANI, properties, etc.) SymbolicInput symbolicInput = parseSymbolicInput(); - // Get the engine to use - // TODO: Create a new method that gets the used engine and the used environment (using portfolio engine) - auto coreSettings = storm::settings::getModule(); - auto engine = coreSettings.getEngine(); - auto buildSettings = storm::settings::getModule(); - // TODO: (end of method) + // Obtain settings for model processing + ModelProcessingInformation mpi = getModelProcessingInformation(symbolicInput); - symbolicInput = preprocessSymbolicInput(symbolicInput, storm::utility::getBuilderType(engine)); + // Preprocess the symbolic input + symbolicInput = preprocessSymbolicInput(symbolicInput, mpi.engine); + + // Export symbolic input (if requested) exportSymbolicInput(symbolicInput); - - auto generalSettings = storm::settings::getModule(); - if (generalSettings.isParametricSet()) { #ifdef STORM_HAVE_CARL - processInputWithValueType(symbolicInput, engine); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); -#endif - } else if (generalSettings.isExactSet()) { -#ifdef STORM_HAVE_CARL - processInputWithValueType(symbolicInput, engine); + switch (mpi.verificationValueType) { + case ModelProcessingInformation::ValueType::Parametric: + processInputWithValueType(symbolicInput, mpi); + break; + case ModelProcessingInformation::ValueType::Exact: + processInputWithValueType(symbolicInput, mpi); + break; + case ModelProcessingInformation::ValueType::FinitePrecision: + processInputWithValueType(symbolicInput, mpi); + break; + } #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); + STORM_LOG_THROW(mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision, storm::exceptions::NotSupportedException, "No exact numbers or parameters are supported in this build."); + processInputWithValueType(symbolicInput, mpi); #endif - } else { - processInputWithValueType(symbolicInput, engine); - } } void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index c1bb6c8a0..c83c39e93 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -25,6 +25,8 @@ #include "storm/models/ModelBase.h" +#include "storm/environment/Environment.h" + #include "storm/exceptions/OptionParserException.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -144,6 +146,76 @@ namespace storm { } } + struct ModelProcessingInformation { + // The engine to use + storm::utility::Engine engine; + + // If set, bisimulation will be applied. + bool applyBisimulation; + + // Which data type is to be used for numbers ... + enum class ValueType { + FinitePrecision, + Exact, + Parametric + }; + ValueType buildValueType; // ... during model building + ValueType verificationValueType; // ... during model verification + + // The Dd library to be used + storm::dd::DdType ddType; + + // The environment used during model checking + storm::Environment env; + }; + + ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input) { + ModelProcessingInformation mpi; + auto coreSettings = storm::settings::getModule(); + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + + // Set the engine. + mpi.engine = coreSettings.getEngine(); + + // Set whether bisimulation is to be used. + mpi.applyBisimulation = generalSettings.isBisimulationSet(); + + // Set the value type used for numeric values + if (generalSettings.isParametricSet()) { + mpi.verificationValueType = ModelProcessingInformation::ValueType::Parametric; + } else if (generalSettings.isExactSet()) { + mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact; + } else { + mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecision; + } + + // Since the remaining settings could depend on the ones above, we need to invoke the portfolio decision tree now. + // TODO: portfolio treatment here + + // Set the Valuetype used during model building + mpi.buildValueType = mpi.verificationValueType; + if (bisimulationSettings.useExactArithmeticInDdBisimulation()) { + if (storm::utility::getBuilderType(mpi.engine) == storm::builder::BuilderType::Dd && mpi.applyBisimulation) { + if (mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision) { + mpi.buildValueType = ModelProcessingInformation::ValueType::Exact; + } + } else { + STORM_LOG_WARN("Requested using exact arithmetic in Dd bisimulation but no dd bisimulation is applied."); + } + } + + // Set the Dd library + mpi.ddType = coreSettings.getDdLibraryType(); + if (mpi.ddType == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue()) { + if (!(mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision)) { + STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic."); + mpi.ddType = storm::dd::DdType::Sylvan; + } + } + return mpi; + } + void ensureNoUndefinedPropertyConstants(std::vector const& properties) { // Make sure there are no undefined constants remaining in any property. for (auto const& property : properties) { @@ -158,8 +230,9 @@ namespace storm { } } - SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::builder::BuilderType const& builderType) { + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::utility::Engine const& engine) { auto ioSettings = storm::settings::getModule(); + auto builderType = storm::utility::getBuilderType(engine); SymbolicInput output = input; @@ -221,10 +294,9 @@ namespace storm { SymbolicInput parseAndPreprocessSymbolicInput(storm::utility::Engine const& engine) { // Get the used builder type to handle cases where preprocessing depends on it auto buildSettings = storm::settings::getModule(); - auto builderType = storm::utility::getBuilderType(engine); SymbolicInput input = parseSymbolicInput(); - input = preprocessSymbolicInput(input, builderType); + input = preprocessSymbolicInput(input, engine); exportSymbolicInput(input); return input; } @@ -291,20 +363,20 @@ namespace storm { } template - std::shared_ptr buildModel(storm::utility::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr buildModel(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings, ModelProcessingInformation const& mpi) { storm::utility::Stopwatch modelBuildingWatch(true); auto buildSettings = storm::settings::getModule(); std::shared_ptr result; if (input.model) { - auto builderType = storm::utility::getBuilderType(engine); + auto builderType = storm::utility::getBuilderType(mpi.engine); if (builderType == storm::builder::BuilderType::Dd) { result = buildModelDd(input); } else if (builderType == storm::builder::BuilderType::Explicit || builderType == storm::builder::BuilderType::Jit) { result = buildModelSparse(input, buildSettings, builderType == storm::builder::BuilderType::Jit); } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { - STORM_LOG_THROW(engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); + STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = buildModelExplicit(ioSettings, buildSettings); } @@ -349,8 +421,7 @@ namespace storm { } template - std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto generalSettings = storm::settings::getModule(); + std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto bisimulationSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); auto transformationSettings = storm::settings::getModule(); @@ -362,7 +433,7 @@ namespace storm { result.second = true; } - if (generalSettings.isBisimulationSet()) { + if (mpi.applyBisimulation) { result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); result.second = true; } @@ -435,17 +506,18 @@ namespace storm { } template - std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { + std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings, ModelProcessingInformation const& mpi) { STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation."); + auto quotientFormat = bisimulationSettings.getQuotientFormat(); + STORM_LOG_INFO("Performing bisimulation minimization..."); - return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode()); + return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode(), quotientFormat); } template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto bisimulationSettings = storm::settings::getModule(); - auto generalSettings = storm::settings::getModule(); std::pair>, bool> intermediateResult = std::make_pair(model, false); if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { @@ -455,14 +527,14 @@ namespace storm { std::unique_ptr>, bool>> result; auto symbolicModel = intermediateResult.first->template as>(); - if (generalSettings.isBisimulationSet()) { - std::shared_ptr> newModel = preprocessDdModelBisimulation(symbolicModel, input, bisimulationSettings); + if (mpi.applyBisimulation) { + std::shared_ptr> newModel = preprocessDdModelBisimulation(symbolicModel, input, bisimulationSettings, mpi); result = std::make_unique>, bool>>(newModel, true); } else { result = std::make_unique>, bool>>(symbolicModel->template toValueType(), !std::is_same::value); } - if (result && result->first->isSymbolicModel() && engine == storm::utility::Engine::DdSparse) { + if (result && result->first->isSymbolicModel() && mpi.engine == storm::utility::Engine::DdSparse) { // Mark as changed. result->second = true; @@ -479,15 +551,15 @@ namespace storm { } template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { storm::utility::Stopwatch preprocessingWatch(true); std::pair, bool> result = std::make_pair(model, false); if (model->isSparseModel()) { - result = preprocessSparseModel(result.first->as>(), input); + result = preprocessSparseModel(result.first->as>(), input, mpi); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = preprocessDdModel(result.first->as>(), input, engine); + result = preprocessDdModel(result.first->as>(), input, mpi); } preprocessingWatch.stop(); @@ -769,45 +841,45 @@ namespace storm { } template - void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { + void verifyWithAbstractionRefinementEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule(); storm::api::AbstractionRefinementOptions options(parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()), parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates())); - verifyProperties(input, [&input,&options] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input,&options,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); - return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true), options); + return storm::api::verifyWithAbstractionRefinementEngine(mpi.env, input.model.get(), storm::api::createTask(formula, true), options); }); } template - void verifyWithExplorationEngine(SymbolicInput const& input) { + void verifyWithExplorationEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) { STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + verifyProperties(input, [&input,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); - return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); + return storm::api::verifyWithExplorationEngine(mpi.env, input.model.get(), storm::api::createTask(formula, true)); }); } template - void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { + void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto sparseModel = model->as>(); auto const& ioSettings = storm::settings::getModule(); verifyProperties(input, - [&sparseModel,&ioSettings] (std::shared_ptr const& formula, std::shared_ptr const& states) { + [&sparseModel,&ioSettings,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); if (ioSettings.isExportSchedulerSet()) { task.setProduceSchedulers(true); } - std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); + std::unique_ptr result = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, task); std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique(sparseModel->getInitialStates()); } else { - filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); + filter = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, storm::api::createTask(states, false)); } if (result && filter) { result->filter(filter->asQualitativeCheckResult()); @@ -832,19 +904,19 @@ namespace storm { } template - void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); + std::unique_ptr result = storm::api::verifyWithHybridEngine(mpi.env, symbolicModel, task); std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); } else { - filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); + filter = storm::api::verifyWithHybridEngine(mpi.env, symbolicModel, storm::api::createTask(states, false)); } if (result && filter) { result->filter(filter->asQualitativeCheckResult()); @@ -854,19 +926,19 @@ namespace storm { } template - void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { bool filterForInitialStates = states->isInitialFormula(); auto task = storm::api::createTask(formula, filterForInitialStates); auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(formula, true)); + std::unique_ptr result = storm::api::verifyWithDdEngine(mpi.env, symbolicModel, storm::api::createTask(formula, true)); std::unique_ptr filter; if (filterForInitialStates) { filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); } else { - filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); + filter = storm::api::verifyWithDdEngine(mpi.env, symbolicModel, storm::api::createTask(states, false)); } if (result && filter) { result->filter(filter->asQualitativeCheckResult()); @@ -876,47 +948,47 @@ namespace storm { } template - void verifyWithAbstractionRefinementEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + void verifyWithAbstractionRefinementEngine(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { + verifyProperties(input, [&model,&mpi] (std::shared_ptr const& formula, std::shared_ptr const& states) { STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); auto symbolicModel = model->as>(); - return storm::api::verifyWithAbstractionRefinementEngine(symbolicModel, storm::api::createTask(formula, true)); + return storm::api::verifyWithAbstractionRefinementEngine(mpi.env, symbolicModel, storm::api::createTask(formula, true)); }); } template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { - if (engine == storm::utility::Engine::Hybrid) { - verifyWithHybridEngine(model, input); - } else if (engine == storm::utility::Engine::Dd) { - verifyWithDdEngine(model, input); + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { + if (mpi.engine == storm::utility::Engine::Hybrid) { + verifyWithHybridEngine(model, input, mpi); + } else if (mpi.engine == storm::utility::Engine::Dd) { + verifyWithDdEngine(model, input, mpi); } else { - verifyWithAbstractionRefinementEngine(model, input); + verifyWithAbstractionRefinementEngine(model, input, mpi); } } template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const&, SymbolicInput const& , storm::utility::Engine const&) { + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const&, SymbolicInput const&, ModelProcessingInformation const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type."); } template - void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { + void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, ModelProcessingInformation const& mpi) { if (model->isSparseModel()) { - verifyWithSparseEngine(model, input); + verifyWithSparseEngine(model, input, mpi); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - verifySymbolicModel(model, input, engine); + verifySymbolicModel(model, input, mpi); } } template - std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine engine) { + std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto ioSettings = storm::settings::getModule(); auto buildSettings = storm::settings::getModule(); std::shared_ptr model; if (!buildSettings.isNoBuildModelSet()) { - model = buildModel(engine, input, ioSettings); + model = buildModel(input, ioSettings, mpi); } if (model) { @@ -926,7 +998,7 @@ namespace storm { STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); if (model) { - auto preprocessingResult = preprocessModel(model, input, engine); + auto preprocessingResult = preprocessModel(model, input, mpi); if (preprocessingResult.second) { model = preprocessingResult.first; model->printModelInformationToStream(std::cout); @@ -937,46 +1009,48 @@ namespace storm { } template - void processInputWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine const& engine) { + void processInputWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) { auto abstractionSettings = storm::settings::getModule(); auto counterexampleSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. - if (engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { - verifyWithAbstractionRefinementEngine(input); - } else if (engine == storm::utility::Engine::Exploration) { - verifyWithExplorationEngine(input); + if (mpi.engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { + verifyWithAbstractionRefinementEngine(input, mpi); + } else if (mpi.engine == storm::utility::Engine::Exploration) { + verifyWithExplorationEngine(input, mpi); } else { - std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); + std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, mpi); if (model) { if (counterexampleSettings.isCounterexampleSet()) { generateCounterexamples(model, input); } else { - verifyModel(model, input, engine); + verifyModel(model, input, mpi); } } } } template - void processInputWithValueType(SymbolicInput const& input, storm::utility::Engine const& engine) { - auto coreSettings = storm::settings::getModule(); - auto generalSettings = storm::settings::getModule(); - auto bisimulationSettings = storm::settings::getModule(); + void processInputWithValueType(SymbolicInput const& input, ModelProcessingInformation const& mpi) { - if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) { - STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic."); - processInputWithValueTypeAndDdlib(input, engine); - } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && std::is_same::value && generalSettings.isBisimulationSet() && bisimulationSettings.useExactArithmeticInDdBisimulation()) { - STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic."); - processInputWithValueTypeAndDdlib(input, engine); - } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { - processInputWithValueTypeAndDdlib(input, engine); + if (mpi.ddType == storm::dd::DdType::CUDD) { + STORM_LOG_ASSERT(mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision && mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && (std::is_same::value), "Unexpected value type for Dd library cudd."); + processInputWithValueTypeAndDdlib(input, mpi); } else { - STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library."); - processInputWithValueTypeAndDdlib(input, engine); + STORM_LOG_ASSERT(mpi.ddType == storm::dd::DdType::Sylvan, "Unknown DD library."); + if (mpi.buildValueType == mpi.verificationValueType) { + processInputWithValueTypeAndDdlib(input, mpi); + } else { + // Right now, we only require (buildType == Exact and verificationType == FinitePrecision). + // We exclude all other combinations to safe a few template instantiations. + STORM_LOG_THROW((std::is_same::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact, storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType"); +#ifdef STORM_HAVE_CARL + processInputWithValueTypeAndDdlib(input, mpi); +#else + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unexpected buildValueType."); +#endif + } } } - } }