From 2dda2c9122ed15d0212050ef4484c161c1930f97 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 18 Aug 2013 00:58:01 +0200
Subject: [PATCH] minimize_obligation: can complement the input TGBA if
 deterministic

This makes dstar2tgba able to produce a minimal WDBA when the input DRA
represent an obligation property.

* src/tgbaalgos/minimize.cc (minimize_obligation): When the
formula is not supplied but the input automaton is deterministic,
complement it to check the result of WDBA minimization.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
tests.
---
 src/tgbaalgos/minimize.cc    | 44 ++++++++++++++++++++++--------------
 src/tgbatest/ltl2dstar.test  | 25 ++------------------
 src/tgbatest/ltl2dstar2.test | 25 +++++++++++++++++++-
 3 files changed, 53 insertions(+), 41 deletions(-)

diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index 5bd4c76cb..babecda2a 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -46,6 +46,8 @@
 #include "tgbaalgos/scc.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/bfssteps.hh"
+#include "tgbaalgos/isdet.hh"
+#include "tgbaalgos/dbacomp.hh"
 #include "priv/countstates.hh"
 
 namespace spot
@@ -647,29 +649,37 @@ namespace spot
     if (is_guarantee_automaton(aut_f))
       return min_aut_f;
 
-    if (!f && !aut_neg_f)
-      {
-	// We do not now if the minimization is safe.
-	delete min_aut_f;
-	return 0;
-      }
-
     const tgba* to_free = 0;
 
     // Build negation automaton if not supplied.
     if (!aut_neg_f)
       {
-	assert(f);
+	if (f)
+	  {
+	    // If we know the formula, simply build the automaton for
+	    // its negation.
+	    const ltl::formula* neg_f =
+	      ltl::unop::instance(ltl::unop::Not, f->clone());
+	    aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
+	    neg_f->destroy();
 
-	const ltl::formula* neg_f =
-	  ltl::unop::instance(ltl::unop::Not, f->clone());
-	aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
-	neg_f->destroy();
-
-	// Remove useless SCCs.
-	const tgba* tmp = scc_filter(aut_neg_f, true);
-	delete aut_neg_f;
-	to_free = aut_neg_f = tmp;
+	    // Remove useless SCCs.
+	    const tgba* tmp = scc_filter(aut_neg_f, true);
+	    delete aut_neg_f;
+	    to_free = aut_neg_f = tmp;
+	  }
+	else if (is_deterministic(aut_f))
+	  {
+	    // If the automaton is deterministic, complementing is
+	    // easy.
+	    to_free = aut_neg_f = dba_complement(aut_f);
+	  }
+	else
+	  {
+	    // Otherwise, we cannot check if the minimization is safe.
+	    delete min_aut_f;
+	    return 0;
+	  }
       }
 
     // If the negation is a guarantee automaton, then the
diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test
index 1419dd8d2..3e8bb93e7 100755
--- a/src/tgbatest/ltl2dstar.test
+++ b/src/tgbatest/ltl2dstar.test
@@ -37,31 +37,10 @@ dstar2tgba=../../bin/dstar2tgba
 
 $ltlfilt -f 'a U b' -l |
 ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
-../ltl2tgba -XDB - |
+$dstar2tgba --stats '%s %e %t %a %d' |
 tee out
 
-cat >expected <<EOF
-digraph G {
-  0 [label="", style=invis, height=0]
-  0 -> 1
-  1 [label="1"]
-  1 -> 1 [label="a & !b\n"]
-  1 -> 2 [label="a & !b\n"]
-  1 -> 3 [label="b\n"]
-  1 -> 4 [label="b\n"]
-  2 [label="2"]
-  2 -> 2 [label="a & !b\n"]
-  2 -> 4 [label="b\n"]
-  3 [label="5"]
-  3 -> 3 [label="1\n"]
-  3 -> 4 [label="1\n"]
-  4 [label="6", peripheries=2]
-  4 -> 4 [label="1\n{Acc[1]}"]
-}
-EOF
-
-
-diff expected out
+test "`cat out`" = '2 3 7 1 1'
 
 RAB=--automata=rabin
 STR=--automata=streett
diff --git a/src/tgbatest/ltl2dstar2.test b/src/tgbatest/ltl2dstar2.test
index 452655f04..620aad739 100755
--- a/src/tgbatest/ltl2dstar2.test
+++ b/src/tgbatest/ltl2dstar2.test
@@ -35,7 +35,10 @@ randltl=../../bin/randltl
 
 
 # Make sure all recurrence formulas are translated into deterministic
-# Büchi automata by the DRA->TGBA converster.
+# Büchi automata by the DRA->TGBA converter.
+# (Note that ltl2tgba is not called with -D when want to make
+# sure we get a deterministic output even if the automaton generated
+# by Spot initially was non-deterministic)
 
 $randltl -n -1 a b --tree-size=5..15 |
 $ltlfilt --syntactic-recurrence --remove-wm -r -u \
@@ -56,6 +59,26 @@ while read f; do
   test $det -eq 1;
 done < formulas
 
+echo ==========================
+
+# For obligation formulas, the output of dstar2tgba should
+# have the same size as the input when option -D is used.
+$randltl -n -1 a b --tree-size=5..15 |
+$ltlfilt --obligation --size-min=4 --size-max=15 --relabel=abc \
+         --remove-wm -r -u |
+head -n 20 > formulas
+
+while read f; do
+  expected=`$ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
+  $ltlfilt -f "$f" -l |
+  ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - foo
+  echo "$f"
+  output=`$dstar2tgba foo -BD --stats '%s %e %d 1'`
+  # the '1 %d' matching '%d 1' makes sure input and output are deterministic.
+  test "$output" = "$expected";
+done < formulas
+
+echo ==========================
 
 # Now make sure that some obviously non-deterministic property
 # are not translated to deterministic.