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