From 54e10c25016be5e2ee411f14851ea36aa8dfd674 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 13 Apr 2010 10:38:08 +0200 Subject: [PATCH] "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 | 14 +++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/ltl2tgba.cc | 62 +++++++++++++++++++- src/tgbatest/safety.test | 2 +- src/tgbatest/spotlbtt.test | 8 +++ src/tgbatest/wdba.test | 117 +++++++++++++++++++++++++++++++++++++ 6 files changed, 202 insertions(+), 2 deletions(-) create mode 100755 src/tgbatest/wdba.test diff --git a/ChangeLog b/ChangeLog index 1f9c8c250..07938b241 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2010-04-13 Alexandre Duret-Lutz + + "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 Better resource handling in minimization. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 154a99005..0d3c5cdf3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -93,6 +93,7 @@ TESTS = \ reductgba.test \ scc.test \ safety.test \ + wdba.test \ randtgba.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6f5cb41f3..f87fe2552 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/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) diff --git a/src/tgbatest/safety.test b/src/tgbatest/safety.test index cd7712921..964ed3847 100755 --- a/src/tgbatest/safety.test +++ b/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 <obligations.txt <(!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 <(!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