From 2feba6ad5edd9c00fd1915d1b508cd27e069293c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 6 Jan 2018 09:13:52 +0100
Subject: [PATCH] simplify_acceptance: fix handling of first edge

Fixes #315.

* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Do not
compare the first edge against previous_a.
* tests/core/accsimpl.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
---
 NEWS                      |  7 +++++++
 spot/twaalgos/cleanacc.cc | 39 +++++++++++++++++++++++++++++----------
 tests/Makefile.am         |  1 +
 tests/core/accsimpl.test  | 30 ++++++++++++++++++++++++++++++
 4 files changed, 67 insertions(+), 10 deletions(-)
 create mode 100755 tests/core/accsimpl.test

diff --git a/NEWS b/NEWS
index e7973d198..a5b7ebd1c 100644
--- a/NEWS
+++ b/NEWS
@@ -256,6 +256,13 @@ New in spot 2.4.4.dev (net yet released)
     been removed.  It's a low-level function was not used anywhere in
     Spot anymore, since it's better to use spot::twa::copy_ap_of().
 
+  Bugs fixed:
+
+  - spot::simplify_acceptance() could produce incorrect output
+    if the first edge of the automaton was the only one with no
+    acceptance set.  In spot 2.4.x this function was only used
+    by autfilt --simplify-acceptance.
+
 New in spot 2.4.4 (2017-12-25)
 
   Bugs fixed:
diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc
index 145ff915a..75d699670 100644
--- a/spot/twaalgos/cleanacc.cc
+++ b/spot/twaalgos/cleanacc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -273,26 +273,45 @@ namespace spot
       if (!used_in_cond)
         return aut;
 
+      // complement[i] holds sets that appear when set #i does not.
       unsigned num_sets = acc.num_sets();
       std::vector<acc_cond::mark_t> complement(num_sets);
 
-
       for (unsigned i = 0; i < num_sets; ++i)
         if (used_in_cond.has(i))
           complement[i] = used_in_cond - acc_cond::mark_t({i});
 
-      acc_cond::mark_t previous_a = 0U;
-      for (auto& t: aut->edges())
+      // Let's visit all edges to update complement[i].  To skip some
+      // duplicated work, prev_acc remember the "acc" sets of the
+      // previous edge, so we can skip consecutive edges with
+      // identical "acc" sets.  Note that there is no value of
+      // prev_acc that would allow us to fail the comparison on the
+      // first edge (this was issue #315), so we have to deal with
+      // that first edge specifically.
+      acc_cond::mark_t prev_acc = 0U;
+      const auto& edges = aut->edges();
+      auto b = edges.begin();
+      auto e = edges.end();
+      auto update = [&](acc_cond::mark_t tacc)
         {
-          if (t.acc == previous_a)
-            continue;
-          previous_a = t.acc;
+          prev_acc = tacc;
           for (unsigned m: used_in_cond.sets())
             {
-              if (t.acc.has(m))
-                complement[m] -= t.acc;
+              if (tacc.has(m))
+                complement[m] -= tacc;
               else
-                complement[m] &= t.acc;
+                complement[m] &= tacc;
+            }
+        };
+      if (b != e)
+        {
+          update(b->acc);
+          ++b;
+          while (b != e)
+            {
+              if (b->acc != prev_acc)
+                update(b->acc);
+              ++b;
             }
         }
       aut->set_acceptance(num_sets,
diff --git a/tests/Makefile.am b/tests/Makefile.am
index f1542ca69..948083f12 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -242,6 +242,7 @@ TESTS_twa = \
   core/explpro4.test \
   core/explsum.test \
   core/dualize.test \
+  core/accsimpl.test \
   core/tripprod.test \
   core/dupexp.test \
   core/exclusive-tgba.test \
diff --git a/tests/core/accsimpl.test b/tests/core/accsimpl.test
new file mode 100755
index 000000000..773dc85af
--- /dev/null
+++ b/tests/core/accsimpl.test
@@ -0,0 +1,30 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+
+set -e
+
+
+# Issue #315
+ltlcross -f FGa \
+  'ltl2tgba -G -D %f | autfilt --complement >%O' \
+  'ltl2tgba -G -D %f | autfilt --complement | autfilt --simplify-acceptance >%O'
-- 
GitLab