added documentation

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");

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<DeterministicAutomaton> 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<DeterministicAutomaton> ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool);