diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 7a0271171..5e53740be 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -72,6 +72,7 @@ namespace spot acc_cond::mark_t common = a_->acc().all_sets(); acc_cond::mark_t union_ = 0U; bool has_acc_self_loop = false; + bool seen = false; for (auto& t: a_->out(s)) { // Ignore transitions that leave the SCC of s. @@ -85,7 +86,10 @@ namespace spot // an accepting self-loop? has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc); + seen = true; } + if (!seen) + common = 0U; cache_[s] = std::make_tuple(common, union_, has_acc_self_loop); } diff --git a/src/tgbatest/degenid.test b/src/tgbatest/degenid.test index 1d7e2b505..91c3af5a7 100755 --- a/src/tgbatest/degenid.test +++ b/src/tgbatest/degenid.test @@ -222,3 +222,35 @@ EOF run 0 ../../bin/dstar2tgba in.dra -BD --stats=%s > out.stat test 6 = "`cat out.stat`" + +# Only one state should be accepting. In spot 1.2.x an initial state +# in a trivial SCC was marked as accepting: this is superfluous. +../../bin/ltl2tgba -BH 'a & GFb & GFc' > out +cat out +cat >expected<