added learning as new engine selection in options

Former-commit-id: e00c7ad75d

src/cli/entrypoints.h

@@ -53,6 +53,11 @@ namespace storm {
         void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
         }
+        
+        template<typename ValueType>
+        void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
+        }
 
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
@@ -120,6 +125,8 @@ namespace storm {
 
             if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
                 verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas, onlyInitialStatesRelevant);
+            } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning) {
+                verifySymbolicModelWithLearningEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
             } else {
                 storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
                 STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
@@ -136,7 +143,7 @@ namespace storm {
                     if (modelFormulasPair.model->isSparseModel()) {
                         if (storm::settings::generalSettings().isCounterexampleSet()) {
                             // If we were requested to generate a counterexample, we now do so for each formula.
-                            for (auto const &formula : modelFormulasPair.formulas) {
+                            for (auto const& formula : modelFormulasPair.formulas) {
                                 generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
                             }
                         } else {

src/settings/modules/GeneralSettings.cpp

@@ -96,9 +96,9 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).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).build());
                 
-                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "abs"};
+                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "learn", "abs"};
                 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. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, learn, abs}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
@@ -346,6 +346,8 @@ namespace storm {
                     engine = GeneralSettings::Engine::Hybrid;
                 } else if (engineStr == "dd") {
                     engine = GeneralSettings::Engine::Dd;
+                } else if (engineStr == "learn") {
+                    engine = GeneralSettings::Engine::Learning;
                 } else if (engineStr == "abs") {
                     engine = GeneralSettings::Engine::AbstractionRefinement;
                 } else {

src/settings/modules/GeneralSettings.h

@@ -27,7 +27,7 @@ namespace storm {
                 // An enumeration of all engines.
 
                 enum class Engine {
-                    Sparse, Hybrid, Dd, AbstractionRefinement
+                    Sparse, Hybrid, Dd, Learning, AbstractionRefinement
                 };
 
                 /*!

src/utility/storm.h

@@ -254,7 +254,7 @@ namespace storm {
                 STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
                 return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
-            case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
+            default: {
                 STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
             }
         }