From c1b7497f840c1ba12278c152c32e9f0988a73cf7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 30 Jun 2018 16:38:56 +0200
Subject: [PATCH] gfguarantee: fix selection of moved init state

Fixes #357.

* spot/twaalgos/gfguarantee.cc: Decide that a moved init state is to
close from the terminal state *before* actually modifying the
automaton.
* tests/core/ltl2tgba2.test: Add a test.
---
 spot/twaalgos/gfguarantee.cc | 22 +++++++++++++++++-----
 tests/core/ltl2tgba2.test    | 10 ++++++++++
 2 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc
index 9d6ab7d98..aa26fb88b 100644
--- a/spot/twaalgos/gfguarantee.cc
+++ b/spot/twaalgos/gfguarantee.cc
@@ -255,11 +255,22 @@ namespace spot
                             moved:
                               continue;
                             }
+
+                          // Make sure no successor of the new initial
+                          // state will reach a terminal state; if
+                          // that is the case, we have to shorten the
+                          // history further.
+                          if (hlen > 0)
+                            for (auto& ei: aut->out(moved_init))
+                              if ((ei.cond & econd) != bddfalse
+                                  && term[si.scc_of(ei.dst)])
+                                goto failed;
+
                           // we have successfully played all history
                           // to a non-terminal state.
                           //
-                          // Combine this edge with any compatible edge from
-                          // the initial state.
+                          // Combine this edge with any compatible
+                          // edge from the initial state.
                           first = true;
                           for (auto& ei: aut->out(moved_init))
                             {
@@ -272,10 +283,11 @@ namespace spot
                                   // the initial state without any
                                   // combination.
                                   bool ts = term[si.scc_of(ei.dst)];
-                                  if (ts && hlen > 0)
-                                    goto failed;
                                   if (ts)
-                                    want_merge_edges = true;
+                                    {
+                                      assert(hlen == 0);
+                                      want_merge_edges = true;
+                                    }
                                   if (first)
                                     {
                                       e.acc = {0};
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index b48c1b448..fcd004f6e 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -378,3 +378,13 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
     ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output
 
 diff formulas output
+
+# Regression test for issue #357.  The second formula used to
+# incorrectly produce 13 edges when translated after the first one
+# because the transition were explored in a different order.
+ltl2tgba -D 'a | Fb' 'GF(d & (!c | XXc))' --stats=%s,%e,%d >out
+cat >expected <<EOF
+3,5,1
+4,12,1
+EOF
+diff out expected