From f596d7f4868375dc177b693259011ad5de17252e Mon Sep 17 00:00:00 2001 From: hannah Date: Mon, 5 Jul 2021 09:23:01 +0200 Subject: [PATCH] fixed output --- src/storm/automata/LTL2DeterministicAutomaton.cpp | 1 + src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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; }