From 071d819c495a1ccbde73ea861cbeef18998ae1cb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 24 Dec 2016 18:32:21 +0100
Subject: [PATCH] complete: add support for alternating autamata

* spot/twaalgos/complete.cc: Do not use the initial
state as a sink if it is universal.
* tests/core/complete.test: Add a test case.
---
 spot/twaalgos/complete.cc |  9 ++++---
 tests/core/complete.test  | 51 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc
index 9ddcda168..cef86c619 100644
--- a/spot/twaalgos/complete.cc
+++ b/spot/twaalgos/complete.cc
@@ -49,7 +49,7 @@ namespace spot
           {
             bool sinkable = true;
             bool first = true;
-            acc_cond::mark_t commonacc = 0U;
+            acc_cond::mark_t commonacc = um.second;
             for (auto& t: aut->out(i))
               {
                 if (t.dst != i)        // Not a self-loop
@@ -80,11 +80,12 @@ namespace spot
 
     unsigned t = aut->num_edges();
 
-    // If the automaton is empty, pretend that state 0 is a sink.
-    if (t == 0)
+    // If the automaton is empty, and the initial state is not
+    // universal, pretend this is the sink.
+    if (t == 0 && !aut->is_univ_dest(aut->get_init_state_number()))
       sink = aut->get_init_state_number();
 
-    // Now complete all states (excluding any newly added the sink).
+    // Now complete all states (excluding any newly added sink).
     for (unsigned i = 0; i < n; ++i)
       {
         bdd missingcond = bddtrue;
diff --git a/tests/core/complete.test b/tests/core/complete.test
index 27a76d931..e69042b79 100755
--- a/tests/core/complete.test
+++ b/tests/core/complete.test
@@ -82,6 +82,27 @@ State: 1
 [0] 1 {0}
 [!0] 1 {0}
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Fin(0)
+properties: very-weak
+--BODY--
+State: 0
+[!0 | 1] 0
+[0&!1] 1&0
+State: 1 {0}
+[0&!1] 1
+--END--
+HOA: v1
+States: 2
+Start: 0&1
+Acceptance: 1 Fin(0)
+--BODY--
+State: 0
+State: 1 {0}
+--END--
 EOF
 
 cat >expected <<EOF
@@ -171,6 +192,36 @@ State: 1 {0}
 [0] 1
 [!0] 1
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete
+properties: deterministic very-weak
+--BODY--
+State: 0
+[!0 | 1] 0
+[0&!1] 1&0
+State: 1 {0}
+[0&!1] 1
+[!0 | 1] 1
+--END--
+HOA: v1
+States: 2
+Start: 0&1
+AP: 0
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0
+State: 1
+[t] 0
+--END--
 EOF
 
 run 0 autfilt -CH automaton >out