From 0621e0e9c57748f39e6c6ae63635b63e75ea4001 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 3 Mar 2017 18:23:57 +0100
Subject: [PATCH] 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                      |  5 +++++
 spot/twaalgos/minimize.cc |  7 +++++++
 spot/twaalgos/postproc.cc |  3 ++-
 spot/twaalgos/stripacc.cc |  3 ++-
 spot/twaalgos/stripacc.hh |  6 ++++--
 tests/core/monitor.test   | 19 ++++++++++++++++---
 tests/core/sbacc.test     |  2 +-
 7 files changed, 37 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 79559b92f..b68c93c4a 100644
--- a/NEWS
+++ b/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
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 4a199fbd5..355f13fc3 100644
--- a/spot/twaalgos/minimize.cc
+++ b/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;
   }
 
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index 5b3f2ca29..367757e33 100644
--- a/spot/twaalgos/postproc.cc
+++ b/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();
diff --git a/spot/twaalgos/stripacc.cc b/spot/twaalgos/stripacc.cc
index 5010f1711..a4018035a 100644
--- a/spot/twaalgos/stripacc.cc
+++ b/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);
   }
 }
diff --git a/spot/twaalgos/stripacc.hh b/spot/twaalgos/stripacc.hh
index b94d5558c..df673d7ff 100644
--- a/spot/twaalgos/stripacc.hh
+++ b/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);
 }
diff --git a/tests/core/monitor.test b/tests/core/monitor.test
index d21fb3c9d..e2a251b1f 100755
--- a/tests/core/monitor.test
+++ b/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
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index fedc228bd..8c080d538 100755
--- a/tests/core/sbacc.test
+++ b/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