From 139ac3d0dc61e6f8a00f5a999d1461439dbadf1d Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Wed, 26 May 2021 12:39:19 +0200
Subject: [PATCH] flag to indicate whether condition should be in dnf

---
 src/storm/automata/LTL2DeterministicAutomaton.cpp | 5 +++--
 src/storm/automata/LTL2DeterministicAutomaton.h   | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
index 5383745ed..06ceb5f03 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.cpp
+++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp
@@ -19,7 +19,7 @@
 namespace storm {
     namespace automata {
 
-        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f) {
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f, bool dnf) {
 #ifdef STORM_HAVE_SPOT
 
             std::string prefixLtl = f.toPrefixString();
@@ -40,7 +40,8 @@ namespace storm {
             auto aut = trans.run(spotFormula);
 
             // TODO necessary for MDP LTL-MC
-            if(!(aut->get_acceptance().is_dnf())){
+            if(!(aut->get_acceptance().is_dnf()) && dnf){
+                STORM_LOG_INFO("Convert acceptance condition into DNF...");
                 aut->set_acceptance(aut->get_acceptance().to_dnf());
             }
 
diff --git a/src/storm/automata/LTL2DeterministicAutomaton.h b/src/storm/automata/LTL2DeterministicAutomaton.h
index c39f1b235..32be1ca32 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.h
+++ b/src/storm/automata/LTL2DeterministicAutomaton.h
@@ -17,7 +17,7 @@ namespace storm {
 
         class LTL2DeterministicAutomaton {
         public:
-            static std::shared_ptr<DeterministicAutomaton> ltl2da(storm::logic::Formula const& f);
+            static std::shared_ptr<DeterministicAutomaton> ltl2da(storm::logic::Formula const&, bool dnf);
         };
 
     }