added TODOs

src/storm/automata/LTL2DeterministicAutomaton.cpp

@@ -102,7 +102,8 @@ namespace storm {
                 }
                 STORM_LOG_THROW(rv == 0, storm::exceptions::FileIoException, "Could not construct deterministic automaton for " << prefixLtl << ", return code = " << rv);
 
-                // TODO for MDP-MC the acceptance condition must be in DNF, otherwise Exception is thrown during computation if accepting ECs
+                // TODO transition-based acceptance is required,
+                //  and 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/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -22,8 +22,6 @@
 #include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
 
 #include "storm/automata/AcceptanceCondition.h"
-#include "storm/automata/DeterministicAutomaton.h"
-#include "storm/automata/LTL2DeterministicAutomaton.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
 
@@ -160,7 +158,7 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
 
             STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
-
+            // TODO simplify APs
             std::map<std::string, storm::storage::BitVector> apSets;
             for (auto& p : extracted) {
                 STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
@@ -176,10 +174,11 @@ namespace storm {
 
             const SparseDtmcModelType& dtmc = this->getModel();
 
+            // TODO ?
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");
-                this->getModel().writeDotToStream(modelDot);
+                dtmc.writeDotToStream(modelDot);
                 modelDot.close();
             }
 

src/storm/transformer/DAProductBuilder.h

@@ -22,7 +22,7 @@ namespace storm {
             }
 
             template <typename Model>
-            typename DAProduct<Model>::ptr build(const storm::storage::SparseMatrix<typename Model::ValueType>& originalMatrix, const storm::storage::BitVector& statesOfInterest) const { //todo transition matrix
+            typename DAProduct<Model>::ptr build(const storm::storage::SparseMatrix<typename Model::ValueType>& originalMatrix, const storm::storage::BitVector& statesOfInterest) const {
                 typename Product<Model>::ptr product = ProductBuilder<Model>::buildProduct(originalMatrix, *this, statesOfInterest);
                 storm::automata::AcceptanceCondition::ptr prodAcceptance
                         = da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(),