From 9ec7df670e36e770ef62a78e182439bd367fa96e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 22 Dec 2017 17:53:30 +0100
Subject: [PATCH] to_tgba: fix handling of CNF with multiple unit clauses
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #313, reported by František Blahoudek.

* spot/twaalgos/totgba.cc (to_generalized_buchi): Fix it.
* tests/core/remfin.test: Test it.
* NEWS: Mention it.
---
 NEWS                    |  6 +++
 spot/twaalgos/totgba.cc |  9 ++++-
 tests/core/remfin.test  | 86 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 99 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 18998208e..bd82deb0d 100644
--- a/NEWS
+++ b/NEWS
@@ -242,6 +242,12 @@ New in spot 2.4.3.dev (not yet released)
     been removed.  It's a low-level function was not used anywhere in
     Spot anymore, since it's better to use spot::twa::copy_ap_of().
 
+  Bugs fixed:
+
+  - The generic to_generalized_buchi() function would fail if the
+    Fin-less & CNF version of the acceptance condition had several
+    unit clauses.
+
 New in spot 2.4.3 (2017-12-19)
 
   Bugs fixed:
diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc
index f77843efe..41ea61202 100644
--- a/spot/twaalgos/totgba.cc
+++ b/spot/twaalgos/totgba.cc
@@ -478,7 +478,8 @@ namespace spot
       while (pos >= end)
         {
           auto term_end = pos - 1 - pos->sub.size;
-          if (pos->sub.op == acc_cond::acc_op::Or)
+          bool inor = pos->sub.op == acc_cond::acc_op::Or;
+          if (inor)
             --pos;
           acc_cond::mark_t m = 0U;
           while (pos > term_end)
@@ -487,7 +488,11 @@ namespace spot
               m |= pos[-1].mark;
               pos -= 2;
             }
-          res.emplace_back(m);
+          if (inor)
+            res.emplace_back(m);
+          else
+            for (unsigned i: m.sets())
+              res.emplace_back(acc_cond::mark_t({i}));
         }
       return res;
     }
diff --git a/tests/core/remfin.test b/tests/core/remfin.test
index 9003375f8..12437b69d 100755
--- a/tests/core/remfin.test
+++ b/tests/core/remfin.test
@@ -268,6 +268,29 @@ HOA: v1 States: 3 Start: 0 AP: 2 "b" "c" Acceptance: 3 Fin(0) &
 complete --BODY-- State: 0 [!0] 0 {1 2} [0] 0 {0 1 2} [0&!1] 1 [0&1] 2
 State: 1 [!0 | !1] 1 {1 2} [0&1] 2 {1} State: 2 [!1] 1 {1 2} [1] 2 {1}
 --END--
+/*
+** Issue #313.  The TGBA conversion of this automaton was wrong.
+*/
+HOA: v1
+States: 2
+Start: 0
+AP: 3 "a" "b" "c"
+Acceptance: 4 (Fin(1)|Fin(2)) & Fin(0) & Inf(3)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 0 {0 3}
+[1 | 2] 0 {1 3}
+[0] 0 {2 3}
+[!1&!2] 1 {1}
+State: 1
+[2] 0 {0 3}
+[2] 0 {1 3}
+[0&2] 0 {2 3}
+[!2] 1 {0}
+[!2] 1 {1}
+[0&!2] 1 {2}
+--END--
 EOF
 
 acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
@@ -842,6 +865,37 @@ State: 3
 [!1] 2 {0 1}
 [1] 3 {0}
 --END--
+HOA: v1
+States: 6
+Start: 0
+AP: 3 "a" "b" "c"
+Acceptance: 4 (Inf(0)&Inf(2)&Inf(3)) | (Inf(0)&Inf(1)&Inf(3))
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[t] 0
+[!1&!2] 1
+[0] 2
+[1 | 2] 4
+State: 1
+[2] 0
+[!2] 1
+[0&2] 2
+[0&!2] 3
+[2] 4
+[!2] 5
+State: 2
+[0] 2 {0 1 3}
+State: 3
+[0&2] 2 {0 1 3}
+[0&!2] 3 {0 1}
+State: 4
+[1 | 2] 4 {0 2 3}
+[!1&!2] 5 {0 2}
+State: 5
+[2] 4 {0 2 3}
+[!2] 5 {0 2}
+--END--
 EOF
 
 cat >expected-tgba <<EOF
@@ -1408,6 +1462,38 @@ State: 3
 [!1] 2 {0}
 [1] 3
 --END--
+HOA: v1
+States: 6
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[t] 0
+[!1&!2] 1
+[0] 2
+[1 | 2] 4
+State: 1
+[2] 0
+[!2] 1
+[0&2] 2
+[0&!2] 3
+[2] 4
+[!2] 5
+State: 2
+[0] 2 {0}
+State: 3
+[0&2] 2
+[0&!2] 3
+State: 4
+[1 | 2] 4 {0}
+[!1&!2] 5
+State: 5
+[2] 4 {0}
+[!2] 5
+--END--
 EOF
 
 run 0 autfilt -H --remove-fin test1 > output