From a038d9658eb6db9c59e2479b25dd89051ed7d02a Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Sun, 13 Jun 2021 18:39:00 +0200
Subject: [PATCH] added TODOs

---
 src/storm/automata/LTL2DeterministicAutomaton.cpp          | 3 ++-
 .../modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp     | 7 +++----
 src/storm/transformer/DAProductBuilder.h                   | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
index 0f07e2a4e..d780bf979 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.cpp
+++ b/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");
diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index 95e87164f..fedbb5895 100644
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/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();
             }
 
diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h
index d90d4b6dc..a6a53f9bd 100644
--- a/src/storm/transformer/DAProductBuilder.h
+++ b/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(),