From f003c3d16fee6b9a5ad71267d5a30815d50bc6af Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 12 Apr 2010 13:39:28 +0200 Subject: [PATCH] Add LTL reductions for strong release. * src/ltlvisit/basicreduce.cc: Perform the following reductions. a R (b & F(a)) = a M b a M (b & F(a)) = a M b a R Fa = Fa a M Fa = Fa a R b & Fa = a M b a R b & a M c = a M (b & c) a M b & a M c = a M (b & c) * src/ltltest/reduccmp.test: More tests. --- ChangeLog | 34 +++++++++---- src/ltltest/reduccmp.test | 5 ++ src/ltlvisit/basicreduce.cc | 97 ++++++++++++++++++++++++++++++++++--- 3 files changed, 119 insertions(+), 17 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8695ebaef..3dc4c1a6b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2010-04-12 Alexandre Duret-Lutz + + Add LTL reductions for strong release. + + * src/ltlvisit/basicreduce.cc: Perform the following reductions. + a R (b & F(a)) = a M b + a M (b & F(a)) = a M b + a R Fa = Fa + a M Fa = Fa + a R b & Fa = a M b + a R b & a M c = a M (b & c) + a M b & a M c = a M (b & c) + * src/ltltest/reduccmp.test: More tests. + 2010-04-12 Alexandre Duret-Lutz Add LTL reductions for weak until. @@ -1714,7 +1728,7 @@ Remove generated files that git follows. - * INSTALL, lbtt/INSTALL, lbtt/doc/texinfo.tex: Do not track + * INSTALL, lbtt/INSTALL, lbtt/doc/texinfo.tex: Do not track anymore these generated files. 2009-06-05 Guillaume Sadegh @@ -1933,7 +1947,7 @@ Add support for ELTL (AST & parser), and an adaptation of LaCIM for ELTL. - * configure.ac: Adjust for src/eltlparse/ and src/eltltest/ + * configure.ac: Adjust for src/eltlparse/ and src/eltltest/ directories, and call AX_BOOST_BASE. * m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]). * src/Makefile.am: Add eltlparse and eltltest. @@ -2024,16 +2038,16 @@ i->s->clone(). * src/misc/optionmap.hh, src/misc/optionmap.cc: Remove the extra `;' after the namespace. - * src/tgbaalgos/tau03opt.cc + * src/tgbaalgos/tau03opt.cc (tau03_opt_search::add_new_state): Remove unreferenced method. - * src/tgbaalgos/ltl2tgba_fm.cc + * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::dump): Remove unreferenced method. - * src/tgbaalgos/lbtt.cc + * src/tgbaalgos/lbtt.cc (acceptance_cond_splitter::count): Remove unreferenced method. - * src/tgba/tgbabddconcreteproduct.cc + * src/tgba/tgbabddconcreteproduct.cc (tgba_bdd_product_factory::get_dict): Remove unreferenced method. - * src/ltlvisit/syntimpl.cc - (eventual_universal_visitor::recurse): Remove unreferenced method. + * src/ltlvisit/syntimpl.cc + (eventual_universal_visitor::recurse): Remove unreferenced method. * src/tgbaalgos/reductgba_sim.cc: Reindent. 2008-12-11 Alexandre Duret-Lutz @@ -4122,7 +4136,7 @@ Likewise. The classes have been renamed are as following emptiness_check -> couvreur99_check emptiness_check_shy -> couvreur99_check_shy - emptiness_check_status -> couvreur99_check_status + emptiness_check_status -> couvreur99_check_status counter_example -> couvreur99_check_result * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Adjust to renaming and new interface. @@ -4998,7 +5012,7 @@ * src/sanity/Makefile.am (check-local): Run it. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parseerr.test - src/ltltest/tunabbrev.test, src/ltltest/reduc.cc, + src/ltltest/tunabbrev.test, src/ltltest/reduc.cc, src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test, diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 4206f4e64..b6838486a 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -120,6 +120,11 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'a U (G(a))' 'Ga' run 0 $x '(a U b) | (a W c)' 'a W (b | c)' run 0 $x '(a U b) | Ga' 'a W b' + + run 0 $x 'a R (b & F(a) & c)' 'a M (b & c)' + run 0 $x 'a R (F(a))' 'Fa' + run 0 $x '(a R b) & (a M c)' 'a M (b & c)' + run 0 $x '(a R b) & Fa' 'a M b' ;; esac diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index f0cf67959..6c78322f7 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -354,7 +354,46 @@ namespace spot } } } + else if (op == binop::M || op == binop::R) + { + // a R Fa = Fa + // a M Fa = Fa + if (fu2 && fu2->op() == unop::F && fu2->child() == f1) + { + result_ = f2; + f1->destroy(); + return; + } + // a R (b & F(a)) = a M b + // a M (b & F(a)) = a M b + multop* fm2 = dynamic_cast(f2); + if (fm2 && fm2->op() == multop::And) + { + int s = fm2->size(); + for (int i = 0; i < s; ++i) + { + unop* c = dynamic_cast(fm2->nth(i)); + if (c && c->op() == unop::F && c->child() == f1) + { + multop::vec* v = new multop::vec; + v->reserve(s - 1); + int j; + for (j = 0; j < i; ++j) + v->push_back(fm2->nth(j)->clone()); + // skip j=i + for (++j; j < s; ++j) + v->push_back(fm2->nth(j)->clone()); + result_ = + binop::instance(binop::M, f1, + multop::instance(multop::And, + v)); + f2->destroy(); + return; + } + } + } + } result_ = binop::instance(op, f1, f2); return; @@ -420,6 +459,35 @@ namespace spot // G(a) & G(b) = G(a & b) tmpG->push_back(uo->child()->clone()); } + else if (uo->op() == unop::F) + { + // F(a) & (a R b) = a M b + // F(a) & (a M b) = a M b + formula* a = uo->child(); + bool rewritten = false; + for (multop::vec::iterator j = i; + j != res->end(); ++j) + { + if (!*j) + continue; + binop* b = dynamic_cast(*j); + if (b && (b->op() == binop::R + || b->op() == binop::M) + && b->first() == a) + { + binop* r = + binop::instance(binop::M, + a->clone(), + b->second()->clone()); + tmpOther->push_back(r); + (*j)->destroy(); + *j = 0; + rewritten = true; + } + } + if (!rewritten) + tmpOther->push_back(uo->clone()); + } else { tmpOther->push_back((*i)->clone()); @@ -458,22 +526,36 @@ namespace spot tmpUright), ftmp->clone())); } - else if (bo->op() == binop::R) + else if (bo->op() == binop::R || bo->op() == binop::M) { // (a R b) & (a R c) = a R (b & c) + // (a R b) & (a M c) = a M (b & c) + bool weak = true; formula* ftmp = dynamic_cast(*i)->first(); - multop::vec* tmpRright = new multop::vec; + multop::vec* right = new multop::vec; for (multop::vec::iterator j = i; j != res->end(); j++) { if (!*j) continue; + // (a R b) & Fa = a M b. + // (a M b) & Fa = a M b. + unop* uo2 = dynamic_cast(*j); + if (uo2 && uo2->op() == unop::F + && uo2->child() == ftmp) + { + (*j)->destroy(); + *j = 0; + weak = false; + } binop* bo2 = dynamic_cast(*j); - if (bo2 && bo2->op() == binop::R + if (bo2 && (bo2->op() == binop::R + || bo2->op() == binop::M) && ftmp == bo2->first()) { - tmpRright - ->push_back(bo2->second()->clone()); + if (bo2->op() == binop::M) + weak = false; + right->push_back(bo2->second()->clone()); if (j != i) { (*j)->destroy(); @@ -482,11 +564,12 @@ namespace spot } } tmpR - ->push_back(binop::instance(binop::R, + ->push_back(binop::instance(weak ? + binop::R : binop::M, ftmp->clone(), multop:: instance(multop::And, - tmpRright))); + right))); } else {