From 369ad87e50ba1524a959bedf15fa6dce1aecc412 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 30 Oct 2011 18:48:27 +0100 Subject: [PATCH] Rewrite syntactic implication using a single function. * src/ltlvisit/simplify.cc (inf_left_recurse_visitor, inf_right_recurse_visitor): Remove. (syntactic_implication, syntactic_implication_aux): Rewrite all rules for syntactic implication. (syntactic_implication_neg): Simplify. --- src/ltlvisit/simplify.cc | 853 ++++++++++++++------------------------- 1 file changed, 311 insertions(+), 542 deletions(-) diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 63b6bbd8b..74bd536b5 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -231,6 +231,8 @@ namespace spot // Return true if f1 => f2 syntactically bool syntactic_implication(const formula* f1, const formula* f2); + bool + syntactic_implication_aux(const formula* f1, const formula* f2); // Return true if f1 => f2 bool @@ -336,508 +338,6 @@ namespace spot namespace { - // Check if f implies the visited formula. - class inf_right_recurse_visitor: public const_visitor - { - public: - - inf_right_recurse_visitor(const formula *f, - ltl_simplifier_cache* c) - : result_(false), f(f), c(c) - { - } - - virtual - ~inf_right_recurse_visitor() - { - } - - int - result() const - { - return result_; - } - - void - visit(const atomic_prop* ap) - { - if (f == ap) - result_ = true; - } - - void - visit(const constant* c) - { - switch (c->val()) - { - case constant::True: - result_ = true; - return; - case constant::False: - result_ = false; - return; - case constant::EmptyWord: - result_ = false; - } - } - - void - visit(const bunop*) - { - } - - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - switch (uo->op()) - { - case unop::Not: - // !f1 => !f1 - if (uo == f) - { - result_ = true; - return; - } - // !a => !f1 if f1 => a - if (f->kind() == formula::UnOp) - { - const unop* op = static_cast(f); - if (op->op() == unop::Not) - result_ = c->syntactic_implication(f1, op->child()); - } - return; - case unop::X: - { - if (f->kind() != formula::UnOp) - return; - const unop* op = static_cast(f); - if (op->op() == unop::X) - result_ = c->syntactic_implication(op->child(), f1); - } - return; - case unop::F: - // f => F(f1) if f => f1 - result_ = c->syntactic_implication(f, f1); - return; - case unop::G: - /* G(a) = false R a */ - if (c->syntactic_implication(f, constant::false_instance())) - result_ = true; - return; - case unop::Finish: - case unop::Closure: - case unop::NegClosure: - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const binop* bo) - { - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - return; - case binop::U: - case binop::W: - if (c->syntactic_implication(f, f2)) - result_ = true; - return; - case binop::R: - if (f->kind() == formula::BinOp) - { - const binop* fb = static_cast(f); - if (fb->op() == binop::R - && c->syntactic_implication(fb->first(), f1) - && c->syntactic_implication(fb->second(), f2)) - { - result_ = true; - return; - } - } - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu->op() == unop::G - && f1 == constant::false_instance() - && c->syntactic_implication(fu->child(), f2)) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f, f1) - && c->syntactic_implication(f, f2)) - result_ = true; - return; - case binop::M: - if (f->kind() == formula::BinOp) - { - const binop* fb = static_cast(f); - if (fb->op() == binop::M - && c->syntactic_implication(fb->first(), f1) - && c->syntactic_implication(fb->second(), f2)) - { - result_ = true; - return; - } - } - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu->op() == unop::F - && f2 == constant::true_instance() - && c->syntactic_implication(fu->child(), f1)) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f, f1) - && c->syntactic_implication(f, f2)) - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const automatop*) - { - assert(0); - } - - void - visit(const multop* mo) - { - multop::type op = mo->op(); - unsigned mos = mo->size(); - switch (op) - { - case multop::And: - for (unsigned i = 0; i < mos; ++i) - if (!c->syntactic_implication(f, mo->nth(i))) - return; - result_ = true; - break; - case multop::Or: - for (unsigned i = 0; i < mos && !result_; ++i) - if (c->syntactic_implication(f, mo->nth(i))) - result_ = true; - break; - case multop::Concat: - case multop::Fusion: - case multop::AndNLM: - break; - } - } - - protected: - bool result_; /* true if f < f1, false otherwise. */ - const formula* f; - ltl_simplifier_cache* c; - }; - - ///////////////////////////////////////////////////////////////////////// - - // Check if the visited formula implies f. - class inf_left_recurse_visitor: public const_visitor - { - public: - - inf_left_recurse_visitor(const formula *f, - ltl_simplifier_cache* c) - : result_(false), f(f), c(c) - { - } - - virtual - ~inf_left_recurse_visitor() - { - } - - bool - special_case(const binop* f2) - { - if (f->kind() != formula::BinOp) - return false; - const binop* fb = static_cast(f); - if (fb->op() == f2->op() - && c->syntactic_implication(f2->first(), fb->first()) - && c->syntactic_implication(f2->second(), fb->second())) - return true; - return false; - } - - bool - special_case_check(const formula* f2) - { - if (f2->kind() != formula::BinOp) - return false; - return special_case(static_cast(f2)); - } - - int - result() const - { - return result_; - } - - void - visit(const atomic_prop* ap) - { - inf_right_recurse_visitor v(ap, c); - const_cast(f)->accept(v); - result_ = v.result(); - } - - void - visit(const bunop*) - { - } - - void - visit(const constant* cst) - { - inf_right_recurse_visitor v(cst, c); - switch (cst->val()) - { - case constant::True: - const_cast(f)->accept(v); - result_ = v.result(); - return; - case constant::False: - result_ = true; - return; - case constant::EmptyWord: - result_ = true; // FIXME - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const unop* uo) - { - const formula* f1 = uo->child(); - inf_right_recurse_visitor v(uo, c); - switch (uo->op()) - { - case unop::Not: - if (uo == f) - result_ = true; - return; - case unop::X: - if (f->kind() == formula::UnOp) - { - const unop* op = static_cast(f); - if (op->op() == unop::X) - result_ = c->syntactic_implication(f1, op->child()); - } - return; - case unop::F: - { - /* F(a) = true U a */ - const formula* tmp = binop::instance(binop::U, - constant::true_instance(), - f1->clone()); - if (special_case_check(tmp)) - { - result_ = true; - tmp->destroy(); - return; - } - if (c->syntactic_implication(tmp, f)) - result_ = true; - tmp->destroy(); - return; - } - case unop::G: - { - /* G(a) = false R a */ - const formula* tmp = binop::instance(binop::R, - constant::false_instance(), - f1->clone()); - if (special_case_check(tmp)) - { - result_ = true; - tmp->destroy(); - return; - } - if (c->syntactic_implication(tmp, f)) - result_ = true; - tmp->destroy(); - return; - } - case unop::Finish: - case unop::Closure: - case unop::NegClosure: - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const binop* bo) - { - if (special_case(bo)) - { - result_ = true; - return; - } - - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - case binop::Equiv: - case binop::Implies: - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - return; - case binop::U: - /* (a < c) && (c < d) => a U b < c U d */ - if (f->kind() == formula::BinOp) - { - const binop* fb = static_cast(f); - if (fb->op() == binop::U - && c->syntactic_implication(f1, fb->first()) - && c->syntactic_implication(f2, fb->second())) - { - result_ = true; - return; - } - } - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu->op() == unop::F - && f1 == constant::true_instance() - && c->syntactic_implication(f2, fu->child())) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f1, f) - && c->syntactic_implication(f2, f)) - result_ = true; - return; - case binop::W: - /* (a < c) && (c < d) => a W b < c W d */ - if (f->kind() == formula::BinOp) - { - const binop* fb = static_cast(f); - if (fb->op() == binop::W - && c->syntactic_implication(f1, fb->first()) - && c->syntactic_implication(f2, fb->second())) - { - result_ = true; - return; - } - } - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu && fu->op() == unop::G - && f2 == constant::false_instance() - && c->syntactic_implication(f1, fu->child())) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f1, f) - && c->syntactic_implication(f2, f)) - result_ = true; - return; - case binop::R: - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu->op() == unop::G - && f1 == constant::false_instance() - && c->syntactic_implication(f2, fu->child())) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f2, f)) - result_ = true; - return; - case binop::M: - if (f->kind() == formula::UnOp) - { - const unop* fu = static_cast(f); - if (fu->op() == unop::F - && f2 == constant::true_instance() - && c->syntactic_implication(f1, fu->child())) - { - result_ = true; - return; - } - } - if (c->syntactic_implication(f2, f)) - result_ = true; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const automatop*) - { - assert(0); - } - - void - visit(const multop* mo) - { - multop::type op = mo->op(); - unsigned mos = mo->size(); - switch (op) - { - case multop::And: - for (unsigned i = 0; (i < mos) && !result_; ++i) - if (c->syntactic_implication(mo->nth(i), f)) - result_ = true; - break; - case multop::Or: - for (unsigned i = 0; i < mos; ++i) - if (!c->syntactic_implication(mo->nth(i), f)) - return; - result_ = true; - break; - case multop::Concat: - case multop::Fusion: - case multop::AndNLM: - break; - } - } - - protected: - bool result_; /* true if f1 < f, 1 otherwise. */ - const formula* f; - ltl_simplifier_cache* c; - }; - ////////////////////////////////////////////////////////////////////// // // NEGATIVE_NORMAL_FORM_VISITOR @@ -2727,61 +2227,336 @@ namespace spot // ltl_simplifier_cache - // Return true if f1 => f2 syntactically + // This implements the recursive rules for syntactic implication. + // (To follow this code please look at the table given as an + // appendix in the documentation for temporal logic operators.) + inline bool - ltl_simplifier_cache::syntactic_implication(const formula* f1, - const formula* f2) + ltl_simplifier_cache::syntactic_implication_aux(const formula* f, + const formula* g) + { + formula::opkind fk = f->kind(); + formula::opkind gk = g->kind(); + + // Deal with all lines except the first one. + switch (fk) + { + case formula::Constant: + case formula::AtomicProp: + case formula::BUnOp: + case formula::AutomatOp: + break; + + case formula::UnOp: + { + const unop* f_ = down_cast(f); + unop::type fo = f_->op(); + + if (gk == formula::UnOp) + { + const unop* g_ = down_cast(g); + unop::type go = g_->op(); + if (fo == unop::F) + { + if ((go == unop::F) + && syntactic_implication(f_->child(), g_->child())) + return true; + } + else if (fo == unop::G) + { + if ((go == unop::G || go == unop::X) + && syntactic_implication(f_->child(), g_->child())) + return true; + } + else if (fo == unop::X) + { + if ((go == unop::F || go == unop::X) + && syntactic_implication(f_->child(), g_->child())) + return true; + } + } + else if (gk == formula::BinOp && fo == unop::G) + { + const binop* g_ = down_cast(g); + binop::type go = g_->op(); + const formula* g1 = g_->first(); + const formula* g2 = g_->second(); + if ((go == binop::U || go == binop::R) + && syntactic_implication(f_->child(), g2)) + return true; + else if (go == binop::W + && (syntactic_implication(f_->child(), g1) + || syntactic_implication(f_->child(), g2))) + return true; + else if (go == binop::M + && (syntactic_implication(f_->child(), g1) + && syntactic_implication(f_->child(), g2))) + return true; + } + // First column. + if (fo == unop::G && syntactic_implication(f_->child(), g)) + return true; + break; + } + + case formula::BinOp: + { + const binop* f_ = down_cast(f); + binop::type fo = f_->op(); + const formula* f1 = f_->first(); + const formula* f2 = f_->second(); + + if (gk == formula::UnOp) + { + const unop* g_ = down_cast(g); + unop::type go = g_->op(); + if (go == unop::F) + { + if (fo == binop::U) + { + if (syntactic_implication(f2, g_->child())) + return true; + } + else if (fo == binop::W) + { + if (syntactic_implication(f1, g_->child()) + && syntactic_implication(f2, g_->child())) + return true; + } + else if (fo == binop::R) + { + if (syntactic_implication(f2, g_->child())) + return true; + } + else if (fo == binop::M) + { + if (syntactic_implication(f1, g_->child()) + || syntactic_implication(f2, g_->child())) + return true; + } + } + } + else if (gk == formula::BinOp) + { + const binop* g_ = down_cast(g); + binop::type go = g_->op(); + const formula* g1 = g_->first(); + const formula* g2 = g_->second(); + + if ((fo == binop::U && (go == binop::U || go == binop::W)) + || (fo == binop::W && go == binop::W) + || (fo == binop::R && go == binop::R) + || (fo == binop::M && (go == binop::R || go == binop::M))) + { + if (syntactic_implication(f1, g1) + && syntactic_implication(f2, g2)) + return true; + } + else if (fo == binop::W && go == binop::U) + { + if (syntactic_implication(f1, g2) + && syntactic_implication(f2, g2)) + return true; + } + else if (fo == binop::R && go == binop::M) + { + if (syntactic_implication(f2, g1) + && syntactic_implication(f2, g2)) + return true; + } + else if ((fo == binop::U && (go == binop::R || go == binop::M)) + || (fo == binop::W && go == binop::R)) + { + if (syntactic_implication(f1, g1) + && syntactic_implication(f2, g1) + && syntactic_implication(f2, g2)) + return true; + } + else if ((fo == binop::M && (go == binop::U || go == binop::W)) + || (fo == binop::R && go == binop::W)) + { + if (syntactic_implication(f1, g2) + && syntactic_implication(f2, g1)) + return true; + } + } + + // First column. + if (fo == binop::U || fo == binop::W) + { + if (syntactic_implication(f1, g) + && syntactic_implication(f2, g)) + return true; + } + else if (fo == binop::R || fo == binop::M) + { + if (syntactic_implication(f2, g)) + return true; + } + break; + } + case formula::MultOp: + { + const multop* f_ = down_cast(f); + multop::type fo = f_->op(); + unsigned fs = f_->size(); + + // First column. + switch (fo) + { + case multop::Or: + { + bool b = true; + for (unsigned i = 0; i < fs; ++i) + if (!syntactic_implication(f_->nth(i), g)) + { + b &= false; + break; + } + if (b) + return true; + break; + } + case multop::And: + { + for (unsigned i = 0; i < fs; ++i) + if (syntactic_implication(f_->nth(i), g)) + return true; + break; + } + case multop::Concat: + case multop::Fusion: + case multop::AndNLM: + break; + } + break; + } + } + + // First line. + switch (gk) + { + case formula::Constant: + case formula::AtomicProp: + case formula::BUnOp: + case formula::AutomatOp: + break; + + case formula::UnOp: + { + const unop* g_ = down_cast(g); + unop::type go = g_->op(); + if (go == unop::F) + { + if (syntactic_implication(f, g_->child())) + return true; + } + break; + } + case formula::BinOp: + { + const binop* g_ = down_cast(g); + binop::type go = g_->op(); + const formula* g1 = g_->first(); + const formula* g2 = g_->second(); + + if (go == binop::U || go == binop::W) + { + if (syntactic_implication(f, g2)) + return true; + } + else if (go == binop::M || go == binop::R) + { + if (syntactic_implication(f, g1) + && syntactic_implication(f, g2)) + return true; + } + break; + } + case formula::MultOp: + { + const multop* g_ = down_cast(g); + multop::type go = g_->op(); + unsigned gs = g_->size(); + + switch (go) + { + case multop::And: + { + bool b = true; + for (unsigned i = 0; i < gs; ++i) + if (!syntactic_implication(f, g_->nth(i))) + { + b &= false; + break; + } + if (b) + return true; + break; + } + case multop::Or: + { + for (unsigned i = 0; i < gs; ++i) + if (syntactic_implication(f, g_->nth(i))) + return true; + break; + } + case multop::Concat: + case multop::Fusion: + case multop::AndNLM: + break; + } + break; + } + } + return false; + } + + // Return true if f => g syntactically + bool + ltl_simplifier_cache::syntactic_implication(const formula* f, + const formula* g) { // We cannot run syntactic_implication on SERE formulae, // except on Boolean formulae. - if (f1->is_sere_formula() && !f1->is_boolean()) + if (f->is_sere_formula() && !f->is_boolean()) return false; - if (f2->is_sere_formula() && !f2->is_boolean()) + if (g->is_sere_formula() && !g->is_boolean()) return false; - if (f1 == f2) + if (f == g) return true; - if (f2 == constant::true_instance() - || f1 == constant::false_instance()) + if (g == constant::true_instance() + || f == constant::false_instance()) return true; // Cache lookup { - pairf p(f1, f2); + pairf p(f, g); syntimpl_cache_t::const_iterator i = syntimpl_.find(p); if (i != syntimpl_.end()) return i->second; } - bool result = false; + bool result; - if (f1->is_boolean() && f2->is_boolean()) + if (f->is_boolean() && g->is_boolean()) { - bdd l = as_bdd(f1); - bdd r = as_bdd(f2); + bdd l = as_bdd(f); + bdd r = as_bdd(g); result = ((l & r) == l); } else { - inf_left_recurse_visitor v1(f2, this); - const_cast(f1)->accept(v1); - if (v1.result()) - { - result = true; - } - else - { - inf_right_recurse_visitor v2(f1, this); - const_cast(f2)->accept(v2); - if (v2.result()) - result = true; - } + result = syntactic_implication_aux(f, g); } // Cache result { - pairf p(f1->clone(), f2->clone()); + pairf p(f->clone(), g->clone()); syntimpl_[p] = result; + // std::cerr << to_string(f) << (result ? " ==> " : " =/=> ") + // << to_string(g) << std::endl; } return result; @@ -2801,22 +2576,16 @@ namespace spot if (f2->is_sere_formula() && !f2->is_boolean()) return false; - const formula* l = f1->clone(); - const formula* r = f2->clone(); if (right) - { - const formula* old = r; - r = nenoform_recursively(r, true, this); - old->destroy(); - } + f2 = nenoform_recursively(f2, true, this); else - { - const formula* old = l; - l = nenoform_recursively(l, true, this); - old->destroy(); - } + f1 = nenoform_recursively(f1, true, this); - return syntactic_implication(l, r); + bool result = syntactic_implication(f1, f2); + + (right ? f2 : f1)->destroy(); + + return result; }