run: fix reduce on automata with Fin

Reported by Florian Renkin.

* spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin
acceptance, check the reduced cycle and revert to the original cycle
if necessary.
* tests/python/intrun.py: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/emptiness.hh: Improve documentation.

NEWS

@@ -61,6 +61,11 @@ New in spot 2.9.0.dev (not yet released)
   - Improve ltldo diagnostics to fix spurious test-suite failure on
     systems with antique GNU libc.
 
+  - twa_run::reduce() could reduce accepting runs incorrectly on
+    automata using Fin in their acceptance condition.  This caused
+    issues in intersecting_run(), exclusive_run(),
+    intersecting_word(), exclusive_word(), which all call reduce().
+
 New in spot 2.9 (2020-04-30)
 
   Command-line tools:

spot/twaalgos/emptiness.cc

@@ -304,11 +304,7 @@ namespace spot
       {
         state_set::const_iterator i = seen.begin();
         while (i != seen.end())
-          {
-            const state* ptr = *i;
-            ++i;
-            ptr->destroy();
-          }
+          (*i++)->destroy();
       }
 
       void
@@ -353,17 +349,19 @@ namespace spot
   {
     ensure_non_empty_cycle("twa_run::reduce()");
     auto& a = aut;
+    auto& acc = a->acc();
     auto res = std::make_shared<twa_run>(a);
     state_set ss;
     shortest_path shpath(a);
     shpath.set_target(&ss);
 
     // We want to find a short segment of the original cycle that
-    // contains all acceptance conditions.
+    // satisfies the acceptance condition.
 
     const state* segment_start; // The initial state of the segment.
     const state* segment_next; // The state immediately after the segment.
 
+
     // Start from the end of the original cycle, and rewind until all
     // acceptance sets have been seen.
     acc_cond::mark_t seen_acc = {};
@@ -374,7 +372,7 @@ namespace spot
         --seg;
         seen_acc |= seg->acc;
       }
-    while (!a->acc().accepting(seen_acc));
+    while (!acc.accepting(seen_acc));
     segment_start = seg->s;
 
     // Now go forward and ends the segment as soon as we have seen all
@@ -390,7 +388,7 @@ namespace spot
 
         ++seg;
       }
-    while (!a->acc().accepting(seen_acc));
+    while (!acc.accepting(seen_acc));
     segment_next = seg == cycle.end() ? cycle.front().s : seg->s;
 
     // Close this cycle if needed, that is, compute a cycle going
@@ -402,6 +400,29 @@ namespace spot
         ss.clear();
         assert(s->compare(segment_start) == 0);
         (void)s;
+
+        // If the acceptance condition uses Fin, it's possible (and
+        // even quite likely) that the cycle we have constructed this
+        // way is now rejecting, because the closing steps might add
+        // unwanted colors.  If that is the case, throw the reduced
+        // cycle away and simply preserve the original one verbatim.
+        if (acc.uses_fin_acceptance())
+          {
+            acc_cond::mark_t seen = {};
+            for (auto& st: res->cycle)
+              seen |= st.acc;
+            if (!acc.accepting(seen))
+              {
+                for (auto& st: res->cycle)
+                  st.s->destroy();
+                res->cycle.clear();
+                for (auto& st: cycle)
+                  {
+                    twa_run::step st2 = { st.s->clone(), st.label, st.acc };
+                    res->cycle.emplace_back(st2);
+                  }
+              }
+          }
       }
 
     // Compute the prefix: it's the shortest path from the initial

spot/twaalgos/emptiness.hh

 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de
+// Copyright (C) 2011, 2013-2018, 2020 Laboratoire de
 // Recherche et Developpement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -413,6 +413,12 @@ namespace spot
     ///
     /// Return a run which is still accepting for <code>aut</code>,
     /// but is no longer than this one.
+    ///
+    /// This is done by trying to find a fragment of the accepting
+    /// single that is accepting, and trying to close a cycle around
+    /// this fragment with fewer edges than in the original cycle.
+    /// (This step works best in Fin-less automata.)  And then trying
+    /// to find a shorter prefix leading to any state of the cycle.
     twa_run_ptr reduce() const;
 
     /// \brief Project an accepting run

tests/Makefile.am

@@ -383,6 +383,7 @@ TESTS_python = \
   python/genem.py \
   python/implies.py \
   python/interdep.py \
+  python/intrun.py \
   python/kripke.py \
   python/ltl2tgba.test \
   python/ltlf.py \

tests/python/intrun.py

+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2020 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/>.
+
+import spot
+
+# This issue was reported by Florian Renkin.  The reduce() call used in
+# intersecting_run() was bogus, and could incorrectly reduce a word
+# intersecting the product into a word not intersecting the product if the
+# acceptance condition uses some Fin.
+a, b = spot.automata("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1" acc-name:
+Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties:
+trans-labels explicit-labels trans-acc complete properties: deterministic
+--BODY-- State: 0 [t] 3 State: 1 [t] 4 {1} State: 2 [0] 2 {1} [!0] 1 {0} State:
+3 [t] 1 {1} State: 4 [!0&1] 4 {3} [!0&!1] 3 [0] 2 {0} --END-- HOA: v1 States: 5
+Start: 0 AP: 2 "p0" "p1" Acceptance: 3 Inf(2) | (Fin(0) & Inf(1)) properties:
+trans-labels explicit-labels trans-acc complete properties: deterministic
+--BODY-- State: 0 [t] 3 State: 1 [t] 4 {1 2} State: 2 [0] 2 {1 2} [!0] 1 {0 2}
+State: 3 [t] 1 {1 2} State: 4 [!0&1] 4 {2} [!0&!1] 3 {2} [0] 2 {0 2} --END--""")
+r = b.intersecting_run(spot.complement(a));
+c = spot.twa_word(r).as_automaton()
+assert c.intersects(b)
+assert not c.intersects(a)