Commit 341eeb2b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent f868e0ce
......@@ -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:
......
......@@ -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
......
......@@ -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()
......
......@@ -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;
......
......@@ -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
///
......
......@@ -589,3 +589,99 @@ EOF
diff out expected
autfilt -q expected
cat >input <<EOF
/* This Büchi automaton is not terminal, because of the
accepting edge between states 0 and 1. */
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 1 Inf(0)
--BODY--
State: 0
[t] 0
State: 1
[0] 0 {0}
[!0] 1
--END--
/* This co-Büchi automaton not terminal for the same reason. */
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[t] 0
State: 1
[0] 0 {0}
[!0] 1
--END--
/* This co-Büchi automaton is terminal. */
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[t] 0
State: 1
[0] 0 {0}
[!0] 1 {0}
--END--
EOF
autfilt --check=strength input >output
cat >expected <<EOF
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic weak
--BODY--
State: 0
[t] 0
State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic weak
--BODY--
State: 0
[t] 0
State: 1
[0] 0 {0}
[!0] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
--BODY--
State: 0
[t] 0
State: 1 {0}
[0] 0
[!0] 1
--END--
EOF
diff output expected
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment