From c36b1588fc97f4535fb6e151f4367c4245b79a4b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 5 Dec 2019 22:27:19 +0100
Subject: [PATCH] remfin: fix tra_to_tba
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes a complementation bug reported by Juraj Major and Tereza
Šťastná.

* spot/twaalgos/remfin.cc (is_scc_tba_type): Fix the condition for
handling Fin-alone pairs.
* tests/core/complement.test: Add Juraj & Tereza's test case.
* NEWS: Mention it.
---
 NEWS                       |  9 +++++++++
 spot/twaalgos/remfin.cc    |  5 +++--
 tests/core/complement.test | 16 ++++++++++++++++
 3 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 432525b7d..7cd025721 100644
--- a/NEWS
+++ b/NEWS
@@ -54,6 +54,15 @@ New in spot 2.8.3.dev  (not yet released)
        parity_min_odd(n) = parity_min(true, n)
        parity_min_even(n) = parity_min(false, n)
 
+  Bugs fixed:
+
+  - The Rabin-to-Büchi conversion could misbehave when applied to
+    Rabin-like acceptance with where some pairs have missing Inf(.)
+    (e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not
+    visit the remaining Inf(.).  This indirectly caused the
+    complementation algorithm to produce incorrect results on such
+    inputs, causing false positives in ltlcross and autcross.
+
 New in spot 2.8.3 (2019-11-06)
 
   Build:
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index 83a0f36b7..18f16a9f3 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -126,7 +126,8 @@ namespace spot
       auto scc_pairs = rs_pairs_view(aut_pairs.pairs(), scc_acc);
       // If there is one aut_fin_alone that is not in the SCC,
       // any cycle in the SCC is accepting.
-      if (scc_pairs.fins_alone().proper_subset(aut_pairs.fins_alone()))
+      auto aut_fin_alone = aut_pairs.fins_alone();
+      if ((scc_acc & aut_fin_alone) != aut_fin_alone)
         {
           for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e)
             {
diff --git a/tests/core/complement.test b/tests/core/complement.test
index 555336d3c..35931f82c 100755
--- a/tests/core/complement.test
+++ b/tests/core/complement.test
@@ -142,3 +142,19 @@ State: 1
 --END--
 EOF
 diff out expected
+
+# The following automaton used to be badly complemented due
+# to a bug in the Rabin-to-BA conversion.
+# Reported by Juraj Major and Tereza Šťastná.
+cat >pos.hoa <<EOF
+HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) |
+(Inf(1) & Fin(2)) properties: trans-labels explicit-labels trans-acc
+--BODY-- State: 0 [0&1&2] 5 {2} State: 1 [0&1&!2] 1 {0} [0&1&2]
+2 [0&!1&!2] 6 State: 2 [!0&1&2] 4 State: 3 [!0&1&2] 2 {0} [0&1&2] 3
+[0&1&2] 1 State: 4 [!0&!1&!2] 7 {2} State: 5 [!0&1&!2] 3 [!0&!1&2]
+5 [!0&!1&!2] 2 {0} State: 6 [!0&1&2] 7 {0 1 2} [!0&!1&!2] 6 State: 7
+[!0&1&2] 4 [0&!1&2] 7 --END--
+EOF
+autfilt --complement pos.hoa >neg.hoa
+autfilt -q --intersect=pos.hoa neg.hoa && exit 1
+: