diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 010698ac7..9a4ad13af 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -11,6 +11,7 @@ #include "storm/utility/macros.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Engine.h" +#include "storm/utility/Portfolio.h" #include "storm/utility/initialize.h" #include "storm/utility/Stopwatch.h" @@ -46,6 +47,7 @@ #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/TransformationSettings.h" +#include "storm/settings/modules/HintSettings.h" #include "storm/storage/Qvbs.h" #include "storm/utility/Stopwatch.h" @@ -147,6 +149,7 @@ namespace storm { } struct ModelProcessingInformation { + // The engine to use storm::utility::Engine engine; @@ -169,6 +172,30 @@ namespace storm { storm::Environment env; }; + void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) { + auto hints = storm::settings::getModule(); + + STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a symbolic model (PRISM or JANI."); + 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::utility::Portfolio pf; + if (hints.isNumberStatesSet()) { + pf.predict(input.model.get(), properties.front(), hints.getNumberStates()); + } else { + pf.predict(input.model.get(), properties.front()); + } + + mpi.engine = pf.getEngine(); + if (pf.enableBisimulation()) { + mpi.applyBisimulation = true; + } + if (pf.enableExact() && mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision) { + mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact; + } + } + ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input) { ModelProcessingInformation mpi; auto coreSettings = storm::settings::getModule(); @@ -190,8 +217,36 @@ namespace storm { 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 + // Since the remaining settings could depend on the ones above, we need apply the portfolio engine now. + bool usePortfolio = mpi.engine == storm::utility::Engine::Portfolio; + if (usePortfolio) { + // 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); + } + + // Check whether these settings are compatible with the provided input. + bool incompatibleSettings = false; + if (input.model) { + switch (mpi.verificationValueType) { + case ModelProcessingInformation::ValueType::Parametric: + incompatibleSettings = storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + case ModelProcessingInformation::ValueType::Exact: + incompatibleSettings = storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + case ModelProcessingInformation::ValueType::FinitePrecision: + incompatibleSettings = storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + } + } + if (incompatibleSettings) { + if (usePortfolio) { + STORM_LOG_WARN("The settings picked by the portfolio engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << (mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision) << ") are incompatible with this model. Falling back to sparse engine without bisimulation and floating point arithmetic."); + mpi.engine = storm::utility::Engine::Sparse; + mpi.applyBisimulation = false; + mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecision; + } else { + STORM_LOG_WARN("The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties."); + } + } + // Set the Valuetype used during model building mpi.buildValueType = mpi.verificationValueType; diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 345dc6a8e..ac03324d1 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -48,6 +48,8 @@ namespace storm { return "expl"; case Engine::AbstractionRefinement: return "abs"; + case Engine::Portfolio: + return "portfolio"; case Engine::Unknown: return "UNKNOWN"; default: diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index 3254749a9..b193eb448 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, Unknown + Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Portfolio, Unknown }; /*! diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/Portfolio.cpp new file mode 100644 index 000000000..5ea49b720 --- /dev/null +++ b/src/storm/utility/Portfolio.cpp @@ -0,0 +1,37 @@ +#include "storm/utility/Portfolio.h" + +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/jani/Property.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace utility { + Portfolio::Portfolio() : engine(storm::utility::Engine::Unknown), bisimulation(false), exact(false) { + // Intentionally left empty + } + + void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) { + + } + + void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate) { + + } + + storm::utility::Engine Portfolio::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 { + return bisimulation; + } + + bool Portfolio::enableExact() const { + return exact; + } + + } +} \ No newline at end of file diff --git a/src/storm/utility/Portfolio.h b/src/storm/utility/Portfolio.h new file mode 100644 index 000000000..17af90af7 --- /dev/null +++ b/src/storm/utility/Portfolio.h @@ -0,0 +1,46 @@ +#pragma once + +#include "storm/utility/Engine.h" + +namespace storm { + + namespace jani { + class Property; + } + + namespace storage { + class SymbolicModelDescription; + } + + namespace utility { + class Portfolio { + public: + Portfolio(); + + /*! + * Predicts "good" settings for the provided model checking query + */ + void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property); + + /*! + * Predicts "good" settings for the provided model checking query + * @param stateEstimate A hint that gives a (rough) estimate for the number of states. + */ + void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate); + + /// Retrieve "good" settings after calling predict. + storm::utility::Engine getEngine() const; + bool enableBisimulation() const; + bool enableExact() const; + + private: + storm::utility::Engine engine; + bool bisimulation; + bool exact; + + + + }; + + } +} \ No newline at end of file