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,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:

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=                                                                   |
+| flag name           | meaning when =true=                                                                          |
-|---------------------+---------------------------------------------------------------------------------------|
+|---------------------+----------------------------------------------------------------------------------------------|
-| =state_acc=         | automaton should be considered has having state-based acceptance                      |
+| =state_acc=         | automaton should be considered has having state-based acceptance                             |
-| =inherently_weak=   | accepting and rejecting cycles cannot be mixed in the same SCC                        |
+| =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                          |
+| =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     |
+| =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       |
+| =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) |
+| =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]]                         |
+| =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

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
+    /// An automaton is terminal if it is weak, its accepting strongly
-    /// can be reached from an accepting cycle, and the accepting
+    /// components are complete, and no accepting edge lead to a
-    /// strongly components are complete (i.e., any suffix is accepted
+    /// non-accepting SCC.
-    /// as soon as we enter an accepting component).
+    ///
+    /// 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()

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;

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
+  /// An automaton is terminal if it is weak, all its accepting SCCs
-  /// are complete.
+  /// 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
   ///

tests/core/strength.test

@@ -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