Renamed portfolio engine to automatic engine.

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.

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::settings::modules::HintSettings>();
             
-            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<storm::jani::Property> 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;

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());
                 

src/storm/utility/Portfolio.cpp → src/storm/utility/AutomaticSettings.cpp

@@ -1,4 +1,4 @@
-#include "storm/utility/Portfolio.h"
+#include "storm/utility/AutomaticSettings.h"
 
 #include <sstream>
 
@@ -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;

src/storm/utility/Portfolio.h → 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

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;
         }

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
         };
         
         /*!