From 2883f81be1a87c152cb50af99c98d3f7540c7387 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 24 May 2019 13:32:36 +0200 Subject: [PATCH] Move settings to separate file --- src/storm-pars-cli/storm-pars.cpp | 10 ++-- src/storm-pars/settings/ParsSettings.cpp | 5 +- .../settings/modules/MonotonicitySettings.cpp | 54 +++++++++++++++++ .../settings/modules/MonotonicitySettings.h | 60 +++++++++++++++++++ .../settings/modules/ParametricSettings.cpp | 32 ---------- .../settings/modules/ParametricSettings.h | 30 ---------- 6 files changed, 124 insertions(+), 67 deletions(-) create mode 100644 src/storm-pars/settings/modules/MonotonicitySettings.cpp create mode 100644 src/storm-pars/settings/modules/MonotonicitySettings.h diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 42415b81a..59bdc61f0 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -13,6 +13,7 @@ #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/MonotonicitySettings.h" #include "storm-pars/settings/modules/RegionSettings.h" #include "storm-pars/transformer/SparseParametricMdpSimplifier.h" @@ -558,6 +559,7 @@ namespace storm { auto buildSettings = storm::settings::getModule(); auto parSettings = storm::settings::getModule(); + auto monSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); @@ -595,7 +597,7 @@ namespace storm { } } - if (parSettings.isMonotonicityAnalysisSet()) { + if (monSettings.isMonotonicityAnalysisSet()) { // Simplify the model storm::utility::Stopwatch simplifyingWatch(true); if (model->isOfType(storm::models::ModelType::Dtmc)) { @@ -650,7 +652,7 @@ namespace storm { } - if (parSettings.isSccEliminationSet()) { + if (monSettings.isSccEliminationSet()) { storm::utility::Stopwatch eliminationWatch(true); // TODO: check for correct Model type STORM_PRINT("Applying scc elimination" << std::endl); @@ -714,11 +716,11 @@ namespace storm { model->printModelInformationToStream(std::cout); } - if (parSettings.isMonotonicityAnalysisSet()) { + if (monSettings.isMonotonicityAnalysisSet()) { std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); // Monotonicity storm::utility::Stopwatch monotonicityWatch(true); - auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, parSettings.isValidateAssumptionsSet(), parSettings.getNumberOfSamples(), parSettings.getMonotonicityAnalysisPrecision()); + auto monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision()); monotonicityChecker.checkMonotonicity(); monotonicityWatch.stop(); STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index d819f8e24..c7eebd767 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -2,6 +2,8 @@ #include "storm-pars/settings/modules/ParametricSettings.h" #include "storm-pars/settings/modules/RegionSettings.h" +#include "storm-pars/settings/modules/MonotonicitySettings.h" + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -28,12 +30,13 @@ namespace storm { namespace settings { void initializeParsSettings(std::string const& name, std::string const& executableName) { storm::settings::mutableManager().setName(name, executableName); - + // Register relevant settings modules. storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pars/settings/modules/MonotonicitySettings.cpp b/src/storm-pars/settings/modules/MonotonicitySettings.cpp new file mode 100644 index 000000000..dd7a91b80 --- /dev/null +++ b/src/storm-pars/settings/modules/MonotonicitySettings.cpp @@ -0,0 +1,54 @@ +#include "storm-pars/settings/modules/MonotonicitySettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string MonotonicitySettings::moduleName = "monotonicity"; + const std::string MonotonicitySettings::monotonicityAnalysis = "monotonicity-analysis"; + const std::string MonotonicitySettings::sccElimination = "mon-elim-scc"; + const std::string MonotonicitySettings::validateAssumptions = "mon-validate-assumptions"; + const std::string MonotonicitySettings::samplesMonotonicityAnalysis = "mon-samples"; + const std::string MonotonicitySettings::precision = "mon-precision"; + + MonotonicitySettings::MonotonicitySettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build()); + + } + + bool MonotonicitySettings::isMonotonicityAnalysisSet() const { + return this->getOption(monotonicityAnalysis).getHasOptionBeenSet(); + } + + bool MonotonicitySettings::isSccEliminationSet() const { + return this->getOption(sccElimination).getHasOptionBeenSet(); + } + + bool MonotonicitySettings::isValidateAssumptionsSet() const { + return this->getOption(validateAssumptions).getHasOptionBeenSet(); + } + + uint_fast64_t MonotonicitySettings::getNumberOfSamples() const { + return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); + } + + double MonotonicitySettings::getMonotonicityAnalysisPrecision() const { + return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble(); + } + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-pars/settings/modules/MonotonicitySettings.h b/src/storm-pars/settings/modules/MonotonicitySettings.h new file mode 100644 index 000000000..f420935cd --- /dev/null +++ b/src/storm-pars/settings/modules/MonotonicitySettings.h @@ -0,0 +1,60 @@ +#ifndef STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ +#define STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ + +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for monotonicity checking. + */ + class MonotonicitySettings : public ModuleSettings { + public: + + /*! + * Creates a new set of monotonicity checking settings. + */ + MonotonicitySettings(); + + /*! + * Retrieves whether monotonicity analysis should be applied. + */ + bool isMonotonicityAnalysisSet() const; + + /*! + * Retrieves whether SCCs in the monotonicity analysis should be eliminated. + */ + bool isSccEliminationSet() const; + + /*! + * Retrieves whether assumptions in monotonicity analysis should be validated + */ + bool isValidateAssumptionsSet() const; + + /*! + * Retrieves the number of samples used for sampling in the monotonicity analysis + */ + uint_fast64_t getNumberOfSamples() const; + + /*! + * Retrieves the precision for the extremal value + */ + double getMonotonicityAnalysisPrecision() const; + + const static std::string moduleName; + + private: + const static std::string monotonicityAnalysis; + const static std::string sccElimination; + const static std::string validateAssumptions; + const static std::string samplesMonotonicityAnalysis; + const static std::string precision; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_MONOTONICITYSETTINGS_H_ */ diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 75d31566e..45528844c 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -21,11 +21,6 @@ namespace storm { const std::string ParametricSettings::samplesOptionName = "samples"; const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving"; const std::string ParametricSettings::sampleExactOptionName = "sample-exact"; - const std::string ParametricSettings::monotonicityAnalysis = "monotonicity-analysis"; - const std::string ParametricSettings::sccElimination = "mon-elim-scc"; - const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions"; - const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples"; - const std::string ParametricSettings::precision = "mon-precision"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.") @@ -37,14 +32,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("samples", "The samples are semicolon-separated entries of the form 'Var1=Val1:Val2:...:Valk,Var2=... that span the sample spaces.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples") - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples") - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build()); - } bool ParametricSettings::exportResultToFile() const { @@ -79,25 +66,6 @@ namespace storm { return this->getOption(sampleExactOptionName).getHasOptionBeenSet(); } - bool ParametricSettings::isMonotonicityAnalysisSet() const { - return this->getOption(monotonicityAnalysis).getHasOptionBeenSet(); - } - - bool ParametricSettings::isSccEliminationSet() const { - return this->getOption(sccElimination).getHasOptionBeenSet(); - } - - bool ParametricSettings::isValidateAssumptionsSet() const { - return this->getOption(validateAssumptions).getHasOptionBeenSet(); - } - - uint_fast64_t ParametricSettings::getNumberOfSamples() const { - return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger(); - } - - double ParametricSettings::getMonotonicityAnalysisPrecision() const { - return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble(); - } } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 60e8fe067..3fe281e4e 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -64,31 +64,6 @@ namespace storm { */ bool isSampleExactSet() const; - /*! - * Retrieves whether monotonicity analysis should be applied. - */ - bool isMonotonicityAnalysisSet() const; - - /*! - * Retrieves whether SCCs in the monotonicity analysis should be eliminated. - */ - bool isSccEliminationSet() const; - - /*! - * Retrieves whether assumptions in monotonicity analysis should be validated - */ - bool isValidateAssumptionsSet() const; - - /*! - * Retrieves the number of samples used for sampling in the monotonicity analysis - */ - uint_fast64_t getNumberOfSamples() const; - - /*! - * Retrieves the precision for the extremal value - */ - double getMonotonicityAnalysisPrecision() const; - const static std::string moduleName; private: @@ -100,11 +75,6 @@ namespace storm { const static std::string samplesOptionName; const static std::string samplesGraphPreservingOptionName; const static std::string sampleExactOptionName; - const static std::string monotonicityAnalysis; - const static std::string sccElimination; - const static std::string validateAssumptions; - const static std::string samplesMonotonicityAnalysis; - const static std::string precision; }; } // namespace modules