From 01edf4f8e12890045981e86d1f5075285c9e2cb4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 20 Mar 2019 22:02:02 +0100
Subject: [PATCH] minimize_obligation: complement very weak automata if needed
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #379.

* spot/twaalgos/minimize.cc: Here.
* tests/core/optba.test: Add test case provided by Rüdiger Ehlers.
* NEWS: Mention the improvement.
---
 NEWS                      |  5 +++++
 spot/twaalgos/minimize.cc | 19 +++++++++++++++----
 tests/core/optba.test     | 13 ++++++++++++-
 3 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 73f9b9cb9..39d078500 100644
--- a/NEWS
+++ b/NEWS
@@ -24,6 +24,11 @@ New in spot 2.7.2.dev (not yet released)
     acc_cond::acc_code::top_conjuncts() can be used to split an
     acceptance condition on the top-level & or |.
 
+  - minimize_obligation() learned to work on very weak automata even
+    if the formula or negated automaton are not supplied.  (This
+    allows "autfilt [-D] --small" to minimize very-weak automata
+    whenever they are found to represent obligation properties.)
+
   Bugs fixed:
 
   - When processing CSV files with MSDOS-style \r\n line endings,
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 42aed0b12..c024d204b 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2010-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -45,6 +45,7 @@
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/alternation.hh>
 #include <spot/tl/hierarchy.hh>
 
 namespace spot
@@ -570,8 +571,12 @@ namespace spot
         ("minimize_obligation() does not support alternation");
 
     // FIXME: We should build scc_info once, pass it to minimize_wdba
-    // and reuse it for is_terminal_automaton(), and
-    // is_weak_automaton().
+    // and reuse it for is_terminal_automaton(),
+    // is_weak_automaton(), and is_very_weak_automaton().
+    // FIXME: we should postpone the call to minimize_wdba() until
+    // we know for sure that we can verify (or that we do not need
+    // to verify) its output, rather than computing in cases where
+    // we may discard it.
     auto min_aut_f = minimize_wdba(aut_f);
 
     if (reject_bigger)
@@ -614,9 +619,15 @@ namespace spot
             // Remove useless SCCs.
             aut_neg_f = scc_filter(aut_neg_f, true);
           }
+        else if (is_very_weak_automaton(aut_f))
+          {
+            // Very weak automata are easy to complement.
+            aut_neg_f = remove_alternation(dualize(aut_f));
+          }
         else
           {
-            // Otherwise, we cannot check if the minimization is safe.
+            // Otherwise, we don't try to complement the automaton and
+            // therefore we cannot check if the minimization is safe.
             return nullptr;
           }
       }
diff --git a/tests/core/optba.test b/tests/core/optba.test
index 65ce06824..52b52e725 100755
--- a/tests/core/optba.test
+++ b/tests/core/optba.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017, 2019 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -160,3 +160,14 @@ test `autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18
 
 # But we should have 19 with Büchi acceptance, not 20.
 test `autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19
+
+
+# This should be reduced to a 3-state minimal WDBA if we
+# correctly recognize that this is an obligation.  Issue #379.
+cat >in <<EOF
+HOA: v1 Start: 0 States: 4 Acceptance: 1 Inf(0)
+AP: 2 "v0" "v1" --BODY-- State: 0 "T3_init" [t] 0 [!0 & !1] 1
+State: 1 "T2" [0&1] 1 [0&1] 2 [!0&!1] 2 [0&1] 3 [!0&!1] 1
+State: 2 "T1" {0} [0&1] 2 State: 3 "all" {0} [t] 3 --END--
+EOF
+test '3,6' = `autfilt --small in --stats=%s,%e`