From 1fe30f7d785ac449624a120813ad86c64cd08766 Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Wed, 19 May 2021 02:03:11 +0200
Subject: [PATCH] Convert acceptance formula into disjunctive normal form

---
 src/storm/automata/LTL2DeterministicAutomaton.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
index 3833db73e..5383745ed 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.cpp
+++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp
@@ -11,6 +11,9 @@
 #include "spot/tl/parse.hh"
 #include "spot/twaalgos/translate.hh"
 #include "spot/twaalgos/hoa.hh"
+#include "spot/twaalgos/totgba.hh"
+#include "spot/twaalgos/toparity.hh"
+#include "spot/twa/acc.hh"
 #endif
 
 namespace storm {
@@ -36,6 +39,11 @@ namespace storm {
             STORM_LOG_INFO("Construct deterministic automaton for "<< spotFormula);
             auto aut = trans.run(spotFormula);
 
+            // TODO necessary for MDP LTL-MC
+            if(!(aut->get_acceptance().is_dnf())){
+                aut->set_acceptance(aut->get_acceptance().to_dnf());
+            }
+
             std::stringstream autStream;
             // Print reachable states in HOA format, implicit edges (i), state-based acceptance (s)
             spot::print_hoa(autStream, aut, "is");