"ltl2tgba -Rm" will apply WDBA-minimization only if correct.

* src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
it is correct. Either we can quickly determine that a formula or
its negation is a safety formula, or we can slowly check the
equivalence of the WDBA-minimized automaton and the original
automaton.
* src/tgbatest/wdba.test: New test.
* src/tgbatest/safety.test: Adjust comment.
* src/tgbatest/spotlbtt.test: Use -Rm.
* src/tgbatest/Makefile.am (TESTS): Add wdba.test.

ChangeLog

@@ -1,3 +1,17 @@
+2010-04-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	"ltl2tgba -Rm" will apply WDBA-minimization only if correct.
+
+	* src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
+	it is correct. Either we can quickly determine that a formula or
+	its negation is a safety formula, or we can slowly check the
+	equivalence of the WDBA-minimized automaton and the original
+	automaton.
+	* src/tgbatest/wdba.test: New test.
+	* src/tgbatest/safety.test: Adjust comment.
+	* src/tgbatest/spotlbtt.test: Use -Rm.
+	* src/tgbatest/Makefile.am (TESTS): Add wdba.test.
+
 2010-04-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Better resource handling in minimization.

src/tgbatest/Makefile.am

@@ -93,6 +93,7 @@ TESTS = \
   reductgba.test \
   scc.test \
   safety.test \
+  wdba.test \
   randtgba.test \
   emptchk.test \
   emptchke.test \

src/tgbatest/ltl2tgba.cc

@@ -55,6 +55,7 @@
 #include "tgbaalgos/sccfilter.hh"
 #include "tgbaalgos/safety.hh"
 #include "tgbaalgos/eltl2tgba_lacim.hh"
+#include "tgbaalgos/gtec/gtec.hh"
 #include "eltlparse/public.hh"
 #include "misc/timer.hh"
 
@@ -907,7 +908,66 @@ main(int argc, char** argv)
 
       spot::tgba_explicit* minimized = 0;
       if (opt_minimize)
-        a = minimized = minimize(a);
+	{
+	  tm.start("WDBA-minimization");
+	  minimized = minimize(a);
+	  tm.stop("WDBA-minimization");
+	  tm.start("WDBA-check");
+	  // If A is a safety automaton, the WDBA minimization
+	  // must be correct.
+	  if (is_safety_automaton(a))
+	    {
+	      a = minimized;
+	    }
+	  else // We don't know if A is a safety automaton.
+	    {
+	      // Let's make sure that a recognize the same language
+	      // as minimized.
+	      spot::ltl::formula* neg =
+		spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
+	      spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt,
+						   fm_symb_merge_opt,
+						   post_branching,
+						   fair_loop_approx,
+						   unobservables, fm_red);
+	      neg->destroy();
+	      spot::tgba* nscc = spot::scc_filter(n, true);
+	      // If the negation is a safety automaton,
+	      // then the minimization is correct.
+	      if (is_safety_automaton(n))
+		{
+		  a = minimized;
+		}
+	      else
+		{
+		  spot::tgba* p = new spot::tgba_product(minimized, nscc);
+		  spot::emptiness_check* ec = couvreur99(p);
+		  spot::emptiness_check_result* res = ec->check();
+		  if (!res)
+		    {
+		      delete ec;
+		      delete p;
+		      spot::tgba* nm = minimize(nscc);
+		      p = new spot::tgba_product(a, nm);
+		      ec = couvreur99(p);
+		      res = ec->check();
+		      if (!res)
+			{
+			  // Finally, we are now sure that it was safe
+			  // to minimize the automaton.
+			  a = minimized;
+			}
+		      delete nm;
+		    }
+		  delete res;
+		  delete ec;
+		  delete p;
+		}
+	      delete nscc;
+	      delete n;
+	    }
+	  tm.stop("WDBA-check");
+	}
 
       spot::tgba_reduc* aut_red = 0;
       if (reduc_aut != spot::Reduce_None)

src/tgbatest/safety.test

@@ -61,7 +61,7 @@ Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r
 G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r)
 EOF
 
-# The negation of the first 4 formulae are not safety properties, but they
+# The negation of the first 5 formulae are not safety properties, but they
 # are obligation properties.
 cat >non-safety.txt <<EOF
 Fp

src/tgbatest/spotlbtt.test

@@ -182,6 +182,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), +pre +WDBA"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -r4 -R3 -Rm -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), pre + allpost reduction"

src/tgbatest/wdba.test

