From a18327d4881fa8f152ca54fd3387da798bfdf884 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 31 Mar 2015 19:18:41 +0200
Subject: [PATCH] stutter: improve closure

if a transition with the same label already exist, reuse it

* src/tgbaalgos/stutter.cc: Here.
* src/tgbatest/stutter.test: Add a test case.
---
 src/tgbaalgos/stutter.cc  | 16 +++++++++++++++-
 src/tgbatest/stutter.test | 33 +++++++++++++++++++++++++++++----
 2 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc
index 634938711..a9c5c4bd2 100644
--- a/src/tgbaalgos/stutter.cc
+++ b/src/tgbaalgos/stutter.cc
@@ -487,13 +487,27 @@ namespace spot
                           {
                             if (!bdd_implies(cond, ts.cond))
                               {
-                                ts.cond = ts.cond | cond;
+                                ts.cond |= cond;
                                 if (std::find(todo.begin(), todo.end(), t)
                                     == todo.end())
                                   todo.push_back(t);
                               }
                             need_new_trans = false;
+			    break;
                           }
+			else if (cond == ts.cond)
+			  {
+			    acc |= ts.acc;
+			    if (ts.acc != acc)
+			      {
+				ts.acc = acc;
+				if (std::find(todo.begin(), todo.end(), t)
+				    == todo.end())
+				  todo.push_back(t);
+			      }
+                            need_new_trans = false;
+			    break;
+			  }
                       }
                     if (need_new_trans)
                       {
diff --git a/src/tgbatest/stutter.test b/src/tgbatest/stutter.test
index ed0aac383..f91caa53a 100755
--- a/src/tgbatest/stutter.test
+++ b/src/tgbatest/stutter.test
@@ -42,7 +42,32 @@ $autfilt --states=12 prod.hoa -q
 #
 # We just run those without checking the output, it is enough to
 # trigger assertions in the HOA output routines.
-run 0 ../../bin/ltl2tgba -H 'X(a U b)' > det.hoa
-run 0 ../../bin/autfilt --destut det.hoa -H
-run 0 ../../bin/autfilt --instut=1 det.hoa -H
-run 0 ../../bin/autfilt --instut=2 det.hoa -H
+run 0 $ltl2tgba -H 'X(a U b)' > det.hoa
+run 0 $autfilt --destut det.hoa -H
+run 0 $autfilt --instut=1 det.hoa -H
+run 0 $autfilt --instut=2 det.hoa -H
+
+$ltl2tgba -H 'a & Fb' | $autfilt --destut -H > output
+
+cat >expected <<EOF
+HOA: v1
+name: "a & Fb"
+States: 3
+Start: 2
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[t] 0 {0}
+State: 1
+[1] 0 {0}
+[!1] 1
+State: 2
+[0&1] 0 {0}
+[0&!1] 1
+--END--
+EOF
+
+diff output expected