diff --git a/CHANGELOG.md b/CHANGELOG.md index 5976115a8..d9b1274da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,8 @@ Version 1.6.x ## Version 1.6.1 (??) - Prism program simplification improved. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata. -- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). +- Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine). +- Renamed portfolio engine to automatic - `storm-dft`: Fix for relevant events when using symmetry reduction. - `storm-pomdp`: Fix for --transformsimple and --transformbinary when used with until formulae. - `storm-pomdp`: POMDPs can be parametric as well. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d5f27ec14..f630e67df 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -10,7 +10,7 @@ #include "storm/utility/macros.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Engine.h" -#include "storm/utility/Portfolio.h" +#include "storm/utility/AutomaticSettings.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" @@ -178,30 +178,30 @@ namespace storm { bool isCompatible; }; - void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) { + void getModelProcessingInformationAutomatic(SymbolicInput const& input, ModelProcessingInformation& mpi) { auto hints = storm::settings::getModule(); - STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); - STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model."); + STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); + STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a JANI input model."); std::vector const& properties = input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties; - STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a property."); - STORM_LOG_WARN_COND(properties.size() == 1, "Portfolio engine does not support decisions based on multiple properties. Only the first property will be considered."); + STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Automatic engine requires a property."); + STORM_LOG_WARN_COND(properties.size() == 1, "Automatic engine does not support decisions based on multiple properties. Only the first property will be considered."); - storm::utility::Portfolio pf; + storm::utility::AutomaticSettings as; if (hints.isNumberStatesSet()) { - pf.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); + as.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates()); } else { - pf.predict(input.model->asJaniModel(), properties.front()); + as.predict(input.model->asJaniModel(), properties.front()); } - mpi.engine = pf.getEngine(); - if (pf.enableBisimulation()) { + mpi.engine = as.getEngine(); + if (as.enableBisimulation()) { mpi.applyBisimulation = true; } - if (pf.enableExact() && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision) { + if (as.enableExact() && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision) { mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact; } - STORM_PRINT_AND_LOG( "Portfolio engine picked the following settings: " << std::endl + STORM_PRINT_AND_LOG( "Automatic engine picked the following settings: " << std::endl << "\tengine=" << mpi.engine << std::boolalpha << "\t bisimulation=" << mpi.applyBisimulation @@ -237,12 +237,12 @@ namespace storm { } auto originalVerificationValueType = mpi.verificationValueType; - // Since the remaining settings could depend on the ones above, we need apply the portfolio engine now. - bool usePortfolio = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Portfolio; - if (usePortfolio) { + // Since the remaining settings could depend on the ones above, we need apply the automatic engine now. + bool useAutomatic = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Automatic; + if (useAutomatic) { if (input.model->isJaniModel()) { // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) - getModelProcessingInformationPortfolio(input, mpi); + getModelProcessingInformationAutomatic(input, mpi); } else { // Transform Prism to jani first STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input."); @@ -255,7 +255,7 @@ namespace storm { janiInput.preprocessedProperties = std::move(modelAndProperties.second); } // This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic) - getModelProcessingInformationPortfolio(janiInput, mpi); + getModelProcessingInformationAutomatic(janiInput, mpi); if (transformedJaniInput) { // We cache the transformation result. *transformedJaniInput = std::move(janiInput); @@ -279,9 +279,9 @@ namespace storm { }; mpi.isCompatible = checkCompatibleSettings(); if (!mpi.isCompatible) { - if (usePortfolio) { + if (useAutomatic) { bool useExact = mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision; - STORM_LOG_WARN("The settings picked by the portfolio engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); + STORM_LOG_WARN("The settings picked by the automatic engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); mpi.engine = storm::utility::Engine::Sparse; mpi.applyBisimulation = false; mpi.verificationValueType = originalVerificationValueType; diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index d520f930b..d56081287 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -37,6 +37,8 @@ namespace storm { for (auto e : storm::utility::getEngines()) { engines.push_back(storm::utility::toString(e)); } + engines.push_back("portfolio"); // for backwards compatibility + 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()); diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/AutomaticSettings.cpp similarity index 92% rename from src/storm/utility/Portfolio.cpp rename to src/storm/utility/AutomaticSettings.cpp index f23ae66af..39a9aed7c 100644 --- a/src/storm/utility/Portfolio.cpp +++ b/src/storm/utility/AutomaticSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/Portfolio.h" +#include "storm/utility/AutomaticSettings.h" #include @@ -90,14 +90,14 @@ namespace storm { }; } - Portfolio::Portfolio() : engine(storm::utility::Engine::Unknown), useBisimulation(false), useExact(false) { + AutomaticSettings::AutomaticSettings() : engine(storm::utility::Engine::Unknown), useBisimulation(false), useExact(false) { // Intentionally left empty } - void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property) { + void AutomaticSettings::predict(storm::jani::Model const& model, storm::jani::Property const& property) { typedef pfinternal::PropertyType PropertyType; auto f = pfinternal::Features(model, property); - STORM_LOG_INFO("Portfolio engine using features " << f.toString() << "."); + STORM_LOG_INFO("Automatic engine using features " << f.toString() << "."); if (f.numVariables <= 12) { if (f.avgDomainSize <= 323.25) { @@ -218,54 +218,54 @@ namespace storm { } } - void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t) { + void AutomaticSettings::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t) { //typedef pfinternal::PropertyType PropertyType; //auto f = pfinternal::Features(model, property); //f.stateEstimate = stateEstimate; - //STORM_LOG_INFO("Portfolio engine using features " << f.toString() << "."); + //STORM_LOG_INFO("Automatic engine using features " << f.toString() << "."); // Right now, we do not make use of the state estimate, so we just ask the 'default' decision tree. predict(model, property); } - storm::utility::Engine Portfolio::getEngine() const { + storm::utility::Engine AutomaticSettings::getEngine() const { STORM_LOG_THROW(engine != storm::utility::Engine::Unknown, storm::exceptions::InvalidOperationException, "Tried to get the engine but apparently no prediction was done before."); return engine; } - bool Portfolio::enableBisimulation() const { + bool AutomaticSettings::enableBisimulation() const { return useBisimulation; } - bool Portfolio::enableExact() const { + bool AutomaticSettings::enableExact() const { return useExact; } - void Portfolio::sparse() { + void AutomaticSettings::sparse() { engine = storm::utility::Engine::Sparse; useBisimulation = false; useExact = false; } - void Portfolio::hybrid() { + void AutomaticSettings::hybrid() { engine = storm::utility::Engine::Hybrid; useBisimulation = false; useExact = false; } - void Portfolio::dd() { + void AutomaticSettings::dd() { engine = storm::utility::Engine::Dd; useBisimulation = false; useExact = false; } - void Portfolio::exact() { + void AutomaticSettings::exact() { engine = storm::utility::Engine::Sparse; useBisimulation = false; useExact = true; } - void Portfolio::ddbisim() { + void AutomaticSettings::ddbisim() { engine = storm::utility::Engine::DdSparse; useBisimulation = true; useExact = false; diff --git a/src/storm/utility/Portfolio.h b/src/storm/utility/AutomaticSettings.h similarity index 95% rename from src/storm/utility/Portfolio.h rename to src/storm/utility/AutomaticSettings.h index 472369bc7..2d3a7c7f7 100644 --- a/src/storm/utility/Portfolio.h +++ b/src/storm/utility/AutomaticSettings.h @@ -10,9 +10,9 @@ namespace storm { } namespace utility { - class Portfolio { + class AutomaticSettings { public: - Portfolio(); + AutomaticSettings(); /*! * Predicts "good" settings for the provided model checking query diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 3c892c8b9..8eaecde4e 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -51,8 +51,8 @@ namespace storm { return "expl"; case Engine::AbstractionRefinement: return "abs"; - case Engine::Portfolio: - return "portfolio"; + case Engine::Automatic: + return "automatic"; case Engine::Unknown: return "UNKNOWN"; default: @@ -72,6 +72,10 @@ namespace storm { return e; } } + if (engineStr == "portfolio") { + STORM_LOG_WARN("The engine name \"portfolio\" is deprecated. The name of this engine has been changed to \"" << toString(Engine::Automatic) << "\"."); + return Engine::Automatic; + } STORM_LOG_ERROR("The engine '" << engineStr << "' was not found."); return Engine::Unknown; } diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index b193eb448..03dfd922a 100644 --- a/src/storm/utility/Engine.h +++ b/src/storm/utility/Engine.h @@ -30,7 +30,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, Jit, Exploration, AbstractionRefinement, Portfolio, Unknown + Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Automatic, Unknown }; /*!