@@ -0,0 +1,117 @@
+#!/bin/sh
+# Copyright (C) 2010 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+. ./defs
+
+set +x
+set -e
+
+cat >obligations.txt <<EOF
+G(!p)
+Fr->(!p U r)
+G(q->G(!p))
+G((q&!r&Fr)->(!p U r))
+G(q&!r->((!p U r)|G!p ))
+(!r U (p&!r))|(G!r)
+G(q&!r->((!r U (p&!r))|G!r))
+(!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p
+Fr->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r)))))))))
+Fq->(!q U (q&((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p)))
+G((q&Fr)->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r))))))))))
+G(q->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|((!p U r)|G!p)|Gp)))))))))
+G(p)
+Fr->(p U r)
+G(q->G(p))
+G((p&!r&Fr)->(p U r))
+G(q&!r->((p U r)|Gp))
+Fr->(!p U (s|r))
+G((q&!r&Fr)->(!p U (s|r)))
+G(q&!r->((!p U (s|r))|G!p))
+Fr->(p->(!r U (s&!r))) U r
+G((q&!r&Fr)->(p->(!r U (s&!r))) U r)
+Fp->(!p U (s&!p&X(!p U t)))
+Fr->(!p U (r|(s&!p&X(!p U t))))
+(G!q)|(!q U (q&Fp->(!p U (s&!p&X(!p U t)))))
+G((q&Fr)->(!p U (r|(s&!p&X(!p U t)))))
+G(q->(Fp->(!p U (r|(s&!p&X(!p U t))))))
+(F(s&XFt))->((!s) U p)
+Fr->((!(s&(!r)&X(!r U (t&!r))))U(r|p))
+(G!q)|((!q)U(q&((F(s&XFt))->((!s) U p))))
+G((q&Fr)->((!(s&(!r)&X(!r U (t&!r))))U(r|p)))
+Fr->(p->(!r U (s&!r&X(!r U t)))) U r
+G((q&Fr)->(p->(!r U (s&!r&X(!r U t)))) U r)
+Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r
+G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r)
+Fp
+G(!q)|F(q&Fp)
+(!p U s)|Gp
+G(q->(!(s&(!r)&X(!r U (t&!r)))U(r|p)|G(!(s&XFt))))
+Fr->(s&X(!r U t)->X(!r U (t&Fp))) U r
+EOF
+
+cat >non-obligations.txt <<EOF
+G(q&!r->(!r U (p&!r)))
+G!q|F(q&((!p U s)|G!p))
+G(p->Fs)
+G(q->G(p->Fs))
+G(q&!r->(((p->(!r U (s&!r))) U r)|G(p->(!r U (s&!r)))))
+G(s&XFt->X(F(t&Fp)))
+G(q->G(s&XFt->X(!t U (t&Fp))))
+G((q&Fr)->(s&X(!r U t)->X(!r U (t&Fp))) U r)
+G(q->(s&X(!r U t)->X(!r U (t&Fp)))U(r|G(s&X(!r U t)->X(!r U (t&Fp)))))
+G(p->F(s&XFt))
+G(q->G(p->(s&XFt)))
+G(q->(p->(!r U (s&!r&X(!r U t))))U(r|G(p->(s&XFt))))
+G(p->F(s&!z&X(!z U t)))
+G(q->G(p->(s&!z&X(!z U t))))
+G(q->(p->(!r U (s&!r&!z&X((!r&!z) U t))))U(r|G(p->(s&!z&X(!z U t)))))
+EOF
+
+success=:
+while read f; do
+  # If the labels of the state have only digits, assume the minimization
+  # worked.
+  x=`../ltl2tgba -f -Rm "!($f)" |
+     grep -v -- '->' |
+     sed -n 's/.*label="\(..*\)".*/\1/p' |
+     tr -d '0-9\n'`
+  case $x in
+  "") echo "OK !($f)";;
+  *) echo "KO !($f)"; success=false;;
+  esac
+done < obligations.txt
+
+echo ====
+
+while read f; do
+  # If the labels of the state have only digits, assume the minimization
+  # worked.
+  x=`../ltl2tgba -f -Rm "!($f)" |
+     grep -v -- '->' |
+     sed -n 's/.*label="\(..*\)".*/\1/p' |
+     tr -d '0-9\n'`
+  case $x in
+  "") echo "wrongly minimized !($f)"; success=false;;
+  *) echo "OK !($f)";;
+  esac
+done < non-obligations.txt
+
+$success