From ff2a96cc1a12e05c9cf0973638b3032a7ceaf46d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 23 Jan 2018 17:24:10 +0100
Subject: [PATCH] fix a bug in streett_to_generalized_buchi

Fixes #320.

* spot/twaalgos/totgba.cc: Fix the bug.
* NEWS: Mention the problem.
* tests/core/streett.test: Add test case.
---
 NEWS                    |  6 +++++-
 spot/twaalgos/totgba.cc | 14 +++++++++++---
 tests/core/streett.test | 24 +++++++++++++++++++++++-
 3 files changed, 39 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 96ddbf35b..7aa56435e 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,10 @@
 New in spot 2.5.0.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - streett_to_generalized_buchi() could produce incorrect result on
+    Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1)
+    where some Fin(x) is used both with and without a paired Fin(y).
 
 New in spot 2.5 (2018-01-20)
 
diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc
index 8fecbf043..d3e89977b 100644
--- a/spot/twaalgos/totgba.cc
+++ b/spot/twaalgos/totgba.cc
@@ -551,6 +551,7 @@ namespace spot
     // At some point we will remove anything that is not used as Inf.
     acc_cond::mark_t to_strip = in->acc().all_sets() - inf;
     acc_cond::mark_t inf_alone = 0U;
+    acc_cond::mark_t fin_alone = 0U;
 
     if (!p)
       return remove_fin(in);
@@ -569,7 +570,14 @@ namespace spot
         if (pair.inf)
           for (unsigned mark: pair.inf.sets())
             inf_to_finpairs[mark] |= pair.fin;
+        else
+          fin_alone |= pair.fin;
       }
+    // If we have something like (Fin(0)|Inf(1))&Fin(0), then 0 is in
+    // fin_alone, but we also have fin_to_infpair[0] = {1}.  This should
+    // really be simplified to Fin(0).
+    for (auto mark: fin_alone.sets())
+      fin_to_infpairs[mark] = 0U;
 
     scc_info si(in, scc_info_options::NONE);
 
@@ -583,10 +591,10 @@ namespace spot
         auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9}
         auto acc_fin = acc & fin;     // {0,  2,  4,6}
         auto acc_inf = acc & inf;     // {  1,  3,    7,9}
-        acc_cond::mark_t fin_wo_inf = 0U;
         // Fin sets that are alone either because the acceptance
-        // condition has not matching Inf, or because the SCC the not
-        // intersect the matching inf.
+        // condition has no matching Inf, or because the SCC does not
+        // intersect the matching Inf.
+        acc_cond::mark_t fin_wo_inf = 0U;
         for (unsigned mark: acc_fin.sets())
           if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf))
             fin_wo_inf.set(mark);
diff --git a/tests/core/streett.test b/tests/core/streett.test
index 908d4c6be..7793fe813 100755
--- a/tests/core/streett.test
+++ b/tests/core/streett.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -113,3 +113,25 @@ EOF
 run 0 autcross --language-preserved \
     'autfilt --tgba %H | tee out.hoa >%O' -F streett.hoa
 grep 'generalized-Buchi 2' out.hoa
+
+
+# Issue #320
+autfilt -q --reject-word='cycle{!a;a;a;!a}' <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Streett 3
+Acceptance: 6 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5))
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[!0] 0 {1 3}
+[0] 1 {}
+State: 1
+[0] 2 {2}
+State: 2
+[!0] 0 {0 4}
+[0] 2 {}
+--END--
+EOF