From 4b5606e742d97a7c8fae9acbd3f81c28016fd325 Mon Sep 17 00:00:00 2001
From: Thomas Medioni <tmedioni@lrde.epita.fr>
Date: Wed, 16 Aug 2017 17:06:09 +0200
Subject: [PATCH] =?UTF-8?q?to=5Fweak=5Falternating():=20fixes=20a=20bug=20?=
 =?UTF-8?q?on=20generalized=20co-B=C3=BCchi=20automata?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #278. Also adds a test ensuring non-regression.

* spot/twaalgos/toweak.cc: Fixes the bug.
* tests/python/toweak.py: Add a test case.
---
 spot/twaalgos/toweak.cc |  5 +++--
 tests/python/toweak.py  | 48 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc
index c368cf939..bca717cbb 100644
--- a/spot/twaalgos/toweak.cc
+++ b/spot/twaalgos/toweak.cc
@@ -121,10 +121,11 @@ namespace spot
                   int curr = static_cast<int>(rank);
                   // We must always be able to go to the previous even rank
                   int lower = less_ ? ((curr - 1) & ~1) : 0;
-                  for (int i = curr; i >= lower; --i)
+                  for (int i = curr, start_set = st.mark.min_set() - 1;
+                       i >= lower; --i, start_set = 0)
                     {
                       if (i % 2)
-                        for (unsigned m = 0; m < numsets_; ++m)
+                        for (unsigned m = start_set; m < numsets_; ++m)
                           levels |= state_to_var_[new_state(d, i, {m})];
                       else
                         levels |= state_to_var_[new_state(d, i, 0U)];
diff --git a/tests/python/toweak.py b/tests/python/toweak.py
index 120d23e00..c1b3ade93 100644
--- a/tests/python/toweak.py
+++ b/tests/python/toweak.py
@@ -53,3 +53,51 @@ def test_phi(phi):
 
 for p in phi1:
   test_phi(p)
+
+
+phi2 = spot.formula("(G((F a) U b)) W a")
+a2 = spot.automaton("""
+HOA: v1
+States: 7
+Start: 1
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc complete univ-branch
+--BODY--
+State: 0
+[t] 0 {0 1}
+State: 1
+[0] 0 {0 1}
+[1] 1&2 {0 1}
+[0&!1] 1&3 {0 1}
+[!0&!1] 1&4 {0 1}
+State: 2
+[1] 2 {0 1}
+[0&!1] 3 {0 1}
+[!0&!1] 4 {0 1}
+State: 3
+[1] 2 {0 1}
+[0&!1] 3 {1}
+[!0&!1] 4 {1}
+State: 4
+[0&1] 2 {0 1}
+[0&!1] 3 {1}
+[!0&!1] 4 {1}
+[!0&1] 5 {0 1}
+State: 5
+[0&1] 2 {0 1}
+[0&!1] 3 {0 1}
+[!0&1] 5 {0}
+[!0&!1] 6 {0}
+State: 6
+[0&1] 2 {0 1}
+[0&!1] 3 {1}
+[!0&1] 5 {0}
+[!0&!1] 6
+--END--
+""")
+a2 = spot.to_weak_alternating(a2)
+assert equivalent(a2, phi2)
+
+