From c0085a8f30aa87d97bd02229c45159cd8bc01902 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 24 Aug 2011 17:40:22 +0200 Subject: [PATCH] Move the remaining reduce() logic into ltl_simplifier. * src/ltlvisit/simplify.hh (ltl_simplifier::negative_normal_form): Allow logical unabbreviations during the NNF pass. * src/ltlvisit/simplify.cc (ltl_simplifier::negative_normal_form) (negative_normal_form_visitor): Adjust. (ltl_simplifier::simplify): Request unabbreviations. * src/ltlvisit/reduce.cc (reduce): Remove most of the code, leaving only a call ltl_simplifier and some wrapper code to convert options. * src/ltltest/reduccmp.test: Add more test cases. --- src/ltltest/reduccmp.test | 7 +++ src/ltlvisit/reduce.cc | 35 +-------------- src/ltlvisit/simplify.cc | 91 +++++++++++++++++++++++++++------------ src/ltlvisit/simplify.hh | 12 +++--- 4 files changed, 77 insertions(+), 68 deletions(-) diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index b7dc60912..e1ec09ec8 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -66,6 +66,11 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'a | (b U a) | a' '(b U a)' run 0 $x 'a U (b U a)' '(b U a)' + run 0 $x 'a <-> !a' '0' + run 0 $x 'a <-> a' '1' + run 0 $x 'a ^ a' '0' + run 0 $x 'a ^ !a' '1' + # Basic reductions run 0 $x 'X(true)' 'true' run 0 $x 'X(false)' 'false' @@ -121,6 +126,8 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)' run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb' + run 0 $x 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)' + run 0 $x 'Gb W a' 'Gb|a' run 0 $x 'Fb M Fa' 'Fa & Fb' diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index e20781729..116cdcb2a 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -22,25 +22,16 @@ // 02111-1307, USA. #include "reduce.hh" -#include "ltlast/allnodes.hh" #include - -#include "lunabbrev.hh" -#include "simpfg.hh" #include "simplify.hh" namespace spot { namespace ltl { - formula* reduce(const formula* f, int opt) { - formula* f1; - formula* f2; - formula* prev = 0; - ltl_simplifier_options o; o.reduce_basics = opt & Reduce_Basics; o.synt_impl = opt & Reduce_Syntactic_Implications; @@ -48,31 +39,7 @@ namespace spot o.containment_checks = opt & Reduce_Containment_Checks; o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger; ltl_simplifier simplifier(o); - - int n = 0; - - while (f != prev) - { - ++n; - assert(n < 100); - if (prev) - { - prev->destroy(); - prev = const_cast(f); - } - else - { - prev = f->clone(); - } - f1 = unabbreviate_logic(f); - f2 = simplify_f_g(f1); - f1->destroy(); - f = simplifier.simplify(f2); - f2->destroy(); - } - prev->destroy(); - - return const_cast(f); + return const_cast(simplifier.simplify(f)); } bool diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 23bccb1ac..0d577f502 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -365,13 +365,15 @@ namespace spot const formula* nenoform_recursively(const formula* f, bool negated, + bool lunabbrev, 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) + negative_normal_form_visitor(bool negated, bool lunabbrev, + ltl_simplifier_cache* c) + : negated_(negated), lunabbrev_(lunabbrev), cache_(c) { } @@ -455,13 +457,41 @@ namespace spot void visit(bunop* bo) { - // !(a*) is not simplified + // !(a*) is not simplified, whatever that means result_ = bunop::instance(bo->op(), recurse_(bo->child(), false), bo->min(), bo->max()); if (negated_) result_ = unop::instance(unop::Not, result_); } + formula* equiv_or_xor(bool equiv, formula* f1, formula* f2) + { + if (!lunabbrev_) + return binop::instance(equiv ? binop::Equiv : binop::Xor, + recurse_(f1, false), + recurse_(f2, false)); + // Rewrite a<=>b as (a&b)|(!a&!b) + if (equiv) + return + multop::instance(multop::Or, + multop::instance(multop::And, + recurse_(f1, false), + recurse_(f2, false)), + multop::instance(multop::And, + recurse_(f1, true), + recurse_(f2, true))); + else + // Rewrite a^b as (a&!b)|(!a&b) + return + multop::instance(multop::Or, + multop::instance(multop::And, + recurse_(f1, false), + recurse_(f2, true)), + multop::instance(multop::And, + recurse_(f1, true), + recurse_(f2, false))); + } + void visit(binop* bo) { @@ -470,68 +500,69 @@ namespace spot switch (bo->op()) { case binop::Xor: - /* !(a ^ b) == a <=> b */ - result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, - recurse_(f1, false), - recurse_(f2, false)); + // !(a ^ b) == a <=> b + result_ = equiv_or_xor(negated_, f1, f2); return; case binop::Equiv: - /* !(a <=> b) == a ^ b */ - result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, - recurse_(f1, false), - recurse_(f2, false)); + // !(a <=> b) == a ^ b + result_ = equiv_or_xor(!negated_, f1, f2); return; case binop::Implies: if (negated_) - /* !(a => b) == a & !b */ + // !(a => b) == a & !b result_ = multop::instance(multop::And, recurse_(f1, false), recurse_(f2, true)); - else + else if (!lunabbrev_) result_ = binop::instance(binop::Implies, - recurse(f1), recurse(f2)); + recurse_(f1, false), + recurse_(f2, false)); + else // a => b == !a | b + result_ = multop::instance(multop::Or, + recurse_(f1, true), + recurse_(f2, false)); return; case binop::U: - /* !(a U b) == !a R !b */ + // !(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 */ + // !(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 */ + // !(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 */ + // !(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 */ + // !(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 */ + // !(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 */ + // !(a <>-> b) == a[]-> !b result_ = binop::instance(negated_ ? binop::UConcat : binop::EConcatMarked, recurse_(f1, false), recurse(f2)); return; } - /* Unreachable code. */ + // Unreachable code. assert(0); } @@ -594,7 +625,9 @@ namespace spot formula* recurse_(formula* f, bool negated) { - return const_cast(nenoform_recursively(f, negated, cache_)); + return + const_cast(nenoform_recursively(f, negated, + lunabbrev_, cache_)); } formula* @@ -606,6 +639,7 @@ namespace spot protected: formula* result_; bool negated_; + bool lunabbrev_; ltl_simplifier_cache* cache_; }; @@ -613,6 +647,7 @@ namespace spot const formula* nenoform_recursively(const formula* f, bool negated, + bool lunabbrev, ltl_simplifier_cache* c) { if (f->kind() == formula::UnOp) @@ -639,7 +674,7 @@ namespace spot } else { - negative_normal_form_visitor v(negated, c); + negative_normal_form_visitor v(negated, lunabbrev, c); const_cast(f)->accept(v); result = v.result(); } @@ -2242,7 +2277,7 @@ namespace spot { formula* neno = 0; if (!f->is_in_nenoform()) - f = neno = negative_normal_form(f); + f = neno = negative_normal_form(f, false, true); formula* res = const_cast(simplify_recursively(f, cache_)); if (neno) neno->destroy(); @@ -2250,9 +2285,11 @@ namespace spot } formula* - ltl_simplifier::negative_normal_form(const formula* f, bool negated) + ltl_simplifier::negative_normal_form(const formula* f, bool negated, + bool lunabbrev) { - return const_cast(nenoform_recursively(f, negated, cache_)); + return const_cast(nenoform_recursively(f, negated, lunabbrev, + cache_)); } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 438d3c403..62277e52a 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -80,13 +80,11 @@ namespace spot /// \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); + /// \param lunabbrev If \c true, also remove Xor, Equiv, and Implies + /// operators. (It is faster than calling + /// spot::ltl::unabbreviate_ltl first.) + formula* negative_normal_form(const formula* f, bool negated = false, + bool lunabbrev = false); private: