From d36cd93ae8f95a3635a51a06058db15dcac5ade8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 14 Feb 2020 12:30:12 +0100 Subject: [PATCH] CLI: Split parsing and preprocessing of symbolic input into two steps. Moved engine related methods and declaration to a separate file. --- src/storm-cli-utilities/cli.cpp | 16 +- src/storm-cli-utilities/model-handling.h | 124 ++++++++------- src/storm-pars-cli/storm-pars.cpp | 17 ++- src/storm-parsers/api/model_descriptions.cpp | 16 +- src/storm-parsers/api/model_descriptions.h | 3 + src/storm-pomdp-cli/storm-pomdp.cpp | 4 +- src/storm/settings/modules/CoreSettings.cpp | 28 ++-- src/storm/settings/modules/CoreSettings.h | 11 +- .../settings/modules/ExplorationSettings.cpp | 3 +- src/storm/utility/Engine.cpp | 141 ++++++++++++++++++ src/storm/utility/Engine.h | 71 +++++++++ 11 files changed, 327 insertions(+), 107 deletions(-) create mode 100644 src/storm/utility/Engine.cpp create mode 100644 src/storm/utility/Engine.h diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index c7b18fb7a..3d7096d1c 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -242,8 +242,20 @@ namespace storm { // Start by setting some urgent options (log levels, resources, etc.) setUrgentOptions(); - // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) - SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput(); + // 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(); + auto builderType = getBuilderType(engine, buildSettings.isJitSet()); + // TODO: (end of method) + + symbolicInput = preprocessSymbolicInput(symbolicInput, builderType); + exportSymbolicInput(symbolicInput); + auto generalSettings = storm::settings::getModule(); if (generalSettings.isParametricSet()) { diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index a49d244e5..7154e7399 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -10,6 +10,7 @@ #include "storm/utility/storm-version.h" #include "storm/utility/macros.h" #include "storm/utility/NumberTraits.h" +#include "storm/utility/Engine.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" @@ -62,13 +63,12 @@ namespace storm { boost::optional> preprocessedProperties; }; - void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) { + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { if (ioSettings.isPrismOrJaniInputSet()) { storm::utility::Stopwatch modelParsingWatch(true); if (ioSettings.isPrismInputSet()) { input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule().isPrismCompatibilityEnabled()); } else { - storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); boost::optional> propertyFilter; if (ioSettings.isJaniPropertiesSet()) { if (ioSettings.areJaniPropertiesSelected()) { @@ -79,7 +79,7 @@ namespace storm { } else { propertyFilter = std::vector(); } - auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures, propertyFilter); + auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), propertyFilter); input.model = std::move(janiInput.first); if (ioSettings.isJaniPropertiesSet()) { input.properties = std::move(janiInput.second); @@ -102,20 +102,48 @@ namespace storm { input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); } } - - SymbolicInput parseSymbolicInput(storm::builder::BuilderType const& builderType) { - auto ioSettings = storm::settings::getModule(); + + SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings) { + // Parse the model input + SymbolicInput input; + storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName()); + STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter())); + storm::utility::Stopwatch modelParsingWatch(true); + auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), ioSettings.getQvbsPropertyFilter()); + input.model = std::move(janiInput.first); + input.properties = std::move(janiInput.second); + modelParsingWatch.stop(); + STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); - // Parse the property filter, if any is given. + // Parse additional properties boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); - - SymbolicInput input; - parseSymbolicModelDescription(ioSettings, input, builderType); parseProperties(ioSettings, input, propertyFilter); + // Substitute constant definitions + auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex())); + input.model = input.model.get().preprocess(constantDefinitions); + if (!input.properties.empty()) { + input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions); + } + return input; } + SymbolicInput parseSymbolicInput() { + auto ioSettings = storm::settings::getModule(); + if (ioSettings.isQvbsInputSet()) { + return parseSymbolicInputQvbs(ioSettings); + } else { + // Parse the property filter, if any is given. + boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); + + SymbolicInput input; + parseSymbolicModelDescription(ioSettings, input); + parseProperties(ioSettings, input, propertyFilter); + return input; + } + } + void ensureNoUndefinedPropertyConstants(std::vector const& properties) { // Make sure there are no undefined constants remaining in any property. for (auto const& property : properties) { @@ -135,6 +163,11 @@ namespace storm { SymbolicInput output = input; + if (output.model && output.model.get().isJaniModel()) { + storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); + storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures); + } + // Substitute constant definitions in symbolic input. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); std::map constantDefinitions; @@ -185,63 +218,28 @@ namespace storm { } } - storm::builder::BuilderType getBuilderType(storm::settings::modules::CoreSettings::Engine const& engine, bool useJit) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + 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::settings::modules::CoreSettings::Engine::Sparse) { + } else if (engine == storm::utility::Engine::Sparse) { if (useJit) { return storm::builder::BuilderType::Jit; } else { return storm::builder::BuilderType::Explicit; } - } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { + } 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 parseAndPreprocessSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings, storm::builder::BuilderType const& builderType) { - // Parse the model input - SymbolicInput input; - storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName()); - STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter())); - storm::utility::Stopwatch modelParsingWatch(true); - storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType); - auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), supportedFeatures, ioSettings.getQvbsPropertyFilter()); - input.model = std::move(janiInput.first); - input.properties = std::move(janiInput.second); - modelParsingWatch.stop(); - STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); - - // Parse additional properties - boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); - parseProperties(ioSettings, input, propertyFilter); - - // Substitute constant definitions - auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex())); - input.model = input.model.get().preprocess(constantDefinitions); - if (!input.properties.empty()) { - input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions); - } - - ensureNoUndefinedPropertyConstants(input.properties); - return input; - } - - SymbolicInput parseAndPreprocessSymbolicInput() { + 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 coreSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); - auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet()); + auto builderType = getBuilderType(engine, buildSettings.isJitSet()); - SymbolicInput input; - if (ioSettings.isQvbsInputSet()) { - input = parseAndPreprocessSymbolicInputQvbs(ioSettings, builderType); - } else { - input = parseSymbolicInput(builderType); - input = preprocessSymbolicInput(input, builderType); - } + SymbolicInput input = parseSymbolicInput(); + input = preprocessSymbolicInput(input, builderType); exportSymbolicInput(input); return input; } @@ -308,7 +306,7 @@ namespace storm { } template - std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr buildModel(storm::utility::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { storm::utility::Stopwatch modelBuildingWatch(true); auto buildSettings = storm::settings::getModule(); @@ -321,7 +319,7 @@ namespace storm { result = buildModelSparse(input, buildSettings); } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); + STORM_LOG_THROW(engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); result = buildModelExplicit(ioSettings, buildSettings); } @@ -479,7 +477,7 @@ namespace storm { result = std::make_unique>, bool>>(symbolicModel->template toValueType(), !std::is_same::value); } - if (result && result->first->isSymbolicModel() && storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::DdSparse) { + if (result && result->first->isSymbolicModel() && storm::settings::getModule().getEngine() == storm::utility::Engine::DdSparse) { // Mark as changed. result->second = true; @@ -903,10 +901,10 @@ namespace storm { template typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { - storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();; - if (engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + storm::utility::Engine engine = coreSettings.getEngine();; + if (engine == storm::utility::Engine::Hybrid) { verifyWithHybridEngine(model, input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Dd) { + } else if (engine == storm::utility::Engine::Dd) { verifyWithDdEngine(model, input); } else { verifyWithAbstractionRefinementEngine(model, input); @@ -929,7 +927,7 @@ namespace storm { } template - std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { + std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine engine) { auto ioSettings = storm::settings::getModule(); auto buildSettings = storm::settings::getModule(); std::shared_ptr model; @@ -961,11 +959,11 @@ namespace storm { auto counterexampleSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. - storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); + storm::utility::Engine engine = coreSettings.getEngine(); - if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { + if (engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { verifyWithAbstractionRefinementEngine(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { + } else if (engine == storm::utility::Engine::Exploration) { verifyWithExplorationEngine(input); } else { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index d290dd47c..7fdf38c1c 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -39,6 +39,7 @@ #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" +#include "storm/utility/Engine.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -207,7 +208,7 @@ namespace storm { PreprocessResult result(model, false); - if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (coreSettings.getEngine() == storm::utility::Engine::Hybrid) { // Currently, hybrid engine for parametric models just refers to building the model symbolically. STORM_LOG_INFO("Translating symbolic model to sparse model..."); result.model = storm::api::transformSymbolicToSparseModel(model); @@ -219,7 +220,7 @@ namespace storm { result.formulas = sparsePreprocessingResult.formulas; } } else { - STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); + STORM_LOG_ASSERT(coreSettings.getEngine() == storm::utility::Engine::Dd, "Expected Dd engine."); if (generalSettings.isBisimulationSet()) { result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as>(), input, bisimulationSettings); result.changed = true; @@ -576,7 +577,7 @@ namespace storm { auto monSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); + STORM_LOG_THROW(engine == storm::utility::Engine::Sparse || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); std::shared_ptr model; if (!buildSettings.isNoBuildModelSet()) { @@ -783,13 +784,13 @@ namespace storm { void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - - // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) - SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); - + auto coreSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); - STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); + STORM_LOG_WARN_COND(engine != storm::utility::Engine::Dd || engine != storm::utility::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); + + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) + SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine); processInputWithValueTypeAndDdlib(symbolicInput); } diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index 983156279..4213b9c52 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -35,8 +35,7 @@ namespace storm { return std::make_pair(std::move(parsedResult.first), std::move(propertyMap)); } - std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter) { - + std::pair> parseJaniModel(std::string const& filename, boost::optional> const& propertyFilter) { bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty(); std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties); @@ -57,13 +56,20 @@ namespace storm { } modelAndFormulae.second = std::move(newProperties); } - modelAndFormulae.first.checkValid(); - auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures, modelAndFormulae.second); - STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of allowed features."); return modelAndFormulae; } + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& supportedFeatures, boost::optional> const& propertyFilter) { + auto modelAndFormulae = parseJaniModel(filename, propertyFilter); + simplifyJaniModel(modelAndFormulae.first, modelAndFormulae.second, supportedFeatures); + return modelAndFormulae; + } + + void simplifyJaniModel(storm::jani::Model& model, std::vector& properties , storm::jani::ModelFeatures const& supportedFeatures) { + auto nonEliminatedFeatures = model.restrictToFeatures(supportedFeatures, properties); + STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of supported features."); + } } } diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index 8e45304c3..0d094b44c 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -20,6 +20,9 @@ namespace storm { storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false, bool simplify = true); std::pair> parseJaniModel(std::string const& filename); + std::pair> parseJaniModel(std::string const& filename, boost::optional> const& propertyFilter = boost::none); std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter = boost::none); + void simplifyJaniModel(storm::jani::Model& model, std::vector& properties , storm::jani::ModelFeatures const& supportedFeatures); + } } diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 9fc95f904..25c0ac954 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -99,9 +99,9 @@ int main(const int argc, const char** argv) { auto const& pomdpSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. - storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); + storm::utility::Engine engine = coreSettings.getEngine(); - storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); + storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine); // We should not export here if we are going to do some processing first. auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, engine); STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP."); diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index bc9ea87fb..19df21f3e 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -32,8 +32,11 @@ namespace storm { const std::string CoreSettings::intelTbbOptionName = "enable-tbb"; const std::string CoreSettings::intelTbbOptionShortName = "tbb"; - CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) { - std::vector engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"}; + CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(storm::utility::Engine::Sparse) { + std::vector engines; + for (auto e : storm::utility::getEngines()) { + engines.push_back(storm::utility::toString(e)); + } this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build()); @@ -133,32 +136,19 @@ namespace storm { return this->getOption(cudaOptionName).getHasOptionBeenSet(); } - CoreSettings::Engine CoreSettings::getEngine() const { + storm::utility::Engine CoreSettings::getEngine() const { return engine; } - void CoreSettings::setEngine(Engine newEngine) { + void CoreSettings::setEngine(storm::utility::Engine const& newEngine) { this->engine = newEngine; } void CoreSettings::finalize() { // Finalize engine. std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); - if (engineStr == "sparse") { - engine = CoreSettings::Engine::Sparse; - } else if (engineStr == "hybrid") { - engine = CoreSettings::Engine::Hybrid; - } else if (engineStr == "dd") { - engine = CoreSettings::Engine::Dd; - } else if (engineStr == "dd-to-sparse") { - engine = CoreSettings::Engine::DdSparse; - } else if (engineStr == "expl") { - engine = CoreSettings::Engine::Exploration; - } else if (engineStr == "abs") { - engine = CoreSettings::Engine::AbstractionRefinement; - } else { - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); - } + engine = storm::utility::engineFromString(engineStr); + STORM_LOG_THROW(engine != storm::utility::Engine::Unknown, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); } bool CoreSettings::check() const { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 405fad91f..c7a2e6f4d 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -5,6 +5,7 @@ #include "storm/settings/modules/ModuleSettings.h" #include "storm/builder/ExplorationOrder.h" +#include "storm/utility/Engine.h" namespace storm { namespace solver { @@ -26,10 +27,6 @@ namespace storm { */ class CoreSettings : public ModuleSettings { public: - // An enumeration of all engines. - enum class Engine { - Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement - }; /*! * Creates a new set of core settings. @@ -118,12 +115,12 @@ namespace storm { * * @return The selected engine. */ - Engine getEngine() const; + storm::utility::Engine getEngine() const; /*! * Sets the engine for further usage. */ - void setEngine(Engine); + void setEngine(storm::utility::Engine const& engine); bool check() const override; void finalize() override; @@ -132,7 +129,7 @@ namespace storm { static const std::string moduleName; private: - Engine engine; + storm::utility::Engine engine; // Define the string names of the options as constants. static const std::string eqSolverOptionName; diff --git a/src/storm/settings/modules/ExplorationSettings.cpp b/src/storm/settings/modules/ExplorationSettings.cpp index 6be2d8c3f..ef86740d2 100644 --- a/src/storm/settings/modules/ExplorationSettings.cpp +++ b/src/storm/settings/modules/ExplorationSettings.cpp @@ -7,6 +7,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/macros.h" +#include "storm/utility/Engine.h" #include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { @@ -91,7 +92,7 @@ namespace storm { this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet(); - STORM_LOG_WARN_COND(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getEngine() == storm::utility::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); return true; } } // namespace modules diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp new file mode 100644 index 000000000..19a719100 --- /dev/null +++ b/src/storm/utility/Engine.cpp @@ -0,0 +1,141 @@ +#include "storm/utility/Engine.h" + +#include "storm/utility/macros.h" + +#include "storm/models/ModelType.h" + +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" + +#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" +#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" + +#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" +#include "storm/modelchecker/CheckTask.h" + +#include "storm/storage/SymbolicModelDescription.h" + +namespace storm { + namespace utility { + + // Returns a list of all available engines (excluding Unknown) + std::vector getEngines() { + std::vector res; + for (int i = 0; i != static_cast(Engine::Unknown); ++i) { + res.push_back(static_cast(i)); + } + return res; + } + + std::string toString(Engine const& engine) { + switch (engine) { + case Engine::Sparse: + return "sparse"; + case Engine::Hybrid: + return "hybrid"; + case Engine::Dd: + return "dd"; + case Engine::DdSparse: + return "dd-to-sparse"; + case Engine::Exploration: + return "expl"; + case Engine::AbstractionRefinement: + return "abs"; + case Engine::Unknown: + return "UNKNOWN"; + default: + STORM_LOG_ASSERT(false, "The given engine has no name assigned to it."); + return "UNKNOWN"; + } + } + + std::ostream& operator<<(std::ostream& os, Engine const& engine) { + os << toString(engine); + return os; + } + + Engine engineFromString(std::string const& engineStr) { + for (Engine const& e : getEngines()) { + if (engineStr == toString(e)) { + return e; + } + } + STORM_LOG_ERROR("The engine '" << engineStr << "' was not found."); + return Engine::Unknown; + } + + template + bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask) { + // Define types to improve readability + typedef storm::models::ModelType ModelType; +#ifdef TODO_IMPLEMENT_CAN_HANDLE_STATIC + switch (engine) { + case Engine::Sparse: + case Engine::DdSparse: + switch (modelType) { + case ModelType::Dtmc: + return storm::modelchecker::SparseDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Mdp: + return storm::modelchecker::SparseMdpPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Ctmc: + return storm::modelchecker::SparseCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::MarkovAutomaton: + return storm::modelchecker::SparseMarkovAutomatonCslModelChecker>::canHandleStatic(checkTask); + case ModelType::S2pg: + case ModelType::Pomdp: + return false; + } + break; + case Engine::Hybrid: + switch (modelType) { + case ModelType::Dtmc: + return storm::modelchecker::HybridDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Mdp: + return storm::modelchecker::HybridMdpPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Ctmc: + return storm::modelchecker::HybridCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::MarkovAutomaton: + case ModelType::S2pg: + case ModelType::Pomdp: + return false; + } + break; + case Engine::Dd: + switch (modelType) { + case ModelType::Dtmc: + return storm::modelchecker::SymbolicDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Mdp: + return storm::modelchecker::SymbolicMdpPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::Ctmc: + case ModelType::MarkovAutomaton: + case ModelType::S2pg: + case ModelType::Pomdp: + return false; + } + break; + default: + STORM_LOG_ERROR("The selected engine" << engine << " is not considered."); + } +#endif + STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType << ") does not seem to be supported for this value type."); + return false; + } + + template + bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask const& checkTask) { + // Check handability based on model type + if (!canHandle(engine, modelDescription.getModelType(), checkTask)) { + return false; + } + // TODO + return true; + } + + + + } +} \ No newline at end of file diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h new file mode 100644 index 000000000..be14f1971 --- /dev/null +++ b/src/storm/utility/Engine.h @@ -0,0 +1,71 @@ +#pragma once + +#include +#include + +#include "storm/models/ModelType.h" +#include "storm/storage/dd/DdType.h" + +namespace storm { + + // Forward Declarations + namespace logic { + class Formula; + } + namespace modelchecker{ + template + class CheckTask; + } + namespace storage { + class SymbolicModelDescription; + } + + namespace utility { + + /// 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 + }; + + /*! + * Returns a list of all available engines (excluding Unknown) + */ + std::vector getEngines(); + + /*! + * Returns a string representation of the given engine. + */ + std::string toString(Engine const& engine); + + /*! + * Writes the string representation of the given engine to the given stream + */ + std::ostream& operator<<(std::ostream& os, Engine const& engine); + + /*! + * Parses the string representation of an engine and returns the corresponding engine. + * If the engine is not found, we print an error and return Engine::Unknown. + */ + Engine engineFromString(std::string const& engineStr); + + /*! + * 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, + * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need + * to actually build the model in order to decide whether it is supported. + */ + template + bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask); + + /*! + * Returns false if the given model description 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, + * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need + * to actually build the model in order to decide whether it is supported. + */ + template + bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription); + + } +} \ No newline at end of file