From 24ba65f5e19f458e82d47a0f624ae8d2e91a79eb Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Aug 2021 15:44:17 +0200 Subject: [PATCH] added documentation --- .../automata/LTL2DeterministicAutomaton.cpp | 2 -- .../automata/LTL2DeterministicAutomaton.h | 21 ++++++++++++------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index e33939f7b..6e1636961 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -96,8 +96,6 @@ namespace storm { } STORM_LOG_THROW(rv == 0, storm::exceptions::FileIoException, "Could not construct deterministic automaton for " << prefixLtl << ", return code = " << rv); - // Transition-based acceptance is required. - // For MDP-MC the acceptance condition must be in DNF, otherwise an exception is thrown during computation if accepting ECs STORM_LOG_INFO("Reading automaton for " << prefixLtl << " from da.hoa"); return DeterministicAutomaton::parseFromFile("da.hoa"); diff --git a/src/storm/automata/LTL2DeterministicAutomaton.h b/src/storm/automata/LTL2DeterministicAutomaton.h index 4134e326f..94669138f 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.h +++ b/src/storm/automata/LTL2DeterministicAutomaton.h @@ -17,18 +17,23 @@ namespace storm { public: /*! - * TODO - * @param f - * @param dnf - * @return + * Converts an LTL formula into a deterministic omega-automaton using the internal LTL2DA tool "Spot". + * The resulting DA uses transition-based acceptance and if specified the acceptance condition is converted to DNF. + * + * @param f The LTL formula. + * @param dnf A Flag indicating whether the acceptance condition is transformed into DNF. + * @return An automaton equivalent to the formula. */ static std::shared_ptr ltl2daSpot(storm::logic::Formula const& f, bool dnf); /*! - * TODO - * @param f - * @param ltl2daTool - * @return + * Converts an LTL formula into a deterministic omega-automaton using an external LTL2DA tool. + * The external tool must guarantee transition-based acceptance. + * Additionally, for MDP model checking, the acceptance condition of the resulting automaton must be in DNF. + * + * @param f The LTL formula. + * @param ltl2daTool The external tool. + * @return An automaton equivalent to the formula. */ static std::shared_ptr ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool);