From 48ecb903c5829b767db16c98c345d2e0601b91c8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 26 Apr 2019 11:27:11 +0200
Subject: [PATCH] sepsets: fix infinite loop

* tests/core/sepsets.test: New test case.
* spot/twaalgos/sepsets.cc: Fix the code.
* NEWS: Mention the problem.
---
 NEWS                     |  5 +++++
 spot/twaalgos/sepsets.cc | 19 +++++++++----------
 tests/core/sepsets.test  | 22 +++++++++++++++++++++-
 3 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/NEWS b/NEWS
index c518dad05..33a95163c 100644
--- a/NEWS
+++ b/NEWS
@@ -46,6 +46,11 @@ New in spot 2.7.3.dev (not yet released)
     acceptance condition.  The output can be alternating only if the
     input was alternating.
 
+  Bugs fixed:
+
+  - separate_sets_here() (and therefore autfilt --separate-sets) could
+    loop infinitely on some inputs.
+
 New in spot 2.7.3 (2019-04-19)
 
   Bugs fixed:
diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc
index 001e88f36..cce0c935e 100644
--- a/spot/twaalgos/sepsets.cc
+++ b/spot/twaalgos/sepsets.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et
+// Copyright (C) 2015-2019 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -56,7 +56,7 @@ namespace spot
     // Fix the acceptance condition
     auto& code = aut->acc().get_acceptance();
     // If code were empty, then common would have been 0.
-    assert (!code.empty());
+    assert(!code.empty());
     acc_cond::acc_word* pos = &code.back();
     acc_cond::acc_word* start = &code.front();
     while (pos > start)
@@ -69,14 +69,13 @@ namespace spot
             break;
           case acc_cond::acc_op::Fin:
           case acc_cond::acc_op::FinNeg:
-            if (!(pos[-1].mark & common))
-              break;
-            for (auto p: map)
-              if (pos[-1].mark & p.first)
-                {
-                  pos[-1].mark -= p.first;
-                  pos[-1].mark |= p.second;
-                }
+            if (pos[-1].mark & common)
+              for (auto p: map)
+                if (pos[-1].mark & p.first)
+                  {
+                    pos[-1].mark -= p.first;
+                    pos[-1].mark |= p.second;
+                  }
             SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Inf:
           case acc_cond::acc_op::InfNeg:
diff --git a/tests/core/sepsets.test b/tests/core/sepsets.test
index 055544c7a..9957da874 100755
--- a/tests/core/sepsets.test
+++ b/tests/core/sepsets.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et Développement de
+# Copyright (C) 2015, 2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -39,6 +39,16 @@ State: 2
 [!0&1&!2] 1
 [0&!2] 2 {0 1}
 --END--
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "p0" "p1" "p2"
+Acceptance: 3 (Fin(1) | Inf(0)) & (Fin(2) | Inf(1))
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0 1 2}
+[0&!1&!2] 0
+--END--
 EOF
 
 cat >expected <<EOF
@@ -60,6 +70,16 @@ State: 2
 [!0&1&!2] 1
 [0&!2] 2 {0 1 2 3}
 --END--
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "p0" "p1" "p2"
+Acceptance: 4 (Fin(3) | Inf(0)) & (Fin(2) | Inf(1))
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0 1 2 3}
+[0&!1&!2] 0
+--END--
 EOF
 
 run 0 autfilt --separate-sets in -H > out