diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test index 0f6d1595c..e48bb059b 100755 --- a/src/ltltest/nenoform.test +++ b/src/ltltest/nenoform.test @@ -1,8 +1,8 @@ #! /bin/sh -# 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 +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -44,7 +44,7 @@ run 0 ../nenoform 'a & b' 'b & a & b' run 0 ../nenoform 'a & !b' '!b & a & a' run 0 ../nenoform 'a & b & (Xc |(f U !g)| e)' \ 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b' -run 0 ../nenoform 'GFa => FGb' 'GFa => FGb' +run 0 ../nenoform 'GFa => FGb' 'FG!a || FGb' # Basic rewritings run 0 ../nenoform '!!a' 'a' @@ -52,8 +52,8 @@ run 0 ../nenoform '!!!!!a' '!a' run 0 ../nenoform '!Xa' 'X!a' run 0 ../nenoform '!Fa' 'G!a' run 0 ../nenoform '!Ga' 'F!a' -run 0 ../nenoform '!(a ^ b)' 'a <=> b' -run 0 ../nenoform '!(a <=> b)' '(((a) ^ (b)))' +run 0 ../nenoform '!(a ^ b)' '!a&!b | a&b' +run 0 ../nenoform '!(a <=> b)' '(!a&b) | a&!b' run 0 ../nenoform '!(a => b)' 'a&!b' run 0 ../nenoform '!(!a => !b)' '!a&b' run 0 ../nenoform '!(a U b)' '!a R !b' diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index f20c8a1a2..59ac8e82b 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -202,7 +202,7 @@ main(int argc, char** argv) spot::ltl::formula* ftmp1; ftmp1 = f1; - f1 = simp->negative_normal_form(f1, false, true); + f1 = simp->negative_normal_form(f1, false); ftmp1->destroy(); int length_f1_before = spot::ltl::length(f1); @@ -219,7 +219,7 @@ main(int argc, char** argv) if (f2) { ftmp1 = f2; - f2 = simp->negative_normal_form(f2, false, true); + f2 = simp->negative_normal_form(f2, false); ftmp1->destroy(); f2s = spot::ltl::to_string(f2); } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 0d577f502..4fd965c3b 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -365,15 +365,13 @@ 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, bool lunabbrev, - ltl_simplifier_cache* c) - : negated_(negated), lunabbrev_(lunabbrev), cache_(c) + negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c) + : negated_(negated), cache_(c) { } @@ -466,10 +464,6 @@ namespace spot 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 @@ -513,10 +507,6 @@ namespace spot result_ = multop::instance(multop::And, recurse_(f1, false), recurse_(f2, true)); - else if (!lunabbrev_) - result_ = binop::instance(binop::Implies, - recurse_(f1, false), - recurse_(f2, false)); else // a => b == !a | b result_ = multop::instance(multop::Or, recurse_(f1, true), @@ -626,8 +616,7 @@ namespace spot recurse_(formula* f, bool negated) { return - const_cast(nenoform_recursively(f, negated, - lunabbrev_, cache_)); + const_cast(nenoform_recursively(f, negated, cache_)); } formula* @@ -639,7 +628,6 @@ namespace spot protected: formula* result_; bool negated_; - bool lunabbrev_; ltl_simplifier_cache* cache_; }; @@ -647,7 +635,6 @@ namespace spot const formula* nenoform_recursively(const formula* f, bool negated, - bool lunabbrev, ltl_simplifier_cache* c) { if (f->kind() == formula::UnOp) @@ -674,7 +661,7 @@ namespace spot } else { - negative_normal_form_visitor v(negated, lunabbrev, c); + negative_normal_form_visitor v(negated, c); const_cast(f)->accept(v); result = v.result(); } @@ -2277,7 +2264,7 @@ namespace spot { formula* neno = 0; if (!f->is_in_nenoform()) - f = neno = negative_normal_form(f, false, true); + f = neno = negative_normal_form(f, false); formula* res = const_cast(simplify_recursively(f, cache_)); if (neno) neno->destroy(); @@ -2285,11 +2272,9 @@ namespace spot } formula* - ltl_simplifier::negative_normal_form(const formula* f, bool negated, - bool lunabbrev) + ltl_simplifier::negative_normal_form(const formula* f, bool negated) { - return const_cast(nenoform_recursively(f, negated, lunabbrev, - cache_)); + return const_cast(nenoform_recursively(f, negated, cache_)); } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 62277e52a..5b93ec22c 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -75,16 +75,13 @@ namespace spot /// Build the negative normal form of formula \a f. /// All negations of the formula are pushed in front of the - /// atomic propositions. + /// atomic propositions. Operators <=>, =>, xor are all removed + /// (calling spot::ltl::unabbreviate_ltl is not needed). /// /// \param f The formula to normalize. /// \param negated If \c true, return the negative normal form of /// \c !f - /// \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); + formula* negative_normal_form(const formula* f, bool negated = false); private: diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b4d94b065..8e7d2ea00 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1604,7 +1604,7 @@ namespace spot // logic abbreviations such as <=>, =>, or XOR, since they // would involve negations at the BDD level. ltl_simplifier s; - f2 = s.negative_normal_form(f, false, true); + f2 = s.negative_normal_form(f, false); } typedef std::set set_type;