Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
BisimulationSettings.cpp
Go to the documentation of this file.
8
10
11namespace storm {
12namespace settings {
13namespace modules {
14
15const std::string BisimulationSettings::moduleName = "bisimulation";
16const std::string BisimulationSettings::typeOptionName = "type";
17const std::string BisimulationSettings::representativeOptionName = "repr";
18const std::string BisimulationSettings::originalVariablesOptionName = "origvars";
19const std::string BisimulationSettings::quotientFormatOptionName = "quot";
20const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
21const std::string BisimulationSettings::reuseOptionName = "reuse";
22const std::string BisimulationSettings::initialPartitionOptionName = "init";
23const std::string BisimulationSettings::refinementModeOptionName = "refine";
24const std::string BisimulationSettings::exactArithmeticDdOptionName = "ddexact";
25
27 std::vector<std::string> types = {"strong", "weak"};
28 this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used.")
29 .setIsAdvanced()
30 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.")
32 .setDefaultValueString("strong")
33 .build())
34 .build());
35
36 std::vector<std::string> quotTypes = {"sparse", "dd"};
37 this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true,
38 "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).")
39 .setIsAdvanced()
40 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.")
43 .build())
44 .build());
45
46 this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false,
47 "Sets whether to use representatives in the quotient rather than block numbers.")
48 .setIsAdvanced()
49 .build());
50 this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false,
51 "Sets whether to use the original variables in the quotient rather than the block variables.")
52 .setIsAdvanced()
53 .build());
54 this->addOption(
55 storm::settings::OptionBuilder(moduleName, exactArithmeticDdOptionName, false, "Sets whether to use exact arithmetic in dd-based bisimulation.")
56 .setIsAdvanced()
57 .build());
58
59 std::vector<std::string> signatureModes = {"eager", "lazy"};
60 this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.")
61 .setIsAdvanced()
62 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
64 .setDefaultValueString("eager")
65 .build())
66 .build());
67
68 std::vector<std::string> reuseModes = {"none", "blocks"};
69 this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.")
70 .setIsAdvanced()
71 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
73 .setDefaultValueString("blocks")
74 .build())
75 .build());
76
77 std::vector<std::string> initialPartitionModes = {"regular", "finer"};
78 this->addOption(storm::settings::OptionBuilder(moduleName, initialPartitionOptionName, true, "Sets which initial partition mode to use.")
79 .setIsAdvanced()
80 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
82 .setDefaultValueString("finer")
83 .build())
84 .build());
85
86 std::vector<std::string> refinementModes = {"full", "changed"};
87 this->addOption(storm::settings::OptionBuilder(moduleName, refinementModeOptionName, true, "Sets which refinement mode to use.")
88 .setIsAdvanced()
89 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
92 .build())
93 .build());
94}
95
97 if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "strong") {
98 return true;
99 }
100 return false;
101}
102
104 if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "weak") {
105 return true;
106 }
107 return false;
108}
109
111 return !this->getOption(quotientFormatOptionName).getHasOptionBeenSet() ||
112 this->getOption(quotientFormatOptionName).getArgumentByName("format").wasSetFromDefaultValue();
113}
114
123
125 return this->getOption(representativeOptionName).getHasOptionBeenSet();
126}
127
129 return this->getOption(originalVariablesOptionName).getHasOptionBeenSet();
130}
131
133 return this->getOption(exactArithmeticDdOptionName).getHasOptionBeenSet();
134}
135
137 std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString();
138 if (modeAsString == "eager") {
140 } else if (modeAsString == "lazy") {
142 }
143 STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unknown signature mode '" << modeAsString << ".");
144}
145
147 std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString();
148 if (reuseModeAsString == "none") {
149 return ReuseMode::None;
150 } else if (reuseModeAsString == "blocks") {
152 }
154}
155
165
167 std::string refinementModeAsString = this->getOption(refinementModeOptionName).getArgumentByName("mode").getValueAsString();
168 if (refinementModeAsString == "full") {
170 } else if (refinementModeAsString == "changed") {
172 }
174}
175
177 bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet();
179 "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");
180 return true;
181}
182} // namespace modules
183} // namespace settings
184} // 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
virtual bool check() const override
Checks whether the settings are consistent.
InitialPartitionMode getInitialPartitionMode() const
Retrieves the initial partition mode.
RefinementMode getRefinementMode() const
Retrieves the refinement mode to use.
storm::dd::bisimulation::QuotientFormat getQuotientFormat() const
Retrieves the format in which the quotient is to be extracted.
storm::dd::bisimulation::SignatureMode getSignatureMode() const
Retrieves the mode to compute signatures.
bool isUseOriginalVariablesSet() const
Retrieves whether the extracted quotient model is supposed to use the same variables as the original ...
BisimulationSettings()
Creates a new set of bisimulation settings.
bool isQuotientFormatSetFromDefaultValue() const
Retrieves whether the format in which the quotient is to be extracted has been set from its default v...
bool isUseRepresentativesSet() const
Retrieves whether representatives for blocks are to be used instead of the block numbers.
bool useExactArithmeticInDdBisimulation() const
Retrieves whether exact arithmetic is to be used in symbolic bisimulation minimization.
bool isStrongBisimulationSet() const
Retrieves whether strong bisimulation is to be used.
ReuseMode getReuseMode() const
Retrieves the selected reuse mode.
bool isWeakBisimulationSet() const
Retrieves whether weak bisimulation is to be used.
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.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SettingsType const & getModule()
Get module.
LabParser.cpp.
Definition cli.cpp:18