From 7c55500d0ea85f0d89899d2c9403a0c524b7d238 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 13 Jan 2015 18:02:13 +0100 Subject: [PATCH] never: fix output of accepting initial states * src/tgbaalgos/neverclaim.cc: Make sure the any accepting initial state is not output as an accept_all state. This bug caused ltl2dstar.test to fail. --- src/tgbaalgos/neverclaim.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 7624317d3..0c75b0fa4 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -126,7 +126,8 @@ namespace spot void process_state(unsigned n) { - if (aut_->state_is_accepting(n) && is_sink(n)) + if (aut_->state_is_accepting(n) && is_sink(n) + && n != aut_->get_init_state_number()) { // We want the accept_all state at the end of the never claim. need_accept_all_ = true;