From fea49630f63ff0de9f4988a97ac927f6ac220d2b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 12 Oct 2011 08:16:45 +0800 Subject: [PATCH] Merge the syntactic implication code with ltl_simplifier. So that we can latter use some combined optimizations. * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Integrate the code from syntimpl.cc * src/ltlvisit/syntimpl.hh, src/ltlvisit/syntimpl.cc: Delete. All code has been moved above. * src/ltlvisit/Makefile.am: Adjust. * src/ltltest/syntimpl.cc: Adjust code. --- src/ltltest/syntimpl.cc | 9 +- src/ltlvisit/Makefile.am | 2 - src/ltlvisit/simplify.cc | 658 ++++++++++++++++++++++++++++++++++++--- src/ltlvisit/simplify.hh | 26 ++ src/ltlvisit/syntimpl.cc | 649 -------------------------------------- src/ltlvisit/syntimpl.hh | 84 ----- 6 files changed, 649 insertions(+), 779 deletions(-) delete mode 100644 src/ltlvisit/syntimpl.cc delete mode 100644 src/ltlvisit/syntimpl.hh diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index a6b11f761..e851ca08c 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -29,7 +29,7 @@ #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/syntimpl.hh" +#include "ltlvisit/simplify.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/nenoform.hh" @@ -67,8 +67,7 @@ main(int argc, char** argv) std::string f2s = spot::ltl::to_string(f2); int exit_return = 0; - spot::ltl::syntactic_implication_cache* c = - new spot::ltl::syntactic_implication_cache; + spot::ltl::ltl_simplifier* c = new spot::ltl::ltl_simplifier; switch (opt) { diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index e6446864f..786bbd14a 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -42,7 +42,6 @@ ltlvisit_HEADERS = \ reduce.hh \ simpfg.hh \ simplify.hh \ - syntimpl.hh \ tostring.hh \ tunabbrev.hh @@ -63,6 +62,5 @@ libltlvisit_la_SOURCES = \ reduce.cc \ simpfg.cc \ simplify.cc \ - syntimpl.cc \ tostring.cc \ tunabbrev.cc diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 85db90587..9afd20750 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -32,7 +32,6 @@ #include "tgba/bdddict.hh" #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" -#include "ltlvisit/syntimpl.hh" #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" #include @@ -42,6 +41,7 @@ namespace spot namespace ltl { + // The name of this class is public, but not its contents. class ltl_simplifier_cache { @@ -49,10 +49,11 @@ namespace spot ptr_hash > f2f_map; typedef Sgi::hash_map > f2b_map; + typedef std::pair pairf; + typedef std::map syntimpl_cache_t; public: bdd_dict dict; ltl_simplifier_options options; - syntactic_implication_cache syntimpl; language_containment_checker lcc; ~ltl_simplifier_cache() @@ -86,6 +87,16 @@ namespace spot old->first->destroy(); } } + { + syntimpl_cache_t::iterator i = syntimpl_.begin(); + syntimpl_cache_t::iterator end = syntimpl_.end(); + while (i != end) + { + syntimpl_cache_t::iterator old = i++; + old->first.first->destroy(); + old->first.second->destroy(); + } + } dict_.unregister_all_my_variables(this); } @@ -118,7 +129,7 @@ namespace spot if (f == constant::true_instance()) result = bddtrue; else if (f == constant::false_instance()) - result = bddtrue; + result = bddfalse; else assert(!"Unsupported operator"); break; @@ -219,16 +230,7 @@ namespace spot // Return true if f1 => f2 syntactically bool - syntactic_implication(const formula* f1, const formula* f2) - { - // We cannot run syntactic_implication on SERE formulae, - // except on Boolean formulae. - if (f1->is_sere_formula() && !f1->is_boolean()) - return false; - if (f2->is_sere_formula() && !f2->is_boolean()) - return false; - return syntimpl.syntactic_implication(f1, f2); - } + syntactic_implication(const formula* f1, const formula* f2); // Return true if f1 => f2 bool @@ -242,30 +244,7 @@ namespace spot // If right==false, true if !f1 => f2, false otherwise. // If right==true, true if f1 => !f2, false otherwise. bool - syntactic_implication_neg(const formula* f1, const formula* f2, - bool right) - { - // We cannot run syntactic_implication_neg on SERE formulae, - // except on Boolean formulae. - if (f1->is_sere_formula() && !f1->is_boolean()) - return false; - if (f2->is_sere_formula() && !f2->is_boolean()) - return false; - trace << "[SIN] Does " << (right ? "(" : "!(") - << to_string(f1) << ") implies " - << (right ? "!(" : "(") << to_string(f2) << ") ?" - << std::endl; - if (syntimpl.syntactic_implication_neg(f1, f2, right)) - { - trace << "[SIN] Yes" << std::endl; - return true; - } - else - { - trace << "[SIN] No" << std::endl; - return false; - } - } + syntactic_implication_neg(const formula* f1, const formula* f2, bool right); // Return true if f1 => !f2 bool contained_neg(const formula* f1, const formula* f2) @@ -350,11 +329,514 @@ namespace spot f2b_map as_bdd_; f2f_map simplified_; f2f_map nenoform_; + syntimpl_cache_t syntimpl_; }; 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 @@ -2240,9 +2722,95 @@ namespace spot } - - ////////////////////////////////////////////////////////////////////// + // ltl_simplifier_cache + + + // Return true if f1 => f2 syntactically + bool + ltl_simplifier_cache::syntactic_implication(const formula* f1, + const formula* f2) + { + // We cannot run syntactic_implication on SERE formulae, + // except on Boolean formulae. + if (f1->is_sere_formula() && !f1->is_boolean()) + return false; + if (f2->is_sere_formula() && !f2->is_boolean()) + return false; + + if (f1 == f2) + return true; + if (f2 == constant::true_instance() + || f1 == constant::false_instance()) + return true; + + // Cache lookup + { + pairf p(f1, f2); + syntimpl_cache_t::const_iterator i = syntimpl_.find(p); + if (i != syntimpl_.end()) + return i->second; + } + + bool result = false; + + 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; + } + + // Cache result + { + pairf p(f1->clone(), f2->clone()); + syntimpl_[p] = result; + } + + return result; + } + + // If right==false, true if !f1 => f2, false otherwise. + // If right==true, true if f1 => !f2, false otherwise. + bool + ltl_simplifier_cache::syntactic_implication_neg(const formula* f1, + const formula* f2, + bool right) + { + // We cannot run syntactic_implication_neg on SERE formulae, + // except on Boolean formulae. + if (f1->is_sere_formula() && !f1->is_boolean()) + return false; + 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(); + } + else + { + const formula* old = l; + l = nenoform_recursively(l, true, this); + old->destroy(); + } + + return syntactic_implication(l, r); + } + + + ///////////////////////////////////////////////////////////////////// // ltl_simplifier ltl_simplifier::ltl_simplifier() @@ -2278,6 +2846,18 @@ namespace spot return const_cast(nenoform_recursively(f, negated, cache_)); } + bool + ltl_simplifier::syntactic_implication(const formula* f1, const formula* f2) + { + return cache_->syntactic_implication(f1, f2); + } + + bool + ltl_simplifier::syntactic_implication_neg(const formula* f1, const formula* f2, + bool right) + { + return cache_->syntactic_implication_neg(f1, f2, right); + } } } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 5b93ec22c..0ddb4c085 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -83,6 +83,32 @@ namespace spot /// \c !f formula* negative_normal_form(const formula* f, bool negated = false); + /// \brief Syntactic implication. + /// + /// Returns whether \a f syntactically implies \a g. + /// + /// This is adapted from + /// \verbatim + /// @InProceedings{ somenzi.00.cav, + /// author = {Fabio Somenzi and Roderick Bloem}, + /// title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, + /// booktitle = {Proceedings of the 12th International Conference on + /// Computer Aided Verification (CAV'00)}, + /// pages = {247--263}, + /// year = {2000}, + /// volume = {1855}, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag} + /// } + /// \endverbatim + /// + bool syntactic_implication(const formula* f, const formula* g); + /// \brief Syntactic implication with one negated argument. + /// + /// If \a right is true, this method returns whether + /// \a f implies !\a g. If \a right is false, this returns + /// whether !\a g implies \a g. + bool syntactic_implication_neg(const formula* f, const formula* g, bool right); private: ltl_simplifier_cache* cache_; diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc deleted file mode 100644 index e0c96efb2..000000000 --- a/src/ltlvisit/syntimpl.cc +++ /dev/null @@ -1,649 +0,0 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// 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. - -#include "syntimpl.hh" -#include "ltlast/allnodes.hh" -#include - -#include "lunabbrev.hh" -#include "simpfg.hh" -#include "nenoform.hh" - -namespace spot -{ - namespace ltl - { - namespace - { - - class inf_right_recurse_visitor: public const_visitor - { - public: - - inf_right_recurse_visitor(const formula *f, - syntactic_implication_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: - if (uo == f) - result_ = true; - 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(a) = true U a */ - 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; - syntactic_implication_cache* c; - }; - - ///////////////////////////////////////////////////////////////////////// - - class inf_left_recurse_visitor: public const_visitor - { - public: - - inf_left_recurse_visitor(const formula *f, - syntactic_implication_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; - 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; - syntactic_implication_cache* c; - }; - - } // anonymous - - // This is called by syntactic_implication() after the - // formulae have been normalized. - bool - syntactic_implication_cache::syntactic_implication(const formula* f1, - const formula* f2) - { - if (f1 == f2) - return true; - if (f2 == constant::true_instance() - || f1 == constant::false_instance()) - return true; - - // Cache lookup - { - pairf p(f1, f2); - cache_t::const_iterator i = cache_.find(p); - if (i != cache_.end()) - return i->second; - } - - bool result = false; - - 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; - } - - // Cache result - { - pairf p(f1->clone(), f2->clone()); - cache_[p] = result; - } - - return result; - } - - bool - syntactic_implication_cache::syntactic_implication_neg(const formula* f1, - const formula* f2, - bool right) - { - formula* l = f1->clone(); - formula* r = f2->clone(); - if (right) - r = unop::instance(unop::Not, r); - else - l = unop::instance(unop::Not, l); - - // Cache lookup - { - pairf p(l, r); - cache_t::const_iterator i = cache_.find(p); - if (i != cache_.end()) - { - l->destroy(); - r->destroy(); - return i->second; - } - } - // Save the cache key for latter. - pairf p(l->clone(), r->clone()); - - formula* tmp = unabbreviate_logic(l); - l->destroy(); - l = simplify_f_g(tmp); - tmp->destroy(); - tmp = negative_normal_form(l); - l->destroy(); - l = tmp; - - tmp = unabbreviate_logic(r); - r->destroy(); - r = simplify_f_g(tmp); - tmp->destroy(); - tmp = negative_normal_form(r); - r->destroy(); - r = tmp; - - bool result = syntactic_implication(l, r); - l->destroy(); - r->destroy(); - - // Cache result if is has not be done by syntactic_implication() already. - if (l != p.first || r != p.second) - { - cache_[p] = result; - } - else - { - p.first->destroy(); - p.second->destroy(); - } - return result; - } - - syntactic_implication_cache::~syntactic_implication_cache() - { - cache_t::const_iterator i = cache_.begin(); - while (i != cache_.end()) - { - // Advance the iterator before deleting the key. - pairf p = i->first; - ++i; - - p.first->destroy(); - p.second->destroy(); - } - } - - } -} diff --git a/src/ltlvisit/syntimpl.hh b/src/ltlvisit/syntimpl.hh deleted file mode 100644 index a91f18f7c..000000000 --- a/src/ltlvisit/syntimpl.hh +++ /dev/null @@ -1,84 +0,0 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// 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. - -#ifndef SPOT_LTLVISIT_SYNTIMPL_HH -# define SPOT_LTLVISIT_SYNTIMPL_HH - -#include "ltlast/formula.hh" -#include - -namespace spot -{ - namespace ltl - { - - /// \brief Syntactic implication. - /// \ingroup ltl_misc - /// - /// This comes from - /// \verbatim - /// @InProceedings{ somenzi.00.cav, - /// author = {Fabio Somenzi and Roderick Bloem}, - /// title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, - /// booktitle = {Proceedings of the 12th International Conference on - /// Computer Aided Verification (CAV'00)}, - /// pages = {247--263}, - /// year = {2000}, - /// volume = {1855}, - /// series = {Lecture Notes in Computer Science}, - /// publisher = {Springer-Verlag} - /// } - /// \endverbatim - class syntactic_implication_cache - { - private: - typedef std::pair pairf; - typedef std::map cache_t; - cache_t cache_; - // Copy disallowed. - syntactic_implication_cache(const syntactic_implication_cache&); - public: - syntactic_implication_cache() {}; - - /// \brief Syntactic implication. - /// - /// Return true if f1 < f2. - bool syntactic_implication(const formula* f1, const formula* f2); - - /// \brief Syntactic implication. - /// - /// If right==false, true if !f1 < f2, false otherwise. - /// If right==true, true if f1 < !f2, false otherwise. - /// - /// \see syntactic_implication - bool syntactic_implication_neg(const formula* f1, const formula* f2, - bool right); - - ~syntactic_implication_cache(); - }; - - - } -} - -#endif // SPOT_LTLVISIT_SYNTIMPL_HH