rename is_guarantee_automaton() as is_terminal_automaton()

* src/twaalgos/safety.hh, src/twaalgos/safety.cc: Here.
* src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
wrap/python/ajax/spotcgi.in: Adjust.
* NEWS: Mention the change.

NEWS

@@ -33,6 +33,9 @@ New in spot 1.99.5a (not yet released)
     automata already tagged as "deterministic", and "inherently-weak"
     or "weak" even for automata tagged "weak" or "terminal".
 
+  * Renamings:
+    is_guarantee_automaton() -> is_terminal_automaton()
+
   Python:
   * Add bindings for is_unambiguous().
 

src/bin/ltlfilt.cc

@@ -589,7 +589,7 @@ namespace
 	    }
 	  else
 	    {
-	      matched &= !guarantee || is_guarantee_automaton(min);
+	      matched &= !guarantee || is_terminal_automaton(min);
 	      matched &= !safety || is_safety_mwdba(min);
 	    }
 	}

src/tests/ikwiad.cc

@@ -1432,7 +1432,7 @@ checked_main(int argc, char** argv)
 		}
 	      else
 		{
-		  bool g = is_guarantee_automaton(ensure_digraph(a));
+		  bool g = is_terminal_automaton(ensure_digraph(a));
 		  bool s = is_safety_mwdba(ensure_digraph(a));
 		  if (g && !s)
 		    {

src/twaalgos/minimize.cc

@@ -590,7 +590,7 @@ namespace spot
     // the case where the input is terminal.  See issue #120.
     // (2) It would be nice to have a more precise detection of
     // terminal automata in the output.  Calling
-    // is_guarantee_automaton() seems overkill here.  But maybe we can
+    // is_terminal_automaton() seems overkill here.  But maybe we can
     // add a quick check inside minimize_dfa.
     if (a->prop_terminal())
       res->prop_terminal(true);
@@ -625,7 +625,7 @@ namespace spot
 
     // If aut_f is a guarantee automaton, the WDBA minimization must be
     // correct.
-    if (is_guarantee_automaton(aut_f))
+    if (is_terminal_automaton(aut_f))
       return min_aut_f;
 
     // Build negation automaton if not supplied.
@@ -654,10 +654,8 @@ namespace spot
 
     // If the negation is a guarantee automaton, then the
     // minimization is correct.
-    if (is_guarantee_automaton(aut_neg_f))
+    if (is_terminal_automaton(aut_neg_f))
-      {
+      return min_aut_f;
-	return min_aut_f;
-      }
 
     bool ok = false;
 

src/twaalgos/safety.cc

@@ -24,8 +24,7 @@
 namespace spot
 {
   bool
-  is_guarantee_automaton(const const_twa_graph_ptr& aut,
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
-			 scc_info* si)
   {
     if (aut->prop_terminal())
       return true;

src/twaalgos/safety.hh

@@ -23,30 +23,18 @@
 
 namespace spot
 {
-  /// \brief Whether an automaton represents a guarantee property.
+  /// \brief Whether an automaton is terminal.
   ///
-  /// A weak deterministic TGBA represents a guarantee property if any
+  /// An automaton is terminal if any accepting path ends on an
-  /// accepting path ends on an accepting state with only one
+  /// accepting state with only one transition that is a self-loop
-  /// transition that is a self-loop labelled by true.
+  /// labelled by true.
-  ///
-  /// Note that in the general case, this is only a sufficient
-  /// condition : some guarantee automata might not be recognized with
-  /// this check e.g. because of some non-determinism in the
-  /// automaton.  In that case, you should interpret a \c false return
-  /// value as "I don't know".
-  ///
-  /// If you apply this function on a weak deterministic TGBA
-  /// (e.g. after a successful minimization with
-  /// minimize_obligation()), then the result leaves no doubt: false
-  /// really means that the automaton is not a guarantee property.
   ///
   /// \param aut the automaton to check
   ///
   /// \param sm an scc_info object for the automaton if available (it
   /// will be built otherwise).
   SPOT_API bool
-  is_guarantee_automaton(const const_twa_graph_ptr& aut,
+  is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
-			 scc_info* sm = nullptr);
 
   /// \brief Whether a minimized WDBA represents a safety property.
   ///

wrap/python/ajax/spotcgi.in

@@ -516,7 +516,7 @@ if output_type == 'f':
             automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
             minimized = spot.minimize_obligation(automaton, f)
             if minimized != automaton:
-                g = spot.is_guarantee_automaton(minimized)
+                g = spot.is_terminal_automaton(minimized)
                 s = spot.is_safety_mwdba(minimized)
                 if s and not f.is_syntactic_safety():
                     unbufprint('<li>pathologic safety</li>')