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 LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f) { + std::shared_ptr 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 ltl2da(storm::logic::Formula const& f); + static std::shared_ptr ltl2da(storm::logic::Formula const&, bool dnf); }; }