From bb7d8ca3c5a787500ff37c399f9853f8b8ecd806 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 11 Mar 2016 19:05:19 +0100
Subject: [PATCH] added learning as new engine selection in options
Former-commit-id: e00c7ad75d19b93437d998291cc48147ad694564
---
src/cli/entrypoints.h | 9 ++++++++-
src/settings/modules/GeneralSettings.cpp | 6 ++++--
src/settings/modules/GeneralSettings.h | 2 +-
src/utility/storm.h | 2 +-
4 files changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index bbb9d6404..359d58d13 100644
--- a/src/cli/entrypoints.h
+++ b/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 {
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 95a48931b..122cb23ad 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/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 {
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 8144c0a1f..f2cbdca47 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/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
};
/*!
diff --git a/src/utility/storm.h b/src/utility/storm.h
index b01b03516..a7a717b8d 100644
--- a/src/utility/storm.h
+++ b/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.");
}
}