diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index bd7a600a2..be323a06f 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -42,6 +42,7 @@ ltlvisit_HEADERS = \ randomltl.hh \ reduce.hh \ simpfg.hh \ + simplify.hh \ syntimpl.hh \ tostring.hh \ tunabbrev.hh @@ -63,6 +64,7 @@ libltlvisit_la_SOURCES = \ randomltl.cc \ reduce.cc \ simpfg.cc \ + simplify.cc \ syntimpl.cc \ tostring.cc \ tunabbrev.cc diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 1392b41b1..9ab588de9 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -21,279 +21,20 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "nenoform.hh" -#include "ltlast/allnodes.hh" -#include +#include "simplify.hh" namespace spot { namespace ltl { - namespace - { - class negative_normal_form_visitor: public visitor - { - public: - negative_normal_form_visitor(bool negated) - : negated_(negated) - { - } - - virtual - ~negative_normal_form_visitor() - { - } - - formula* result() const - { - return result_; - } - - void - visit(atomic_prop* ap) - { - formula* f = ap->clone(); - if (negated_) - result_ = unop::instance(unop::Not, f); - else - result_ = f; - } - - void - visit(constant* c) - { - if (!negated_) - { - result_ = c; - return; - } - - switch (c->val()) - { - case constant::True: - result_ = constant::false_instance(); - return; - case constant::False: - result_ = constant::true_instance(); - return; - case constant::EmptyWord: - result_ = unop::instance(unop::Not, - constant::empty_word_instance()); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(unop* uo) - { - formula* f = uo->child(); - switch (uo->op()) - { - case unop::Not: - result_ = recurse_(f, negated_ ^ true); - return; - case unop::X: - /* !Xa == X!a */ - result_ = unop::instance(unop::X, recurse(f)); - return; - case unop::F: - /* !Fa == G!a */ - result_ = unop::instance(negated_ ? unop::G : unop::F, - recurse(f)); - return; - case unop::G: - /* !Ga == F!a */ - result_ = unop::instance(negated_ ? unop::F : unop::G, - recurse(f)); - return; - case unop::Closure: - result_ = unop::instance(negated_ ? - unop::NegClosure : unop::Closure, - recurse_(f, false)); - return; - case unop::NegClosure: - result_ = unop::instance(negated_ ? - unop::Closure : uo->op(), - recurse_(f, false)); - return; - /* !Finish(x), is not simplified */ - case unop::Finish: - result_ = unop::instance(uo->op(), recurse_(f, false)); - if (negated_) - result_ = unop::instance(unop::Not, result_); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(bunop* bo) - { - // !(a*) is not simplified - result_ = bunop::instance(bo->op(), recurse_(bo->child(), false), - bo->min(), bo->max()); - if (negated_) - result_ = unop::instance(unop::Not, result_); - } - - void - visit(binop* bo) - { - formula* f1 = bo->first(); - formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - /* !(a ^ b) == a <=> b */ - result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Equiv: - /* !(a <=> b) == a ^ b */ - result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Implies: - if (negated_) - /* !(a => b) == a & !b */ - result_ = multop::instance(multop::And, - recurse_(f1, false), - recurse_(f2, true)); - else - result_ = binop::instance(binop::Implies, - recurse(f1), recurse(f2)); - return; - case binop::U: - /* !(a U b) == !a R !b */ - result_ = binop::instance(negated_ ? binop::R : binop::U, - recurse(f1), recurse(f2)); - return; - case binop::R: - /* !(a R b) == !a U !b */ - result_ = binop::instance(negated_ ? binop::U : binop::R, - recurse(f1), recurse(f2)); - return; - case binop::W: - /* !(a W b) == !a M !b */ - result_ = binop::instance(negated_ ? binop::M : binop::W, - recurse(f1), recurse(f2)); - return; - case binop::M: - /* !(a M b) == !a W !b */ - result_ = binop::instance(negated_ ? binop::W : binop::M, - recurse(f1), recurse(f2)); - return; - case binop::UConcat: - /* !(a []-> b) == a<>-> !b */ - result_ = binop::instance(negated_ ? - binop::EConcat : binop::UConcat, - recurse_(f1, false), recurse(f2)); - return; - case binop::EConcat: - /* !(a <>-> b) == a[]-> !b */ - result_ = binop::instance(negated_ ? - binop::UConcat : binop::EConcat, - recurse_(f1, false), recurse(f2)); - return; - case binop::EConcatMarked: - /* !(a <>-> b) == a[]-> !b */ - result_ = binop::instance(negated_ ? - binop::UConcat : - binop::EConcatMarked, - recurse_(f1, false), recurse(f2)); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(automatop* ao) - { - bool negated = negated_; - negated_ = false; - automatop::vec* res = new automatop::vec; - unsigned aos = ao->size(); - for (unsigned i = 0; i < aos; ++i) - res->push_back(recurse(ao->nth(i))); - result_ = automatop::instance(ao->get_nfa(), res, negated); - } - - void - visit(multop* mo) - { - multop::type op = mo->op(); - /* !(a & b & c) == !a | !b | !c */ - /* !(a | b | c) == !a & !b & !c */ - if (negated_) - switch (op) - { - case multop::And: - op = multop::Or; - break; - case multop::Or: - op = multop::And; - break; - case multop::Concat: - case multop::Fusion: - case multop::AndNLM: - break; - } - multop::vec* res = new multop::vec; - unsigned mos = mo->size(); - switch (op) - { - case multop::And: - case multop::Or: - { - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(op, res); - break; - } - case multop::Concat: - case multop::Fusion: - case multop::AndNLM: - { - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse_(mo->nth(i), false)); - result_ = multop::instance(op, res); - assert(!negated_); - } - } - } - - formula* - recurse_(formula* f, bool negated) - { - return negative_normal_form(f, negated); - } - - formula* - recurse(formula* f) - { - return recurse_(f, negated_); - } - - protected: - formula* result_; - bool negated_; - }; - } - formula* negative_normal_form(const formula* f, bool negated) { if (!negated && f->is_in_nenoform()) return f->clone(); - negative_normal_form_visitor v(negated); - const_cast(f)->accept(v); - return v.result(); + + ltl_simplifier s; + return s.negative_normal_form(f, negated); } } diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index 3569c1359..f26c25153 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -23,7 +25,6 @@ # define SPOT_LTLVISIT_NENOFORM_HH #include "ltlast/formula.hh" -#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc new file mode 100644 index 000000000..c6109dc97 --- /dev/null +++ b/src/ltlvisit/simplify.cc @@ -0,0 +1,561 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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. + + +#include "simplify.hh" +#include "misc/hash.hh" +#include "tgba/bdddict.hh" +#include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" +#include + +namespace spot +{ + namespace ltl + { + + // The name of this class is public, but not its contents. + class ltl_simplifier_cache + { + typedef Sgi::hash_map > f2f_map; + typedef Sgi::hash_map > f2b_map; + public: + ltl_simplifier_options options; + + ~ltl_simplifier_cache() + { + { + f2f_map::iterator i = simplified_.begin(); + f2f_map::iterator end = simplified_.end(); + while (i != end) + { + f2f_map::iterator old = i++; + old->second->destroy(); + old->first->destroy(); + } + } + { + f2f_map::iterator i = nenoform_.begin(); + f2f_map::iterator end = nenoform_.end(); + while (i != end) + { + f2f_map::iterator old = i++; + old->second->destroy(); + old->first->destroy(); + } + } + { + f2b_map::iterator i = as_bdd_.begin(); + f2b_map::iterator end = as_bdd_.end(); + while (i != end) + { + f2b_map::iterator old = i++; + old->first->destroy(); + } + } + + dict_.unregister_all_my_variables(this); + } + + ltl_simplifier_cache() + { + } + + ltl_simplifier_cache(ltl_simplifier_options opt) : options(opt) + { + } + + // Convert a Boolean formula into a BDD for easier comparison. + bdd + as_bdd(const formula* f) + { + // Lookup the result in case it has already been computed. + f2b_map::const_iterator it = as_bdd_.find(f); + if (it != as_bdd_.end()) + return it->second; + + bdd result = bddfalse; + + switch (f->kind()) + { + case formula::Constant: + if (f == constant::true_instance()) + result = bddtrue; + else if (f == constant::false_instance()) + result = bddtrue; + else + assert(!"Unsupported operator"); + break; + case formula::AtomicProp: + result = bdd_ithvar(dict_.register_proposition(f, this)); + break; + case formula::UnOp: + { + const unop* uo = static_cast(f); + assert(uo->op() == unop::Not); + result = !as_bdd(uo->child()); + break; + } + case formula::BinOp: + { + const binop* bo = static_cast(f); + int op = 0; + switch (bo->op()) + { + case binop::Xor: + op = bddop_xor; + break; + case binop::Implies: + op = bddop_imp; + break; + case binop::Equiv: + op = bddop_biimp; + break; + default: + assert(!"Unsupported operator"); + } + result = bdd_apply(as_bdd(bo->first()), as_bdd(bo->second()), op); + break; + } + case formula::MultOp: + { + const multop* mo = static_cast(f); + switch (mo->op()) + { + case multop::And: + { + result = bddtrue; + unsigned s = mo->size(); + for (unsigned n = 0; n < s; ++n) + result &= as_bdd(mo->nth(n)); + break; + } + case multop::Or: + { + result = bddfalse; + unsigned s = mo->size(); + for (unsigned n = 0; n < s; ++n) + result |= as_bdd(mo->nth(n)); + break; + } + case multop::Concat: + case multop::Fusion: + case multop::AndNLM: + assert(!"Unsupported operator"); + break; + } + break; + } + case formula::BUnOp: + case formula::AutomatOp: + assert(!"Unsupported operator"); + break; + } + + // Cache the result before returning. + as_bdd_[f->clone()] = result; + return result; + } + + const formula* + lookup_nenoform(const formula* f) + { + f2f_map::const_iterator i = nenoform_.find(f); + if (i == nenoform_.end()) + return 0; + return i->second->clone(); + } + + void + cache_nenoform(const formula* orig, const formula* nenoform) + { + nenoform_[orig->clone()] = nenoform->clone(); + } + + const formula* + lookup_simplified(const formula* f) + { + f2f_map::const_iterator i = simplified_.find(f); + if (i == simplified_.end()) + return 0; + return i->second->clone(); + } + + void + cache_simplified(const formula* orig, const formula* simplified) + { + simplified_[orig->clone()] = simplified->clone(); + } + + private: + bdd_dict dict_; + f2b_map as_bdd_; + f2f_map simplified_; + f2f_map nenoform_; + }; + + + namespace + { + // Forward declaration. + const formula* + nenoform_recursively(const formula* f, + bool negated, + ltl_simplifier_cache* c); + + class negative_normal_form_visitor: public visitor + { + public: + negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c) + : negated_(negated), cache_(c) + { + } + + virtual + ~negative_normal_form_visitor() + { + } + + formula* result() const + { + return result_; + } + + void + visit(atomic_prop* ap) + { + formula* f = ap->clone(); + if (negated_) + result_ = unop::instance(unop::Not, f); + else + result_ = f; + } + + void + visit(constant* c) + { + // Negation of constants is taken care of in the constructor + // of unop::Not, so these cases should be caught by + // nenoform_recursively(). + assert(!negated_); + result_ = c; + return; + } + + void + visit(unop* uo) + { + formula* f = uo->child(); + switch (uo->op()) + { + case unop::Not: + // "Not"s should be caught by nenoform_recursively(). + assert(!"Not should not occur"); + //result_ = recurse_(f, negated_ ^ true); + return; + case unop::X: + /* !Xa == X!a */ + result_ = unop::instance(unop::X, recurse(f)); + return; + case unop::F: + /* !Fa == G!a */ + result_ = unop::instance(negated_ ? unop::G : unop::F, + recurse(f)); + return; + case unop::G: + /* !Ga == F!a */ + result_ = unop::instance(negated_ ? unop::F : unop::G, + recurse(f)); + return; + case unop::Closure: + result_ = unop::instance(negated_ ? + unop::NegClosure : unop::Closure, + recurse_(f, false)); + return; + case unop::NegClosure: + result_ = unop::instance(negated_ ? + unop::Closure : uo->op(), + recurse_(f, false)); + return; + /* !Finish(x), is not simplified */ + case unop::Finish: + result_ = unop::instance(uo->op(), recurse_(f, false)); + if (negated_) + result_ = unop::instance(unop::Not, result_); + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(bunop* bo) + { + // !(a*) is not simplified + result_ = bunop::instance(bo->op(), recurse_(bo->child(), false), + bo->min(), bo->max()); + if (negated_) + result_ = unop::instance(unop::Not, result_); + } + + void + visit(binop* bo) + { + formula* f1 = bo->first(); + formula* f2 = bo->second(); + switch (bo->op()) + { + case binop::Xor: + /* !(a ^ b) == a <=> b */ + result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, + recurse_(f1, false), + recurse_(f2, false)); + return; + case binop::Equiv: + /* !(a <=> b) == a ^ b */ + result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, + recurse_(f1, false), + recurse_(f2, false)); + return; + case binop::Implies: + if (negated_) + /* !(a => b) == a & !b */ + result_ = multop::instance(multop::And, + recurse_(f1, false), + recurse_(f2, true)); + else + result_ = binop::instance(binop::Implies, + recurse(f1), recurse(f2)); + return; + case binop::U: + /* !(a U b) == !a R !b */ + result_ = binop::instance(negated_ ? binop::R : binop::U, + recurse(f1), recurse(f2)); + return; + case binop::R: + /* !(a R b) == !a U !b */ + result_ = binop::instance(negated_ ? binop::U : binop::R, + recurse(f1), recurse(f2)); + return; + case binop::W: + /* !(a W b) == !a M !b */ + result_ = binop::instance(negated_ ? binop::M : binop::W, + recurse(f1), recurse(f2)); + return; + case binop::M: + /* !(a M b) == !a W !b */ + result_ = binop::instance(negated_ ? binop::W : binop::M, + recurse(f1), recurse(f2)); + return; + case binop::UConcat: + /* !(a []-> b) == a<>-> !b */ + result_ = binop::instance(negated_ ? + binop::EConcat : binop::UConcat, + recurse_(f1, false), recurse(f2)); + return; + case binop::EConcat: + /* !(a <>-> b) == a[]-> !b */ + result_ = binop::instance(negated_ ? + binop::UConcat : binop::EConcat, + recurse_(f1, false), recurse(f2)); + return; + case binop::EConcatMarked: + /* !(a <>-> b) == a[]-> !b */ + result_ = binop::instance(negated_ ? + binop::UConcat : + binop::EConcatMarked, + recurse_(f1, false), recurse(f2)); + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(automatop* ao) + { + bool negated = negated_; + negated_ = false; + automatop::vec* res = new automatop::vec; + unsigned aos = ao->size(); + for (unsigned i = 0; i < aos; ++i) + res->push_back(recurse(ao->nth(i))); + result_ = automatop::instance(ao->get_nfa(), res, negated); + } + + void + visit(multop* mo) + { + multop::type op = mo->op(); + /* !(a & b & c) == !a | !b | !c */ + /* !(a | b | c) == !a & !b & !c */ + if (negated_) + switch (op) + { + case multop::And: + op = multop::Or; + break; + case multop::Or: + op = multop::And; + break; + case multop::Concat: + case multop::Fusion: + case multop::AndNLM: + break; + } + multop::vec* res = new multop::vec; + unsigned mos = mo->size(); + switch (op) + { + case multop::And: + case multop::Or: + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(op, res); + break; + } + case multop::Concat: + case multop::Fusion: + case multop::AndNLM: + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse_(mo->nth(i), false)); + result_ = multop::instance(op, res); + assert(!negated_); + } + } + } + + formula* + recurse_(formula* f, bool negated) + { + return const_cast(nenoform_recursively(f, negated, cache_)); + } + + formula* + recurse(formula* f) + { + return recurse_(f, negated_); + } + + protected: + formula* result_; + bool negated_; + ltl_simplifier_cache* cache_; + }; + + + const formula* + nenoform_recursively(const formula* f, + bool negated, + ltl_simplifier_cache* c) + { + if (f->kind() == formula::UnOp) + { + const unop* uo = static_cast(f); + if (uo->op() == unop::Not) + { + negated = !negated; + f = uo->child(); + } + } + + const formula* key = f; + if (negated) + key = unop::instance(unop::Not, f->clone()); + const formula* result = c->lookup_nenoform(key); + if (result) + goto done; + + if (key->is_in_nenoform() + || (c->options.nenoform_stop_on_boolean && key->is_boolean())) + { + result = key->clone(); + } + else + { + negative_normal_form_visitor v(negated, c); + const_cast(f)->accept(v); + result = v.result(); + } + + c->cache_nenoform(key, result); + done: + if (negated) + key->destroy(); + + return result; + } + + } + + + + const formula* + simplify_recursively(const formula* f, + ltl_simplifier_cache* c) + { + const formula* result = c->lookup_simplified(f); + if (result) + return result; + + result = 0;// XXX + + c->cache_simplified(f, result); + return result; + } + + + ////////////////////////////////////////////////////////////////////// + // ltl_simplifier + + ltl_simplifier::ltl_simplifier() + : cache_(new ltl_simplifier_cache) + { + } + + ltl_simplifier::ltl_simplifier(ltl_simplifier_options& opt) + : cache_(new ltl_simplifier_cache(opt)) + { + } + + ltl_simplifier::~ltl_simplifier() + { + delete cache_; + } + + formula* + ltl_simplifier::simplify(const formula* f) + { + return const_cast(simplify_recursively(f, cache_)); + } + + formula* + ltl_simplifier::negative_normal_form(const formula* f, bool negated) + { + return const_cast(nenoform_recursively(f, negated, cache_)); + } + + + } +} diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh new file mode 100644 index 000000000..ff1977c42 --- /dev/null +++ b/src/ltlvisit/simplify.hh @@ -0,0 +1,92 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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. + +#ifndef SPOT_LTLVISIT_SIMPLIFY_HH +# define SPOT_LTLVISIT_SIMPLIFY_HH + +#include "ltlast/formula.hh" +#include "bdd.h" + +namespace spot +{ + namespace ltl + { + class ltl_simplifier_options + { + public: + ltl_simplifier_options() + : reduce_basics(true), + synt_impl(true), + event_univ(true), + containment_checks(false), + containment_checks_stronger(false), + // If true, Boolean subformulae will not be put into + // negative normal form. + nenoform_stop_on_boolean(false) + { + } + + bool reduce_basics; + bool synt_impl; + bool event_univ; + bool containment_checks; + bool containment_checks_stronger; + bool nenoform_stop_on_boolean; + }; + + // fwd declaration to hide technical details. + class ltl_simplifier_cache; + + /// \brief Rewrite or simplify \a f in various ways. + /// \ingroup ltl_rewriting + class ltl_simplifier + { + public: + ltl_simplifier(); + ltl_simplifier(ltl_simplifier_options& opt); + ~ltl_simplifier(); + + /// Simplify the formula \a f (using options supplied to the constructor). + formula* simplify(const formula* f); + + /// Build the negative normal form of formula \a f. + /// All negations of the formula are pushed in front of the + /// atomic propositions. + /// + /// \param f The formula to normalize. + /// \param negated If \c true, return the negative normal form of + /// \c !f + /// + /// Note that this will not remove abbreviated operators. If you + /// want to remove abbreviations, call spot::ltl::unabbreviate_logic + /// or spot::ltl::unabbreviate_ltl first. (Calling these functions + /// after spot::ltl::negative_normal_form would likely produce a + /// formula which is not in negative normal form.) + formula* negative_normal_form(const formula* f, bool negated = false); + + + private: + ltl_simplifier_cache* cache_; + }; + } + +} + +#endif // SPOT_LTLVISIT_SIMPLIFY_HH