diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index c70158354..52e1192f0 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -47,6 +47,7 @@ namespace storm { aut = to_generalized_rabin(aut,true); } + STORM_LOG_INFO("The deterministic automaton has acceptance condition: "<< aut->get_acceptance()); STORM_LOG_INFO(aut->get_acceptance()); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index f564c8221..d80f4a64f 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -38,7 +38,7 @@ namespace storm { auto sat = subResult.getTruthValuesVector(); apSets[p.first] = std::move(sat); - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << apSets[p.first].getNumberOfSetBits() << " states."); } return apSets; }