From 341eeb2ba1c7a349f427d29f18d76c12f20706cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Nov 2016 16:19:05 +0100 Subject: [PATCH] strength: fix is_terminal() Fix #198. Reported by Maximilien Colange. * spot/twaalgos/strength.cc (is_terminal): Test that no accepting transition lead to a rejecting SCC. * tests/core/strength.test: Add test case. * spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org: Adjust documentation. * NEWS: Mention the fix. --- NEWS | 5 ++ doc/org/concepts.org | 18 ++++---- spot/twa/twa.hh | 10 ++-- spot/twaalgos/strength.cc | 11 +++++ spot/twaalgos/strength.hh | 8 +++- tests/core/strength.test | 96 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 133 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index 340b218a3..04fb9e0eb 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.2.1.dev (Not yet released) * scc_filter() had a left-over print statement that would print "names" when copying the name of the states. + * is_terminal() should reject automata that have accepting + transitions going into rejecting SCCs. The whole point of + being a terminal automaton is that reaching an accepting + transition guarantees that any suffix will be accepted. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 0e7a7f44f..54ad43fe1 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -990,15 +990,15 @@ better choices. There are actually several property flags that are stored into each automaton, and that can be queried or set by algorithms: -| flag name | meaning when =true= | -|---------------------+---------------------------------------------------------------------------------------| -| =state_acc= | automaton should be considered has having state-based acceptance | -| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | -| =weak= | transitions of an SCC all belong to the same acceptance sets | -| =terminal= | automaton is weak, accepting SCCs are complete and may not reach rejecting cycles | -| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | -| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | -| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | +| flag name | meaning when =true= | +|---------------------+----------------------------------------------------------------------------------------------| +| =state_acc= | automaton should be considered has having state-based acceptance | +| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | +| =weak= | transitions of an SCC all belong to the same acceptance sets | +| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | +| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | +| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | +| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | For each flag =flagname=, the =twa= class has a method =prop_flagname()= that returns the value of the flag as an instance of diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 4ec67956e..6afe8aedb 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1179,10 +1179,12 @@ namespace spot /// \brief Whether the automaton is terminal. /// - /// An automaton is terminal if it is weak, no non-accepting cycle - /// can be reached from an accepting cycle, and the accepting - /// strongly components are complete (i.e., any suffix is accepted - /// as soon as we enter an accepting component). + /// An automaton is terminal if it is weak, its accepting strongly + /// components are complete, and no accepting edge lead to a + /// non-accepting SCC. + /// + /// This property ensures that a word can be accepted as soon as + /// on of its prefixes move through an accepting edge. /// /// \see prop_weak() /// \see prop_inherently_weak() diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 1c4fb6524..b547a0ac6 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -79,6 +79,17 @@ namespace spot break; } } + // A terminal automaton should accept any word that as a prefix + // leading to an accepting edge. In other words, we cannot have + // an accepting edge that goes into a rejecting SCC. + if (terminal && is_term) + for (auto& e: aut->edges()) + if (si->is_rejecting_scc(si->scc_of(e.dst)) + && aut->acc().accepting(e.acc)) + { + is_term = false; + break; + } exit: if (need_si) delete si; diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index dd0a426dc..a711d01e5 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -25,8 +25,12 @@ namespace spot { /// \brief Whether an automaton is terminal. /// - /// An automaton is terminal if it is weak, and all accepting SCCs - /// are complete. + /// An automaton is terminal if it is weak, all its accepting SCCs + /// are complete, and no accepting transitions lead to a + /// non-accepting SCC. + /// + /// This property guarantees that a word is accepted if it has some + /// prefix that reaches an accepting transition. /// /// \param aut the automaton to check /// diff --git a/tests/core/strength.test b/tests/core/strength.test index e70622877..46ea1174c 100755 --- a/tests/core/strength.test +++ b/tests/core/strength.test @@ -589,3 +589,99 @@ EOF diff out expected autfilt -q expected + + +cat >input <output + +cat >expected <