From 536e45b34288dd32b4db179fb34c808ccd195ab0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Jun 2012 14:45:25 +0200 Subject: [PATCH] Arrange multops so that Boolean arguments come first. This helps recursive implication checks. Also order atomic propositions with strverscmp(). * src/ltlast/formula.hh (formula_ptr_less_than_multop, is_literal, atomic_prop_cmp): New. * src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them. * src/ltlast/multop.cc: Use formula_ptr_less_than_multop. * src/ltltest/isop.test, src/ltltest/ltlfilt.test, src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/explicit.test, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests. * NEWS: Mention the new order. --- NEWS | 5 +++ src/ltlast/formula.cc | 22 +++++++++++ src/ltlast/formula.hh | 75 ++++++++++++++++++++++++++++++++++++++ src/ltlast/multop.cc | 31 +++++++--------- src/ltltest/isop.test | 8 ++-- src/ltltest/ltlfilt.test | 4 +- src/tgbatest/det.test | 8 ++-- src/tgbatest/dstar.test | 4 +- src/tgbatest/explicit.test | 4 +- src/tgbatest/explpro2.test | 9 ++--- src/tgbatest/explpro3.test | 10 +---- src/tgbatest/explprod.test | 9 ++--- src/tgbatest/nondet.test | 4 +- src/tgbatest/tripprod.test | 7 +--- 14 files changed, 143 insertions(+), 57 deletions(-) diff --git a/NEWS b/NEWS index 3f3d70560..6db246f97 100644 --- a/NEWS +++ b/NEWS @@ -158,6 +158,11 @@ New in spot 1.1.4a (not relased) Small or Deterministic. These can now be combined with Complete as Any|Complete, Small|Complete, or Deterministic|Complete. + - operands of n-ary operators (like & and |) are now ordered so + that Boolean terms come first. This speeds up syntactic + implication checks slightly. Also, literals are now sorted + using strverscmp(), so that p5 comes before p12. + - All the parsers implemented in Spot now use the same type to store locations. diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 655c704ae..c7cbd27a0 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -20,9 +20,14 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include "formula.hh" #include "misc/hash.hh" +#include "misc/casts.hh" #include +#include "unop.hh" +#include "atomic_prop.hh" +#include namespace spot { @@ -114,5 +119,22 @@ namespace spot return out; } + + + const formula* is_literal(const formula* f) + { + const unop* g = is_Not(f); + if (g) + f = g->child(); + return is_atomic_prop(f); + } + + int atomic_prop_cmp(const formula* f, const formula* g) + { + const atomic_prop* a = down_cast(f); + const atomic_prop* b = down_cast(g); + return strverscmp(a->name().c_str(), b->name().c_str()); + } + } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 6b36f2fc3..35141e90c 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -354,6 +354,20 @@ namespace spot opkind kind_; }; + + /// \brief Change \a f into a if it is equal to + /// !a or a. + /// + /// Return 0 otherwise. + SPOT_API + const formula* is_literal(const formula* f); + + + /// Compare two atomic propositions. + SPOT_API + int atomic_prop_cmp(const formula* f, const formula* g); + + /// \ingroup ltl_essentials /// \brief Strict Weak Ordering for const formula*. /// @@ -377,6 +391,67 @@ namespace spot assert(right); if (left == right) return false; + + size_t l = left->hash(); + size_t r = right->hash(); + if (l != r) + return l < r; + // Because the hash code assigned to each formula is the + // number of formulae constructed so far, it is very unlikely + // that we will ever reach a case were two different formulae + // have the same hash. This will happen only ever with have + // produced 256**sizeof(size_t) formulae (i.e. max_count has + // looped back to 0 and started over). In that case we can + // order two formulae by looking at their text representation. + // We could be more efficient and look at their AST, but it's + // not worth the burden. (Also ordering pointers is ruled out + // because it breaks the determinism of the implementation.) + return left->dump() < right->dump(); + } + }; + + /// \brief Strict Weak Ordering for const formula* + /// inside ltl::multop. + /// \ingroup ltl_essentials + /// + /// This is the comparison functor used by to order the + /// ltl::multop operands. It keeps Boolean formulae first in + /// order to speed up implication checks. + /// + /// Also keep literal alphabetically ordered. + struct formula_ptr_less_than_multop: + public std::binary_function + { + bool + operator()(const formula* left, const formula* right) const + { + assert(left); + assert(right); + if (left == right) + return false; + + // We want Boolean formulae first. + bool lib = left->is_boolean(); + if (lib != right->is_boolean()) + return lib; + + // We have two Boolean formulae + if (lib) + { + // Literals should come first + const formula* litl = is_literal(left); + const formula* litr = is_literal(right); + if (!litl != !litr) + return litl; + if (litl) + { + // And they should be sorted alphabetically + int cmp = atomic_prop_cmp(litl, litr); + if (cmp) + return cmp < 0; + } + } + size_t l = left->hash(); size_t r = right->hash(); if (l != r) diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 30bdbd817..aa07f9582 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -199,13 +199,13 @@ namespace spot } } // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // AndNLM(And(Bool1,Bool2),Exps1...,Exps2...,Exps3...) // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + // AndRat(And(Bool1,Bool2),Exps1...,Exps2...,Exps3...) // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2)) + // AndRat(Or(Bool1,Bool2),Exps1...,Exps2...,Exps3...) if (!b->empty()) - v->push_back(multop::instance(op, b)); + v->insert(v->begin(), multop::instance(op, b)); else delete b; } @@ -240,18 +240,15 @@ namespace spot i = v->erase(i); continue; } - if (const multop* p = is_multop(*i)) + if (const multop* p = is_multop(*i, op)) { - if (p->op() == op) - { - unsigned ps = p->size(); - for (unsigned n = 0; n < ps; ++n) - inlined.push_back(p->nth(n)->clone()); - (*i)->destroy(); - // FIXME: Do not use erase. See previous FIXME. - i = v->erase(i); - continue; - } + unsigned ps = p->size(); + for (unsigned n = 0; n < ps; ++n) + inlined.push_back(p->nth(n)->clone()); + (*i)->destroy(); + // FIXME: Do not use erase. See previous FIXME. + i = v->erase(i); + continue; } // All operator except "Concat" and "Fusion" are // commutative, so we just keep a list of the inlined @@ -263,13 +260,13 @@ namespace spot ++i; } if (op == Concat || op == Fusion) - *v = inlined; + v->swap(inlined); else v->insert(v->end(), inlined.begin(), inlined.end()); } if (op != Concat && op != Fusion) - std::sort(v->begin(), v->end(), formula_ptr_less_than()); + std::sort(v->begin(), v->end(), formula_ptr_less_than_multop()); unsigned orig_size = v->size(); diff --git a/src/ltltest/isop.test b/src/ltltest/isop.test index 989bbc459..2a5a1f553 100755 --- a/src/ltltest/isop.test +++ b/src/ltltest/isop.test @@ -33,9 +33,9 @@ run 0 ../../bin/ltlfilt --boolean-to-isop input > output cat> expected<-> ((a & !b) | (b & !a)) +{{{{!a && !b} | {b && d}}}[*];a[*]}<>-> ((!a & b) | (a & !b)) EOF cat output @@ -46,9 +46,9 @@ run 0 ../../bin/ltlfilt input > output cat> expected< b) & (b -> d) -(a -> b) & Xc & (b -> d) +(a -> b) & (b -> d) & Xc GF((a | b) & (b | d)) -{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!b | !a)) +{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!a | !b)) EOF cat output diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index 5e5ad3e95..c1640e1ad 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -90,7 +90,7 @@ b W GFa Fb G(a & Xb) Xa -F(a & X(b & !a)) +F(a & X(!a & b)) a & (b | c) EOF @@ -98,7 +98,7 @@ checkopt --simplify --eventual --unique <formulas <<'EOF' -1,14,X((a M F((!c & !b) | (c & b))) W (G!c U b)) +1,14,X((a M F((!b & !c) | (b & c))) W (G!c U b)) 1,5,X(((a & b) R (!a U !c)) R b) 1,10,XXG(Fa U Xb) 1,5,(!a M !b) W F!c 1,3,(b & Fa & GFc) R a -1,2,(a R (b W a)) W G(!a M (c | b)) -1,11,(Fa W b) R (Fc | !a) +1,2,(a R (b W a)) W G(!a M (b | c)) +1,11,(Fa W b) R (!a | Fc) 1,7,X(G(!a M !b) | G(a | G!a)) 1,2,Fa W Gb 1,3,Ga | GFb @@ -49,7 +49,7 @@ cat >formulas <<'EOF' 1,4,X(Gb | GFa) 1,9,X(Gc | XG((b & Ga) | (!b & F!a))) 1,2,Ga R Fb -1,3,G(a U (b | X((!c & !a) | (a & c)))) +1,3,G(a U (b | X((!a & !c) | (a & c)))) 1,5,XG((G!a & F!b) | (Fa & (a | Gb))) 1,10,(a U X!a) | XG(!b & XFc) 1,4,X(G!a | GFa) diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index 8dde21c58..826837ce0 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -216,7 +216,7 @@ digraph G { 1 [label="1"] 1 -> 2 [label="!a & !b\n"] 1 -> 3 [label="a & !b\n"] - 1 -> 4 [label="b & !a\n"] + 1 -> 4 [label="!a & b\n"] 1 -> 5 [label="a & b\n"] 2 [label="2"] 2 -> 2 [label="!b\n"] @@ -224,7 +224,7 @@ digraph G { 3 [label="4", peripheries=2] 3 -> 2 [label="!a & !b\n{Acc[1]}"] 3 -> 3 [label="a & !b\n{Acc[1]}"] - 3 -> 4 [label="b & !a\n{Acc[1]}"] + 3 -> 4 [label="!a & b\n{Acc[1]}"] 3 -> 5 [label="a & b\n{Acc[1]}"] 4 [label="3", peripheries=2] 4 -> 4 [label="1\n{Acc[1]}"] diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test index 313bd8694..2626c1bf8 100755 --- a/src/tgbatest/explicit.test +++ b/src/tgbatest/explicit.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -25,7 +25,7 @@ set -e -run 0 ../explicit | sed 's/c & b/b \& c/' > stdout +run 0 ../explicit > stdout cat >expected <expected <<'EOF' acc = "p2$1" "p3" "p2" "p1"; -"s1 * s1", "s2 * s2", "b & !a", "p2$1" "p1"; +"s1 * s1", "s2 * s2", "!a & b", "p2$1" "p1"; "s1 * s1", "s3 * s3", "a & !b", "p3" "p2"; EOF -run 0 ../explprod input1 input2 | - sed 's/!a & b/b \& !a/;s/!b & a/a \& !b/'> stdout - -cat stdout +run 0 ../explprod input1 input2 | tee stdout diff stdout expected rm input1 input2 stdout expected diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index 78c53de64..79b0d689b 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -43,13 +43,7 @@ acc = "p2" "p3"; "s1 * s1", "s3 * s3", "a & !b", "p3"; EOF -run 0 ../explprod input1 input2 > stdout - -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed 's/"p3" "p2"/"p2" "p3"/g;s/!b & a/a \& !b/g; - s/b & !a/!a \& b/g' stdout > tmp_ && mv tmp_ stdout - -cat stdout +run 0 ../explprod input1 input2 | +sed 's/"p3" "p2"/"p2" "p3"/g' | tee stdout diff stdout expected rm input1 input2 stdout expected diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 94c6d54c4..c28a62b4f 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -1,6 +1,6 @@ #!/bin/sh -# Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Université Pierre et Marie Curie. @@ -46,9 +46,6 @@ acc = "p3" "p2" "p1"; "s2 * s2", "s3 * s1", "a & c", "p3" "p1"; EOF -run 0 ../explprod input1 input2 | - sed 's/b & a/a \& b/;s/c & a/a \& c/' > stdout - -cat stdout +run 0 ../explprod input1 input2 | tee stdout diff stdout expected rm input1 input2 stdout expected diff --git a/src/tgbatest/nondet.test b/src/tgbatest/nondet.test index 170e13721..556122a54 100755 --- a/src/tgbatest/nondet.test +++ b/src/tgbatest/nondet.test @@ -25,7 +25,7 @@ cat >expected.1<expected.2< stdout - -cat stdout +run 0 ../tripprod input1 input2 input3 | tee stdout diff stdout expected rm input1 input2 input3 stdout expected