From 225169b2b38398357c8a70d585bcec29e4c36f1d Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 18 Jun 2021 09:24:39 +0200 Subject: [PATCH] added ltl2da option --- .../automata/LTL2DeterministicAutomaton.cpp | 29 +++++-------------- .../automata/LTL2DeterministicAutomaton.h | 20 +++++++++---- .../modelchecker/ModelCheckerEnvironment.cpp | 25 +++++++++++++++- .../modelchecker/ModelCheckerEnvironment.h | 8 ++++- .../helper/ltl/SparseLTLHelper.cpp | 16 ++++++++-- .../settings/modules/ModelCheckerSettings.cpp | 10 +++++++ .../settings/modules/ModelCheckerSettings.h | 17 ++++++++++- 7 files changed, 93 insertions(+), 32 deletions(-) diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index d780bf979..bef88aaaf 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -22,12 +22,10 @@ namespace storm { namespace automata { - bool LTL2DeterministicAutomaton::isExternalDaToolSet() { - return std::getenv("LTL2DA"); - } - std::shared_ptr LTL2DeterministicAutomaton::ltl2daInternalTool(std::string const& prefixLtl, bool dnf) { + std::shared_ptr LTL2DeterministicAutomaton::ltl2daSpot(storm::logic::Formula const& f, bool dnf) { #ifdef STORM_HAVE_SPOT + std::string prefixLtl = f.toPrefixString(); spot::parsed_formula spotPrefixLtl = spot::parse_prefix_ltl(prefixLtl); if(!spotPrefixLtl.errors.empty()){ @@ -68,12 +66,10 @@ namespace storm { } // TODO: this is quite hacky, improve robustness - std::shared_ptr LTL2DeterministicAutomaton::ltl2daExternalTool(std::string const& prefixLtl) { - - - std::string ltl2da_tool = std::getenv("LTL2DA"); + std::shared_ptr LTL2DeterministicAutomaton::ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool) { + std::string prefixLtl = f.toPrefixString(); - STORM_LOG_INFO("Calling external LTL->DA tool: " << ltl2da_tool << " '" << prefixLtl << "' da.hoa"); + STORM_LOG_INFO("Calling external LTL->DA tool: " << ltl2daTool << " '" << prefixLtl << "' da.hoa"); pid_t pid; @@ -82,7 +78,7 @@ namespace storm { if (pid == 0) { // we are in the child process - if (execlp(ltl2da_tool.c_str(), ltl2da_tool.c_str(), prefixLtl.c_str(), "da.hoa", NULL) < 0) { + if (execlp(ltl2daTool.c_str(), ltl2daTool.c_str(), prefixLtl.c_str(), "da.hoa", NULL) < 0) { std::cerr << "ERROR: exec failed: " << strerror(errno) << std::endl; std::exit(1); } @@ -110,17 +106,6 @@ namespace storm { } } - std::shared_ptr LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f, bool dnf) { - std::string prefixLtl = f.toPrefixString(); - - storm::automata::DeterministicAutomaton::ptr da; - if(isExternalDaToolSet()){ - da = ltl2daExternalTool(prefixLtl); - } else { - da = ltl2daInternalTool(prefixLtl, dnf); - } - return da; - } - } + } diff --git a/src/storm/automata/LTL2DeterministicAutomaton.h b/src/storm/automata/LTL2DeterministicAutomaton.h index 1471922d3..4134e326f 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.h +++ b/src/storm/automata/LTL2DeterministicAutomaton.h @@ -15,13 +15,23 @@ namespace storm { class LTL2DeterministicAutomaton { public: - static std::shared_ptr ltl2da(storm::logic::Formula const&, bool dnf); - private: - static bool isExternalDaToolSet(); + /*! + * TODO + * @param f + * @param dnf + * @return + */ + static std::shared_ptr ltl2daSpot(storm::logic::Formula const& f, bool dnf); + + /*! + * TODO + * @param f + * @param ltl2daTool + * @return + */ + static std::shared_ptr ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool); - static std::shared_ptr ltl2daInternalTool(std::string const& prefixLtl, bool dnf); - static std::shared_ptr ltl2daExternalTool(std::string const& prefixLtl); }; } diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp index f0d917a28..8836d57be 100644 --- a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp @@ -3,6 +3,7 @@ #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidEnvironmentException.h" @@ -12,7 +13,10 @@ namespace storm { ModelCheckerEnvironment::ModelCheckerEnvironment() { - // Intentionally left empty + auto const& mcSettings = storm::settings::getModule(); + if (mcSettings.isLtl2daSet()) { + ltl2da = mcSettings.getLtl2da(); + } } ModelCheckerEnvironment::~ModelCheckerEnvironment() { @@ -26,6 +30,25 @@ namespace storm { MultiObjectiveModelCheckerEnvironment const& ModelCheckerEnvironment::multi() const { return multiObjectiveModelCheckerEnvironment.get(); } + + bool ModelCheckerEnvironment::isLtl2daSet() const { + return ltl2da.is_initialized(); + } + + boost::optional const& ModelCheckerEnvironment::getLtl2da() const { + return ltl2da; + } + + void ModelCheckerEnvironment::setLtl2da(std::string const& value) { + ltl2da = value; + } + + void ModelCheckerEnvironment::unsetLtl2da() { + ltl2da = boost::none; + } + + + } diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h index 2ec1eebd8..416172a36 100644 --- a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h @@ -20,9 +20,15 @@ namespace storm { MultiObjectiveModelCheckerEnvironment& multi(); MultiObjectiveModelCheckerEnvironment const& multi() const; - + bool isLtl2daSet() const; + boost::optional const& getLtl2da() const; + void setLtl2da(std::string const& value); + void unsetLtl2da(); + + private: SubEnvironment multiObjectiveModelCheckerEnvironment; + boost::optional ltl2da; }; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index ea6df66fc..89ab5737d 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -15,6 +15,8 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + namespace storm { namespace modelchecker { namespace helper { @@ -272,11 +274,21 @@ namespace storm { ltlFormula = formula.asSharedPointer(); } - STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula->toString()); STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); - std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, Nondeterministic); + // Convert LTL formula to a deterministic automaton + std::shared_ptr da; + if (env.modelchecker().isLtl2daSet()) { + // Use the external tool given via ltl2da + std::string ltl2da = env.modelchecker().getLtl2da().get(); + da = storm::automata::LTL2DeterministicAutomaton::ltl2daExternalTool(*ltlFormula, ltl2da); + } + else { + // Use the internal tool (Spot) + // For nondeterministic models the acceptance condition is transformed into DNF + da = storm::automata::LTL2DeterministicAutomaton::ltl2daSpot(*ltlFormula, Nondeterministic); + } STORM_LOG_INFO("Deterministic automaton for LTL formula has " << da->getNumberOfStates() << " states, " diff --git a/src/storm/settings/modules/ModelCheckerSettings.cpp b/src/storm/settings/modules/ModelCheckerSettings.cpp index da0b64d8e..c68cc5a6b 100644 --- a/src/storm/settings/modules/ModelCheckerSettings.cpp +++ b/src/storm/settings/modules/ModelCheckerSettings.cpp @@ -14,14 +14,24 @@ namespace storm { const std::string ModelCheckerSettings::moduleName = "modelchecker"; const std::string ModelCheckerSettings::filterRewZeroOptionName = "filterrewzero"; + const std::string ModelCheckerSettings::ltl2daName = "ltl2da"; 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()); } bool ModelCheckerSettings::isFilterRewZeroSet() const { return this->getOption(filterRewZeroOptionName).getHasOptionBeenSet(); } + + bool ModelCheckerSettings::isLtl2daSet() const { + return this->getOption(ltl2daName).getHasOptionBeenSet(); + } + + std::string ModelCheckerSettings::getLtl2da() const { + return this->getOption(ltl2daName).getArgumentByName("filename").getValueAsString(); + } } // namespace modules } // namespace settings diff --git a/src/storm/settings/modules/ModelCheckerSettings.h b/src/storm/settings/modules/ModelCheckerSettings.h index 4c6a1dfd6..2f731690f 100644 --- a/src/storm/settings/modules/ModelCheckerSettings.h +++ b/src/storm/settings/modules/ModelCheckerSettings.h @@ -19,15 +19,30 @@ namespace storm { * Creates a new set of general settings. */ ModelCheckerSettings(); - + bool isFilterRewZeroSet() const; + /*! + * Retrieves whether the external ltl2da tool has been set. + * + * @return True iff the external ltl2da has been set. + */ + bool isLtl2daSet() 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; + // The name of the module. static const std::string moduleName; private: // Define the string names of the options as constants. static const std::string filterRewZeroOptionName; + static const std::string ltl2daName; }; } // namespace modules