From 17325419fbb02c4fe381b7b4a4ed4a69e93fa246 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 17 Feb 2020 10:49:45 +0100 Subject: [PATCH] Introduced JIT as a separate engine. --- src/storm-cli-utilities/cli.cpp | 9 +++---- src/storm-cli-utilities/model-handling.h | 25 ++++------------- src/storm/settings/modules/BuildSettings.cpp | 6 ----- src/storm/settings/modules/BuildSettings.h | 6 ----- src/storm/utility/Engine.cpp | 28 ++++++++++++++++++++ src/storm/utility/Engine.h | 9 +++++-- 6 files changed, 44 insertions(+), 39 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 3d7096d1c..ccacbc749 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -250,28 +250,27 @@ namespace storm { auto coreSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); auto buildSettings = storm::settings::getModule(); - auto builderType = getBuilderType(engine, buildSettings.isJitSet()); // TODO: (end of method) - symbolicInput = preprocessSymbolicInput(symbolicInput, builderType); + symbolicInput = preprocessSymbolicInput(symbolicInput, storm::utility::getBuilderType(engine)); exportSymbolicInput(symbolicInput); auto generalSettings = storm::settings::getModule(); if (generalSettings.isParametricSet()) { #ifdef STORM_HAVE_CARL - processInputWithValueType(symbolicInput); + 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); + processInputWithValueType(symbolicInput, engine); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { - processInputWithValueType(symbolicInput); + processInputWithValueType(symbolicInput, engine); } } diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 7154e7399..11fa5e8ac 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -218,25 +218,10 @@ namespace storm { } } - storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine, bool useJit) { - if (engine == storm::utility::Engine::Dd || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::DdSparse || engine == storm::utility::Engine::AbstractionRefinement) { - return storm::builder::BuilderType::Dd; - } else if (engine == storm::utility::Engine::Sparse) { - if (useJit) { - return storm::builder::BuilderType::Jit; - } else { - return storm::builder::BuilderType::Explicit; - } - } else if (engine == storm::utility::Engine::Exploration) { - return storm::builder::BuilderType::Explicit; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type."); - } - 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 = getBuilderType(engine, buildSettings.isJitSet()); + auto builderType = storm::utility::getBuilderType(engine); SymbolicInput input = parseSymbolicInput(); input = preprocessSymbolicInput(input, builderType); @@ -262,7 +247,7 @@ namespace storm { } template - std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) { + std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings, bool useJit) { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); @@ -286,7 +271,7 @@ namespace storm { options.setBuildAllLabels(true); options.setBuildAllRewardModels(true); } - return storm::api::buildSparseModel(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); + return storm::api::buildSparseModel(input.model.get(), options, useJit, storm::settings::getModule().isDoctorSet()); } template @@ -312,11 +297,11 @@ namespace storm { auto buildSettings = storm::settings::getModule(); std::shared_ptr result; if (input.model) { - auto builderType = getBuilderType(engine, buildSettings.isJitSet()); + auto builderType = storm::utility::getBuilderType(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); + 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."); diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3ebc6d109..cdf4239c1 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -18,7 +18,6 @@ namespace storm { const std::string BuildSettings::moduleName = "build"; - const std::string jitOptionName = "jit"; const std::string explorationOrderOptionName = "explorder"; const std::string explorationOrderOptionShortName = "eo"; const std::string explorationChecksOptionName = "explchecks"; @@ -38,7 +37,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build()); @@ -53,10 +51,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build()); } - bool BuildSettings::isJitSet() const { - return this->getOption(jitOptionName).getHasOptionBeenSet(); - } - bool BuildSettings::isExplorationOrderSet() const { return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index b80424c7f..70d0777c6 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -16,12 +16,6 @@ namespace storm { * Creates a new set of core settings. */ BuildSettings(); - /*! - * Retrieves whether the option to use the JIT builder is set. - * - * @return True iff the JIT builder is to be used. - */ - bool isJitSet() const; /*! * Retrieves whether the model exploration order was set. diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 19a719100..52b59f610 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -19,6 +19,10 @@ #include "storm/storage/SymbolicModelDescription.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidArgumentException.h" + namespace storm { namespace utility { @@ -41,6 +45,8 @@ namespace storm { return "dd"; case Engine::DdSparse: return "dd-to-sparse"; + case Engine::Jit: + return "jit"; case Engine::Exploration: return "expl"; case Engine::AbstractionRefinement: @@ -67,6 +73,28 @@ namespace storm { STORM_LOG_ERROR("The engine '" << engineStr << "' was not found."); return Engine::Unknown; } + + storm::builder::BuilderType getBuilderType(Engine const& engine) { + switch (engine) { + case Engine::Sparse: + return storm::builder::BuilderType::Explicit; + case Engine::Hybrid: + return storm::builder::BuilderType::Dd; + case Engine::Dd: + return storm::builder::BuilderType::Dd; + case Engine::DdSparse: + return storm::builder::BuilderType::Dd; + case Engine::Jit: + return storm::builder::BuilderType::Jit; + case Engine::Exploration: + return storm::builder::BuilderType::Explicit; + case Engine::AbstractionRefinement: + return storm::builder::BuilderType::Dd; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given engine has no builder type to it."); + return storm::builder::BuilderType::Explicit; + } + } template bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask) { diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index be14f1971..2c43047e5 100644 --- a/src/storm/utility/Engine.h +++ b/src/storm/utility/Engine.h @@ -5,6 +5,7 @@ #include "storm/models/ModelType.h" #include "storm/storage/dd/DdType.h" +#include "storm/builder/BuilderType.h" namespace storm { @@ -25,7 +26,7 @@ namespace storm { /// An enumeration of all engines. enum class Engine { // The last one should always be 'Unknown' to make sure that the getEngines() method below works. - Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement, Unknown + Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Unknown }; /*! @@ -49,6 +50,11 @@ namespace storm { */ Engine engineFromString(std::string const& engineStr); + /*! + * Returns the builder type used for the given engine. + */ + storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine); + /*! * Returns false if the given model type and checkTask can certainly not be handled by the given engine. * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true, @@ -66,6 +72,5 @@ namespace storm { */ template bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription); - } } \ No newline at end of file