remfin: fix tra_to_tba

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

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

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)
             {

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
+: