From f02ca87f07dcadbd2fa6c8854d4810647403ecfd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 19 Apr 2017 18:46:35 +0200
Subject: [PATCH] sbacc: fix a serious bug

Reported by Thibaud Michaud

* spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty
mark, as it might be accepting.
* tests/core/sbacc.test: Add test cases.
* NEWS: Mention the bug.
---
 NEWS                   |  5 +++-
 spot/twaalgos/sbacc.cc | 17 ++++++++++-
 tests/core/sbacc.test  | 65 ++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index ea74dac0e..51839d344 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,9 @@
 New in spot 2.3.3.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - the transformation to state-based acceptance (spot::sbacc()) was
+    incorrect on automata where the empty acceptance mark is accepting.
 
 New in spot 2.3.3 (2017-04-11)
 
diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc
index 93acc554c..89df387be 100644
--- a/spot/twaalgos/sbacc.cc
+++ b/spot/twaalgos/sbacc.cc
@@ -22,6 +22,7 @@
 #include <utility>
 #include <spot/twaalgos/sbacc.hh>
 #include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/stripacc.hh>
 
 namespace spot
 {
@@ -33,6 +34,18 @@ namespace spot
       throw std::runtime_error
         ("sbacc() does not support alternation");
 
+    // We will need a mark that is rejecting to mark rejecting states.
+    // If no such mark exist, our work is actually quite simple: we
+    // just have to copy the automaton and give it "t" as acceptance
+    // condition.
+    auto unsat_mark = old->acc().unsat_mark();
+    if (!unsat_mark.first)
+      {
+        auto res = make_twa_graph(old, twa::prop_set::all());
+        strip_acceptance_here(res);
+        return res;
+      }
+
     scc_info si(old);
 
     unsigned ns = old->num_states();
@@ -97,7 +110,7 @@ namespace spot
           {
             unsigned scc_dst = si.scc_of(t.dst);
             acc_cond::mark_t acc = 0U;
-            bool dst_acc = si.is_accepting_scc(scc_dst);
+            bool dst_acc = !si.is_rejecting_scc(scc_dst);
             if (maybe_accepting && scc_src == scc_dst)
               acc = t.acc - common_out[t.src];
             else if (dst_acc)
@@ -106,6 +119,8 @@ namespace spot
               acc = one_in[t.dst];
             if (dst_acc)
               acc |= common_out[t.dst];
+            else
+              acc = unsat_mark.second;
             res->new_edge(one.second, new_state(t.dst, acc),
                           t.cond, one.first.second);
           }
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index 8c080d538..ca960a9ae 100755
--- a/tests/core/sbacc.test
+++ b/tests/core/sbacc.test
@@ -159,3 +159,68 @@ randltl --weak-fairness -n 20 2 |
              "$ltl2tgba -H %f | $autfilt -H >%O"
 
 test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`
+
+
+# Test case from Thibaud Michaud.  This used to fail, because sbacc()
+# would remove acceptance marks from all rejecting SCCS...
+cat >tm.hoa <<EOF
+HOA: v1
+States: 5
+Start: 1
+AP: 4 "req" "go" "ack" "cancel"
+acc-name: parity max odd 3
+Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))
+properties: trans-labels explicit-labels trans-acc colored complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 1 {0}
+State: 1
+[!0] 0 {0}
+[0] 2 {0}
+State: 2
+[2] 1 {0}
+[!2] 3 {0}
+State: 3
+[t] 4 {0}
+State: 4
+[2] 1 {2}
+[!2] 3 {1}
+--END--
+EOF
+autfilt --sbacc tm.hoa > out.hoa
+autfilt -q --equivalent-to out.hoa tm.hoa
+
+# Tautological acceptances are converted to "t"
+cat >taut.hoa <<EOF
+HOA: v1
+States: 2
+Start: 1
+AP: 0
+Acceptance: 2 Fin(0) | Inf(0) | Fin(1)
+--BODY--
+State: 0
+[t] 1 {0}
+State: 1
+[t] 0
+[t] 1 {1}
+--END--
+EOF
+cat >expect.hoa <<EOF
+HOA: v1
+States: 2
+Start: 1
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete weak
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 0
+[t] 1
+--END--
+EOF
+autfilt --sbacc taut.hoa > out.hoa
+diff out.hoa expect.hoa