Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TopologicalEquationSolverSettings.cpp
Go to the documentation of this file.
2
4
12
14
18
19namespace storm {
20namespace settings {
21namespace modules {
22
23const std::string TopologicalEquationSolverSettings::moduleName = "topological";
24const std::string TopologicalEquationSolverSettings::underlyingEquationSolverOptionName = "eqsolver";
25const std::string TopologicalEquationSolverSettings::underlyingMinMaxMethodOptionName = "minmax";
26const std::string TopologicalEquationSolverSettings::extendRelevantValuesOptionName = "relevant-values";
27
28#ifdef STORM_HAVE_GMM
29const std::string defaultEqSolverString = "gmm++";
30#else
31const std::string defaultEqSolverString = "eigen";
32#endif
33
35 std::vector<std::string> linearEquationSolver = {"gmm++", "native", "eigen", "elimination"};
36 this->addOption(storm::settings::OptionBuilder(moduleName, underlyingEquationSolverOptionName, true,
37 "Sets which solver is considered for solving the underlying equation systems.")
38 .setIsAdvanced()
39 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used solver.")
42 .build())
43 .build());
44 std::vector<std::string> minMaxSolvingTechniques = {
45 "vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch",
46 "ii", "interval-iteration", "svi", "sound-value-iteration", "ovi", "optimistic-value-iteration", "vi-to-pi", "vi-to-lp"};
47 this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true,
48 "Sets which minmax method is considered for solving the underlying minmax equation systems.")
49 .setIsAdvanced()
50 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.")
52 .setDefaultValueString("value-iteration")
53 .build())
54 .build());
55
56 this->addOption(
57 storm::settings::OptionBuilder(moduleName, extendRelevantValuesOptionName, true, "Sets whether relevant values are set to the underlying solver.")
58 .setIsAdvanced()
59 .build());
60}
61
63 return this->getOption(underlyingEquationSolverOptionName).getHasOptionBeenSet();
64}
65
67 return !this->getOption(underlyingEquationSolverOptionName).getHasOptionBeenSet() ||
68 this->getOption(underlyingEquationSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue();
69}
70
72 std::string equationSolverName = this->getOption(underlyingEquationSolverOptionName).getArgumentByName("name").getValueAsString();
73 if (equationSolverName == "gmm++") {
74 return storm::solver::EquationSolverType::Gmmxx;
75 } else if (equationSolverName == "native") {
76 return storm::solver::EquationSolverType::Native;
77 } else if (equationSolverName == "eigen") {
78 return storm::solver::EquationSolverType::Eigen;
79 } else if (equationSolverName == "elimination") {
80 return storm::solver::EquationSolverType::Elimination;
81 }
82 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << equationSolverName << "'.");
83}
84
86 return this->getOption(underlyingMinMaxMethodOptionName).getHasOptionBeenSet();
87}
88
90 return !this->getOption(underlyingMinMaxMethodOptionName).getHasOptionBeenSet() ||
91 this->getOption(underlyingMinMaxMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue();
92}
93
95 std::string minMaxEquationSolvingTechnique = this->getOption(underlyingMinMaxMethodOptionName).getArgumentByName("name").getValueAsString();
96 if (minMaxEquationSolvingTechnique == "value-iteration" || minMaxEquationSolvingTechnique == "vi") {
97 return storm::solver::MinMaxMethod::ValueIteration;
98 } else if (minMaxEquationSolvingTechnique == "policy-iteration" || minMaxEquationSolvingTechnique == "pi") {
99 return storm::solver::MinMaxMethod::PolicyIteration;
100 } else if (minMaxEquationSolvingTechnique == "linear-programming" || minMaxEquationSolvingTechnique == "lp") {
101 return storm::solver::MinMaxMethod::LinearProgramming;
102 } else if (minMaxEquationSolvingTechnique == "ratsearch" || minMaxEquationSolvingTechnique == "rs") {
103 return storm::solver::MinMaxMethod::RationalSearch;
104 } else if (minMaxEquationSolvingTechnique == "interval-iteration" || minMaxEquationSolvingTechnique == "ii") {
105 return storm::solver::MinMaxMethod::IntervalIteration;
106 } else if (minMaxEquationSolvingTechnique == "sound-value-iteration" || minMaxEquationSolvingTechnique == "svi") {
107 return storm::solver::MinMaxMethod::SoundValueIteration;
108 } else if (minMaxEquationSolvingTechnique == "optimistic-value-iteration" || minMaxEquationSolvingTechnique == "ovi") {
109 return storm::solver::MinMaxMethod::OptimisticValueIteration;
110 } else if (minMaxEquationSolvingTechnique == "vi-to-pi") {
111 return storm::solver::MinMaxMethod::ViToPi;
112 } else if (minMaxEquationSolvingTechnique == "vi-to-lp") {
113 return storm::solver::MinMaxMethod::ViToLp;
114 }
115
116 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << minMaxEquationSolvingTechnique << "'.");
117}
118
120 return this->getOption(extendRelevantValuesOptionName).getHasOptionBeenSet();
121}
122
124 if (this->isUnderlyingEquationSolverTypeSet() && getUnderlyingEquationSolverType() == storm::solver::EquationSolverType::Topological) {
125 STORM_LOG_WARN("Underlying solver type of the topological solver can not be the topological solver.");
126 return false;
127 }
128 if (this->isUnderlyingMinMaxMethodSet() && getUnderlyingMinMaxMethod() == storm::solver::MinMaxMethod::Topological) {
129 STORM_LOG_WARN("Underlying minmax method of the topological solver can not be topological.");
130 return false;
131 }
132 return true;
133}
134
135} // namespace modules
136} // namespace settings
137} // namespace storm
virtual std::string getValueAsString() const =0
Retrieves the value of this argument as a string.
virtual bool wasSetFromDefaultValue() const =0
static ArgumentBuilder createStringArgument(std::string const &name, std::string const &description)
Creates a string argument with the given parameters.
static std::shared_ptr< ArgumentValidator< std::string > > createMultipleChoiceValidator(std::vector< std::string > const &choices)
This class provides the interface to create an option...
ArgumentBase const & getArgumentByName(std::string const &argumentName) const
Returns a reference to the argument with the specified long name.
Definition Option.cpp:79
bool getHasOptionBeenSet() const
Retrieves whether the option has been set.
Definition Option.cpp:125
This is the base class of the settings for a particular module.
void addOption(std::shared_ptr< Option > const &option)
Adds and registers the given option.
Option & getOption(std::string const &longName)
Retrieves the option with the given long name.
bool check() const override
Checks whether the settings are consistent.
bool isUnderlyingMinMaxMethodSet() const
Retrieves whether the underlying equation solver type has been set.
bool isUnderlyingMinMaxMethodSetFromDefaultValue() const
Retrieves whether the underlying minmax method is set from its default value.
TopologicalEquationSolverSettings()
Creates a new set of native equation solver settings.
bool isUnderlyingEquationSolverTypeSetFromDefaultValue() const
Retrieves whether the underlying equation solver type is set from its default value.
bool isExtendRelevantValues() const
If true, the relevant states of each SCC are computed and passed to the underlying equation solver.
storm::solver::EquationSolverType getUnderlyingEquationSolverType() const
Retrieves the method that is to be used for solving systems of linear equations.
storm::solver::MinMaxMethod getUnderlyingMinMaxMethod() const
Retrieves the method that is to be used for solving systems of linear equations.
bool isUnderlyingEquationSolverTypeSet() const
Retrieves whether the underlying equation solver type has been set.
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SettingsType const & getModule()
Get module.
LabParser.cpp.
Definition cli.cpp:18