From 6e8170e386095b8a36d944ecb17bb3a3402dc992 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 1 Apr 2015 15:26:05 +0200
Subject: [PATCH] degen: do not mark initial trivial SCCs as accepting
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Doing so is not wrong, but it's superfluous, and the extra accepting
state will cause additional work in emptiness checks based on NDFS.
Report from Jan Strejček.

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case.
---
 src/tgbaalgos/degen.cc    |  4 ++++
 src/tgbatest/degenid.test | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+)

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<<EOF
+HOA: v1
+name: "a & G(Fb & Fc)"
+States: 4
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant
+--BODY--
+State: 0
+[0] 1
+State: 1 {0}
+[1&2] 1
+[!1&2] 2
+[!2] 3
+State: 2
+[1] 1
+[!1] 2
+State: 3
+[1&2] 1
+[!1&2] 2
+[!2] 3
+--END--
+EOF
+diff out expected