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");