From f0d1aff610234dbce4a94534233d0b8d1fe08829 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 3 Mar 2020 14:35:55 +0100 Subject: [PATCH] Added new settings and environment module for time-bounded settings. --- src/storm/environment/SubEnvironment.cpp | 2 + .../environment/solver/SolverEnvironment.cpp | 9 +++ .../environment/solver/SolverEnvironment.h | 4 ++ .../solver/TimeBoundedSolverEnvironment.cpp | 60 +++++++++++++++++ .../solver/TimeBoundedSolverEnvironment.h | 36 ++++++++++ src/storm/settings/SettingsManager.cpp | 2 + .../modules/TimeBoundedSolverSettings.cpp | 62 +++++++++++++++++ .../modules/TimeBoundedSolverSettings.h | 66 +++++++++++++++++++ src/storm/solver/SolverSelectionOptions.cpp | 10 +++ src/storm/solver/SolverSelectionOptions.h | 1 + 10 files changed, 252 insertions(+) create mode 100644 src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp create mode 100644 src/storm/environment/solver/TimeBoundedSolverEnvironment.h create mode 100644 src/storm/settings/modules/TimeBoundedSolverSettings.cpp create mode 100644 src/storm/settings/modules/TimeBoundedSolverSettings.h diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index c42e21c93..8e5a23e83 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -9,6 +9,7 @@ #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/TimeBoundedSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/MultiplierEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" @@ -65,6 +66,7 @@ namespace storm { template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; + template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 07a02aca1..9825d926b 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -1,6 +1,7 @@ #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/TimeBoundedSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/MultiplierEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" @@ -38,6 +39,14 @@ namespace storm { return longRunAverageSolverEnvironment.get(); } + TimeBoundedSolverEnvironment& SolverEnvironment::timeBounded() { + return timeBoundedSolverEnvironment.get(); + } + + TimeBoundedSolverEnvironment const& SolverEnvironment::timeBounded() const { + return timeBoundedSolverEnvironment.get(); + } + MinMaxSolverEnvironment& SolverEnvironment::minMax() { return minMaxSolverEnvironment.get(); } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 26ac33fea..4f0a88869 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -15,6 +15,7 @@ namespace storm { class GmmxxSolverEnvironment; class NativeSolverEnvironment; class LongRunAverageSolverEnvironment; + class TimeBoundedSolverEnvironment; class MinMaxSolverEnvironment; class MultiplierEnvironment; class GameSolverEnvironment; @@ -34,6 +35,8 @@ namespace storm { NativeSolverEnvironment const& native() const; LongRunAverageSolverEnvironment& lra(); LongRunAverageSolverEnvironment const& lra() const; + TimeBoundedSolverEnvironment& timeBounded(); + TimeBoundedSolverEnvironment const& timeBounded() const; MinMaxSolverEnvironment& minMax(); MinMaxSolverEnvironment const& minMax() const; MultiplierEnvironment& multiplier(); @@ -60,6 +63,7 @@ namespace storm { SubEnvironment gameSolverEnvironment; SubEnvironment topologicalSolverEnvironment; SubEnvironment longRunAverageSolverEnvironment; + SubEnvironment timeBoundedSolverEnvironment; SubEnvironment minMaxSolverEnvironment; SubEnvironment multiplierEnvironment; diff --git a/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp new file mode 100644 index 000000000..743474e4b --- /dev/null +++ b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp @@ -0,0 +1,60 @@ +#include "storm/environment/solver/TimeBoundedSolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/TimeBoundedSolverSettings.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + + TimeBoundedSolverEnvironment::TimeBoundedSolverEnvironment() { + auto const& tbSettings = storm::settings::getModule(); + maMethod = tbSettings.getMaMethod(); + maMethodSetFromDefault = tbSettings.isMaMethodSetFromDefaultValue(); + precision = storm::utility::convertNumber(tbSettings.getPrecision()); + relative = tbSettings.isRelativePrecision(); + unifPlusKappa = tbSettings.getUnifPlusKappa(); + } + + TimeBoundedSolverEnvironment::~TimeBoundedSolverEnvironment() { + // Intentionally left empty + } + + storm::solver::MaBoundedReachabilityMethod const& TimeBoundedSolverEnvironment::getMaMethod() const { + return maMethod; + } + + bool const& TimeBoundedSolverEnvironment::isMaMethodSetFromDefault() const { + return maMethodSetFromDefault; + } + + void TimeBoundedSolverEnvironment::setMaMethod(storm::solver::MaBoundedReachabilityMethod value, bool isSetFromDefault) { + maMethod = value; + maMethodSetFromDefault = isSetFromDefault; + } + + storm::RationalNumber const& TimeBoundedSolverEnvironment::getPrecision() const { + return precision; + } + + void TimeBoundedSolverEnvironment::setPrecision(storm::RationalNumber value) { + precision = value; + } + + bool const& TimeBoundedSolverEnvironment::getRelativeTerminationCriterion() const { + return relative; + } + + void TimeBoundedSolverEnvironment::setRelativeTerminationCriterion(bool value) { + relative = value; + } + + storm::RationalNumber const& TimeBoundedSolverEnvironment::getUnifPlusKappa() const { + return unifPlusKappa; + } + + void TimeBoundedSolverEnvironment::setUnifPlusKappa(storm::RationalNumber value) { + unifPlusKappa = value; + } + +} diff --git a/src/storm/environment/solver/TimeBoundedSolverEnvironment.h b/src/storm/environment/solver/TimeBoundedSolverEnvironment.h new file mode 100644 index 000000000..ddf1d8321 --- /dev/null +++ b/src/storm/environment/solver/TimeBoundedSolverEnvironment.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/solver/SolverSelectionOptions.h" + +namespace storm { + + class TimeBoundedSolverEnvironment { + public: + + TimeBoundedSolverEnvironment(); + ~TimeBoundedSolverEnvironment(); + + storm::solver::MaBoundedReachabilityMethod const& getMaMethod() const; + bool const& isMaMethodSetFromDefault() const; + void setMaMethod(storm::solver::MaBoundedReachabilityMethod value, bool isSetFromDefault = false); + + storm::RationalNumber const& getPrecision() const; + void setPrecision(storm::RationalNumber value); + bool const& getRelativeTerminationCriterion() const; + void setRelativeTerminationCriterion(bool value); + + storm::RationalNumber const& getUnifPlusKappa() const; + void setUnifPlusKappa(storm::RationalNumber value); + + private: + storm::solver::MaBoundedReachabilityMethod maMethod; + bool maMethodSetFromDefault; + + storm::RationalNumber precision; + bool relative; + + storm::RationalNumber unifPlusKappa; + }; +} + diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8e278fecb..4824ce135 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -32,6 +32,7 @@ #include "storm/settings/modules/GurobiSettings.h" #include "storm/settings/modules/Smt2SmtSolverSettings.h" #include "storm/settings/modules/TopologicalEquationSolverSettings.h" +#include "storm/settings/modules/TimeBoundedSolverSettings.h" #include "storm/settings/modules/ExplorationSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/AbstractionSettings.h" @@ -657,6 +658,7 @@ namespace storm { 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/settings/modules/TimeBoundedSolverSettings.cpp b/src/storm/settings/modules/TimeBoundedSolverSettings.cpp new file mode 100644 index 000000000..88b323c8f --- /dev/null +++ b/src/storm/settings/modules/TimeBoundedSolverSettings.cpp @@ -0,0 +1,62 @@ +#include "storm/settings/modules/TimeBoundedSolverSettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/OptionBuilder.h" + +#include "storm/utility/macros.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string TimeBoundedSolverSettings::moduleName = "timebounded"; + + const std::string TimeBoundedSolverSettings::maMethodOptionName = "mamethod"; + const std::string TimeBoundedSolverSettings::precisionOptionName = "precision"; + const std::string TimeBoundedSolverSettings::absoluteOptionName = "absolute"; + const std::string TimeBoundedSolverSettings::unifPlusKappaOptionName = "kappa"; + + TimeBoundedSolverSettings::TimeBoundedSolverSettings() : ModuleSettings(moduleName) { + std::vector maMethods = {"imca", "unifplus"}; + this->addOption(storm::settings::OptionBuilder(moduleName, maMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, unifPlusKappaOptionName, false, "The truncation factor used in unifPlus.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("kappa", "The factor").setDefaultValueDouble(0.1).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + } + + bool TimeBoundedSolverSettings::isPrecisionSet() const { + return this->getOption(precisionOptionName).getHasOptionBeenSet(); + } + + double TimeBoundedSolverSettings::getPrecision() const { + return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); + } + + bool TimeBoundedSolverSettings::isRelativePrecision() const { + return !this->getOption(absoluteOptionName).getHasOptionBeenSet(); + } + + storm::solver::MaBoundedReachabilityMethod TimeBoundedSolverSettings::getMaMethod() const { + std::string techniqueAsString = this->getOption(maMethodOptionName).getArgumentByName("name").getValueAsString(); + if (techniqueAsString == "imca") { + return storm::solver::MaBoundedReachabilityMethod::Imca; + } + return storm::solver::MaBoundedReachabilityMethod::UnifPlus; + } + + bool TimeBoundedSolverSettings::isMaMethodSetFromDefaultValue() const { + return !this->getOption(maMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(maMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + + double TimeBoundedSolverSettings::getUnifPlusKappa() const { + return this->getOption(unifPlusKappaOptionName).getArgumentByName("kappa").getValueAsDouble(); + } + + } + } +} diff --git a/src/storm/settings/modules/TimeBoundedSolverSettings.h b/src/storm/settings/modules/TimeBoundedSolverSettings.h new file mode 100644 index 000000000..8140da9ce --- /dev/null +++ b/src/storm/settings/modules/TimeBoundedSolverSettings.h @@ -0,0 +1,66 @@ +#pragma once + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" + +#include "storm/solver/SolverSelectionOptions.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the min/max solver settings. + */ + class TimeBoundedSolverSettings : public ModuleSettings { + public: + + TimeBoundedSolverSettings(); + + /*! + * Retrieves whether solving technique for time bounded reachability on Markov Automata has been set from its default value. + */ + bool isMaMethodSetFromDefaultValue() const; + + /*! + * Retrieves the selected solving technique for time bounded reachability on Markov Automata. + */ + storm::solver::MaBoundedReachabilityMethod getMaMethod() const; + + /*! + * Retrieves whether the precision has been set. + * + * @return True iff the precision has been set. + */ + bool isPrecisionSet() const; + + /*! + * Retrieves the precision that is used for detecting convergence. + * + * @return The precision to use for detecting convergence. + */ + double getPrecision() const; + + /*! + * Retrieves whether the convergence criterion has been set to relative or absolute. + */ + bool isRelativePrecision() const; + + /*! + * Retrieves the truncation factor used for unifPlus + */ + double getUnifPlusKappa() const; + + // The name of the module. + static const std::string moduleName; + + private: + static const std::string maMethodOptionName; + static const std::string precisionOptionName; + static const std::string absoluteOptionName; + static const std::string unifPlusKappaOptionName; + }; + + } + } +} diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index f635b5a38..2b913c2ae 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -60,6 +60,16 @@ namespace storm { return "invalid"; } + std::string toString(MaBoundedReachabilityMethod m) { + switch(m) { + case MaBoundedReachabilityMethod::Imca: + return "imca"; + case MaBoundedReachabilityMethod::UnifPlus: + return "unifplus"; + } + return "invalid"; + } + std::string toString(LpSolverType t) { switch(t) { case LpSolverType::Gurobi: diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index d21262099..e6d38274b 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -10,6 +10,7 @@ namespace storm { ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration, GainBiasEquations, LraDistributionEquations) + ExtendEnumsWithSelectionField(MaBoundedReachabilityMethod, Imca, UnifPlus) ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological)