to_tgba: fix handling of CNF with multiple unit clauses

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

@@ -1,6 +1,10 @@
 New in spot 2.4.3.dev (not yet released)
 
-  Nothing yet.
+  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)
 

spot/twaalgos/totgba.cc

@@ -75,7 +75,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)
@@ -84,7 +85,11 @@ namespace spot
               m |= pos[-1].mark;
               pos -= 2;
             }
+          if (inor)
             res.emplace_back(m);
+          else
+            for (unsigned i: m.sets())
+              res.emplace_back(acc_cond::mark_t({i}));
         }
       return res;
     }

tests/core/remfin.test

@@ -270,6 +270,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)'
@@ -844,6 +867,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
@@ -1410,6 +1464,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