monitor: fix -MD/-M difference in property output

Fixes #241.

* spot/twaalgos/postproc.cc: Use the deterministic monitor if it
has as many states as the non-deterministic one.
* spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
for terminal automata.
* spot/twaalgos/stripacc.cc: Set the weak property.
* spot/twaalgos/stripacc.hh: Improve documentation.
* tests/core/monitor.test, tests/core/sbacc.test: Update.
* NEWS: Mention the issue.

NEWS

@@ -30,6 +30,11 @@ New in spot 2.3.1.dev (not yet released)
 
   - 'ltl2tgba --any -C -M ...' would not complete automata.
 
+  - while not incorrect, the HOA properties output by 'ltl2tgba -M'
+    could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D'
+    would always report 'weak' automata.  Both variants now report the
+    most precise between 'weak' or 'terminal'.
+
   Deprecation notices:
 
   - Using --format=%a to print the number of atomic propositions in

spot/twaalgos/minimize.cc

@@ -490,6 +490,13 @@ namespace spot
     res->prop_deterministic(true);
     res->prop_weak(true);
     res->prop_state_acc(true);
+    // Quickly check if this is a terminal automaton
+    for (auto& e: res->edges())
+      if (e.src == e.dst && e.cond == bddtrue)
+        {
+          res->prop_terminal(true);
+          break;
+        }
     return res;
   }
 

spot/twaalgos/postproc.cc

@@ -234,10 +234,11 @@ namespace spot
 
             // For Small,High we return the smallest between the output of
             // the simulation, and that of the deterministic minimization.
+            // Prefer the deterministic automaton in case of equality.
             if (PREF_ == Small && level_ == High && simul_)
               {
                 auto m = minimize_monitor(a);
-                if (m->num_states() < a->num_states())
+                if (m->num_states() <= a->num_states())
                   a = m;
               }
             a->remove_unused_ap();

spot/twaalgos/stripacc.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2014, 2015, 2017 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -30,5 +30,6 @@ namespace spot
         t.acc = 0U;
     a->set_generalized_buchi(0);
     a->release_named_properties();
+    a->prop_weak(true);
   }
 }

spot/twaalgos/stripacc.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012-2014, 2017 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -26,7 +26,9 @@ namespace spot
   /// \ingroup twa_misc
   /// \brief Remove all acceptance sets from a twa_graph.
   ///
-  /// This is equivalent to marking all states/transitions as accepting.
+  /// This will also set the acceptance condition to true, and mark
+  /// the automaton as weak.  Doing so obviously makes all recognized
+  /// infinite runs accepting.
   SPOT_API void
   strip_acceptance_here(twa_graph_ptr a);
 }

tests/core/monitor.test

@@ -44,7 +44,7 @@ digraph G {
 }
 EOF
 
-expect ltl2tgba --monitor a GFa --hoa<<EOF
+expect ltl2tgba --monitor a GFa Ga --hoa<<EOF
 HOA: v1
 name: "a"
 States: 2
@@ -68,11 +68,24 @@ AP: 0
 acc-name: all
 Acceptance: 0 t
 properties: trans-labels explicit-labels state-acc complete
-properties: deterministic stutter-invariant
+properties: deterministic stutter-invariant terminal
 --BODY--
 State: 0
 [t] 0
 --END--
+HOA: v1
+name: "Ga"
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant weak
+--BODY--
+State: 0
+[0] 0
+--END--
 EOF
 
 # Completing a monitor can produce a Büchi automaton.
@@ -85,7 +98,7 @@ AP: 1 "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
-properties: deterministic stutter-invariant inherently-weak
+properties: deterministic stutter-invariant weak
 --BODY--
 State: 0 {0}
 [0] 0

tests/core/sbacc.test

@@ -141,7 +141,7 @@ Start: 0
 AP: 1 "a"
 acc-name: all
 Acceptance: 0 t
-properties: trans-labels explicit-labels state-acc deterministic
+properties: trans-labels explicit-labels state-acc deterministic weak
 --BODY--
 State: 0
 [0] 1