diff --git a/NEWS b/NEWS
index 46a9855fa..40b56e84d 100644
--- a/NEWS
+++ b/NEWS
@@ -113,6 +113,12 @@ New in spot 2.8.6.dev (not yet released)
- autfilt --uniq was not considering differences in acceptance
conditions or number of states when discarding automata.
+ - In an automaton with acceptance condition containing some Fin, and
+ whose accepting cycle could be reduced to a self-loop in an
+ otherwise larger SCC, the generation of an accepting run could be
+ wrong. This could in turn cause segfaults or infinite loops while
+ running autcross or autfilt --stats=%w.
+
New in spot 2.8.6 (2020-02-19)
Bugs fixed:
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index cf0d7a71a..e3375c7e4 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -558,37 +558,43 @@ namespace spot
};
// The SCC exploration has a small optimization that can flag SCCs
- // has accepting if they contain accepting self-loops, even if the
+ // as accepting if they contain accepting self-loops, even if the
// SCC itself has some Fin acceptance to check. So we have to
// deal with this situation before we look for the more complex
// case of satisfying the condition with a larger cycle. We do
// this first, because it's good to return a small cycle if we
// can.
const acc_cond& acccond = aut_->acc();
- for (unsigned s: node.states())
- for (auto& e: aut_->out(s))
- if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc))
- {
- // We have found an accepting self-loop. That's the cycle
- // part of our accepting run.
- r->cycle.clear();
- r->cycle.emplace_front(aut_->state_from_number(e.src),
- e.cond, e.acc);
- // Add the prefix.
- r->prefix.clear();
- if (e.src != init)
- explicit_bfs_steps(aut_, init, r->prefix,
- [](const twa_graph::edge_storage_t&)
- {
- return false; // Do not filter.
- },
- [&](const twa_graph::edge_storage_t& t)
- {
- return t.dst == e.src;
- });
- return;
- }
-
+ unsigned num_states = aut_->num_states();
+ for (unsigned s = 0; s < num_states; ++s)
+ {
+ // We scan the entire state to find those in the SCC, because
+ // we cannot rely on TRACK_STATES being on.
+ if (scc_of(s) != scc)
+ continue;
+ for (auto& e: aut_->out(s))
+ if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc))
+ {
+ // We have found an accepting self-loop. That's the cycle
+ // part of our accepting run.
+ r->cycle.clear();
+ r->cycle.emplace_front(aut_->state_from_number(e.src),
+ e.cond, e.acc);
+ // Add the prefix.
+ r->prefix.clear();
+ if (e.src != init)
+ explicit_bfs_steps(aut_, init, r->prefix,
+ [](const twa_graph::edge_storage_t&)
+ {
+ return false; // Do not filter.
+ },
+ [&](const twa_graph::edge_storage_t& t)
+ {
+ return t.dst == e.src;
+ });
+ return;
+ }
+ }
// Prefix search
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 7fafd738d..d05a08035 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -314,6 +314,7 @@ TESTS_twa = \
core/autcross2.test \
core/autcross3.test \
core/autcross4.test \
+ core/autcross5.test \
core/complementation.test \
core/randpsl.test \
core/cycles.test \
diff --git a/tests/core/autcross5.test b/tests/core/autcross5.test
new file mode 100755
index 000000000..1dc4a29d5
--- /dev/null
+++ b/tests/core/autcross5.test
@@ -0,0 +1,200 @@
+#!/bin/sh
+# -*- 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 .
+
+. ./defs
+set -e
+
+# Based on a report by Juraj Major.
+
+cat >a7.hoa <_a7.hoa < %O' 2>stderr && exit 2
+cat stderr
+grep 'both automata accept the infinite word:' stderr