From c8e9b431009df1d273d7cf3e1940f0d91d95a7cb Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 9 Aug 2021 12:21:33 +0200 Subject: [PATCH] Changed ltl2da option to slightly more descriptive ltl2datool (this is also the name of the corresponding option in PRISM) --- .../modelchecker/ModelCheckerEnvironment.cpp | 20 +++++++++---------- .../modelchecker/ModelCheckerEnvironment.h | 11 +++++----- .../helper/ltl/SparseLTLHelper.cpp | 5 ++--- .../settings/modules/ModelCheckerSettings.cpp | 12 +++++------ .../settings/modules/ModelCheckerSettings.h | 6 +++--- 5 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp index 8836d57be..6dbb25890 100644 --- a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp @@ -14,8 +14,8 @@ namespace storm { ModelCheckerEnvironment::ModelCheckerEnvironment() { auto const& mcSettings = storm::settings::getModule(); - if (mcSettings.isLtl2daSet()) { - ltl2da = mcSettings.getLtl2da(); + if (mcSettings.isLtl2daToolSet()) { + ltl2daTool = mcSettings.getLtl2daTool(); } } @@ -31,20 +31,20 @@ namespace storm { return multiObjectiveModelCheckerEnvironment.get(); } - bool ModelCheckerEnvironment::isLtl2daSet() const { - return ltl2da.is_initialized(); + bool ModelCheckerEnvironment::isLtl2daToolSet() const { + return ltl2daTool.is_initialized(); } - boost::optional const& ModelCheckerEnvironment::getLtl2da() const { - return ltl2da; + std::string const& ModelCheckerEnvironment::getLtl2daTool() const { + return ltl2daTool.get(); } - void ModelCheckerEnvironment::setLtl2da(std::string const& value) { - ltl2da = value; + void ModelCheckerEnvironment::setLtl2daTool(std::string const& value) { + ltl2daTool = value; } - void ModelCheckerEnvironment::unsetLtl2da() { - ltl2da = boost::none; + void ModelCheckerEnvironment::unsetLtl2daTool() { + ltl2daTool = boost::none; } diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h index b5bca9835..6867a487c 100644 --- a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h @@ -21,15 +21,16 @@ namespace storm { MultiObjectiveModelCheckerEnvironment& multi(); MultiObjectiveModelCheckerEnvironment const& multi() const; - bool isLtl2daSet() const; - boost::optional const& getLtl2da() const; - void setLtl2da(std::string const& value); - void unsetLtl2da(); + + bool isLtl2daToolSet() const; + std::string const& getLtl2daTool() const; + void setLtl2daTool(std::string const& value); + void unsetLtl2daTool(); private: SubEnvironment multiObjectiveModelCheckerEnvironment; - boost::optional ltl2da; + boost::optional ltl2daTool; }; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index da1a32a93..8215aa4b3 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -595,10 +595,9 @@ namespace storm { // Convert LTL formula to a deterministic automaton std::shared_ptr da; - if (env.modelchecker().isLtl2daSet()) { + if (env.modelchecker().isLtl2daToolSet()) { // Use the external tool given via ltl2da - std::string ltl2da = env.modelchecker().getLtl2da().get(); - da = storm::automata::LTL2DeterministicAutomaton::ltl2daExternalTool(*ltlFormula, ltl2da); + da = storm::automata::LTL2DeterministicAutomaton::ltl2daExternalTool(*ltlFormula, env.modelchecker().getLtl2daTool()); } else { // Use the internal tool (Spot) diff --git a/src/storm/settings/modules/ModelCheckerSettings.cpp b/src/storm/settings/modules/ModelCheckerSettings.cpp index c68cc5a6b..d54e8a92e 100644 --- a/src/storm/settings/modules/ModelCheckerSettings.cpp +++ b/src/storm/settings/modules/ModelCheckerSettings.cpp @@ -14,23 +14,23 @@ namespace storm { const std::string ModelCheckerSettings::moduleName = "modelchecker"; const std::string ModelCheckerSettings::filterRewZeroOptionName = "filterrewzero"; - const std::string ModelCheckerSettings::ltl2daName = "ltl2da"; + const std::string ModelCheckerSettings::ltl2daToolOptionName = "ltl2datool"; ModelCheckerSettings::ModelCheckerSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, filterRewZeroOptionName, false, "If set, states with reward zero are filtered out, potentially reducing the size of the equation system").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, ltl2daName, false, "If set, use an external tool to convert LTL formulas to state-based deterministic automata in HOA format").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A script that can be called with a prefix formula and a name for the output automaton.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, ltl2daToolOptionName, false, "If set, use an external tool to convert LTL formulas to state-based deterministic automata in HOA format").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A script that can be called with a prefix formula and a name for the output automaton.").build()).build()); } bool ModelCheckerSettings::isFilterRewZeroSet() const { return this->getOption(filterRewZeroOptionName).getHasOptionBeenSet(); } - bool ModelCheckerSettings::isLtl2daSet() const { - return this->getOption(ltl2daName).getHasOptionBeenSet(); + bool ModelCheckerSettings::isLtl2daToolSet() const { + return this->getOption(ltl2daToolOptionName).getHasOptionBeenSet(); } - std::string ModelCheckerSettings::getLtl2da() const { - return this->getOption(ltl2daName).getArgumentByName("filename").getValueAsString(); + std::string ModelCheckerSettings::getLtl2daTool() const { + return this->getOption(ltl2daToolOptionName).getArgumentByName("filename").getValueAsString(); } } // namespace modules diff --git a/src/storm/settings/modules/ModelCheckerSettings.h b/src/storm/settings/modules/ModelCheckerSettings.h index 2f731690f..6d5511863 100644 --- a/src/storm/settings/modules/ModelCheckerSettings.h +++ b/src/storm/settings/modules/ModelCheckerSettings.h @@ -27,14 +27,14 @@ namespace storm { * * @return True iff the external ltl2da has been set. */ - bool isLtl2daSet() const; + bool isLtl2daToolSet() const; /*! * Retrieves the external ltl2da tool that is used for converting LTL formulas to deterministic automata. * * @return The executable to use for converting LTL formulas to deterministic automata. */ - std::string getLtl2da() const; + std::string getLtl2daTool() const; // The name of the module. static const std::string moduleName; @@ -42,7 +42,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string filterRewZeroOptionName; - static const std::string ltl2daName; + static const std::string ltl2daToolOptionName; }; } // namespace modules