diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 8c19a45c0..58f15eff9 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1347,6 +1347,10 @@ $\OR$):
f \OR ((\X f) \R g) &\equiv g \W f \\
f \AND ((\X f) \U g) &\equiv g \M f &
f \OR ((\X f) \M g) &\equiv g \U f \\
+ f \AND (g \OR \X(g \R f)) &\equiv g \R f &
+ f \OR (g \AND \X(g \W f)) &\equiv g \W f \\
+ f \AND (g \OR \X(g \M f)) &\equiv g \M f &
+ f \OR (g \AND \X(g \U f)) &\equiv g \U f \\
\end{align*}
The above rules are applied even if more terms are presents in the
operator's arguments. For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index d375b6e4c..23a81dc75 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D�veloppement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012 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.
@@ -133,6 +133,19 @@ namespace spot
return (*children_)[n];
}
+ formula*
+ multop::all_but(unsigned n) const
+ {
+ unsigned s = size();
+ vec* v = new vec;
+ v->reserve(s-1);
+ for (unsigned pos = 0; pos < n; ++pos)
+ v->push_back(nth(pos)->clone());
+ for (unsigned pos = n + 1; pos < s; ++pos)
+ v->push_back(nth(pos)->clone());
+ return instance(op_, v);
+ }
+
multop::type
multop::op() const
{
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index c5412fd58..1cfe4bebb 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -1,8 +1,8 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D�veloppement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012 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.
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@@ -111,15 +111,22 @@ namespace spot
/// Get the number of children.
unsigned size() const;
- /// \brief Get the nth children.
+ /// \brief Get the nth child.
///
/// Starting with \a n = 0.
const formula* nth(unsigned n) const;
- /// \brief Get the nth children.
+ /// \brief Get the nth child.
///
/// Starting with \a n = 0.
formula* nth(unsigned n);
+ /// \brief construct a formula without the nth child.
+ ///
+ /// If the formula \c f is a|b|c|d and d
+ /// is child number 2, then calling f->all_but(2) will
+ /// return a new formula a|b|d.
+ formula* all_but(unsigned n) const;
+
/// Get the type of this operator.
type op() const;
/// Get the type of this operator, as a string.
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 4fa701cb7..b8ccd14c6 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -198,6 +198,10 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'a & (Xa W b) & (Xa U c)' '(b R a) & (c M a)'
run 0 $x 'a & (Xa W b) & XGa' 'Ga'
run 0 $x 'a & (Xa U b) & XGa' '(b M a) & Ga' # Fb & Ga ?
+ run 0 $x 'a|(c&b&X((b&c) U a))|d' '((b&c) U a)|d'
+ run 0 $x 'a|(c&X((b&c) W a)&b)|d' '((b&c) W a)|d'
+ run 0 $x 'a&(c|b|X((b|c) M a))&d' '((b|c) M a)&d'
+ run 0 $x 'a&(c|X((b|c) R a)|b)&d' '((b|c) R a)&d'
# Syntactic implication
run 0 $x '(a & b) R (a R c)' '(a & b)R c'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 1d96e2285..6adae0291 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -672,6 +672,15 @@ namespace spot
return static_cast(f);
}
+
+ unop*
+ is_unop(formula* f)
+ {
+ if (f->kind() != formula::UnOp)
+ return 0;
+ return static_cast(f);
+ }
+
unop*
is_unop(formula* f, unop::type op)
{
@@ -719,6 +728,14 @@ namespace spot
return is_G(op->child());
}
+ binop*
+ is_binop(formula* f)
+ {
+ if (f->kind() != formula::BinOp)
+ return 0;
+ return static_cast(f);
+ }
+
binop*
is_binop(formula* f, binop::type op)
{
@@ -730,6 +747,19 @@ namespace spot
return bo;
}
+ // Same with two choices.
+ binop*
+ is_binop(formula* f, binop::type op1, binop::type op2)
+ {
+ if (f->kind() != formula::BinOp)
+ return 0;
+ binop* bo = static_cast(f);
+ binop::type op = bo->op();
+ if (op == op1 || op == op2)
+ return bo;
+ return 0;
+ }
+
binop*
is_U(formula* f)
{
@@ -759,11 +789,8 @@ namespace spot
formula*
is_XRM(formula* f)
{
- if (f->kind() != formula::BinOp)
- return 0;
- binop* bo = static_cast(f);
- binop::type t = bo->op();
- if (t != binop::R && t != binop::M)
+ binop* bo = is_binop(f, binop::R, binop::M);
+ if (!bo)
return 0;
unop* uo = is_X(bo->first());
if (!uo)
@@ -776,11 +803,8 @@ namespace spot
formula*
is_XWU(formula* f)
{
- if (f->kind() != formula::BinOp)
- return 0;
- binop* bo = static_cast(f);
- binop::type t = bo->op();
- if (t != binop::W && t != binop::U)
+ binop* bo = is_binop(f, binop::W, binop::U);
+ if (!bo)
return 0;
unop* uo = is_X(bo->first());
if (!uo)
@@ -811,6 +835,58 @@ namespace spot
return is_multop(f, multop::Or);
}
+ // b & X(b W a) or b & X(b U a)
+ // This returns (b W a) or (b U a).
+ binop*
+ is_bXbWU(formula* f)
+ {
+ multop* mo = is_multop(f, multop::And);
+ if (!mo)
+ return 0;
+ unsigned s = mo->size();
+ for (unsigned pos = 0; pos < s; ++pos)
+ {
+ unop* u = is_X(mo->nth(pos));
+ if (!u)
+ continue;
+ binop* bo = is_binop(u->child(), binop::U, binop::W);
+ if (!bo)
+ continue;
+ formula* b = mo->all_but(pos);
+ bool result = (b == bo->first());
+ b->destroy();
+ if (result)
+ return bo;
+ }
+ return 0;
+ }
+
+ // b | X(b R a) or b | X(b M a)
+ // This returns (b R a) or (b M a).
+ binop*
+ is_bXbRM(formula* f)
+ {
+ multop* mo = is_multop(f, multop::Or);
+ if (!mo)
+ return 0;
+ unsigned s = mo->size();
+ for (unsigned pos = 0; pos < s; ++pos)
+ {
+ unop* u = is_X(mo->nth(pos));
+ if (!u)
+ continue;
+ binop* bo = is_binop(u->child(), binop::R, binop::M);
+ if (!bo)
+ continue;
+ formula* b = mo->all_but(pos);
+ bool result = (b == bo->first());
+ b->destroy();
+ if (result)
+ return bo;
+ }
+ return 0;
+ }
+
formula*
unop_multop(unop::type uop, multop::type mop, multop::vec* v)
{
@@ -1652,11 +1728,8 @@ namespace spot
return;
}
- // Same effect as dynamic_cast, only faster.
- unop* fu1 =
- (a->kind() == formula::UnOp) ? static_cast(a) : 0;
- unop* fu2 =
- (b->kind() == formula::UnOp) ? static_cast(b) : 0;
+ unop* fu1 = is_unop(a);
+ unop* fu2 = is_unop(b);
// X(a) U X(b) = X(a U b)
// X(a) R X(b) = X(a R b)
@@ -1943,6 +2016,8 @@ namespace spot
// a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...)
// a & (Xa W b) = b R a
// a & (Xa U b) = b M a
+ // a & (b | X(b R a)) = b R a
+ // a & (b | X(b M a)) = b M a
if (!mo->is_X_free())
{
typedef Sgi::hash_setis_X_free())
+ continue;
+
+ binop* barg = is_bXbRM((*res)[n]);
+ if (barg)
+ {
+ wuset[barg->second()].insert(n);
+ continue;
+ }
+
unop* uo = is_X((*res)[n]);
if (!uo)
continue;
@@ -2017,8 +2106,8 @@ namespace spot
(*res)[n] = 0;
}
// Make a second pass to check if the "a"
- // terms can be used to simplify "Xa W b" or
- // "Xa U b".
+ // terms can be used to simplify "Xa W b",
+ // "Xa U b", "b | X(b R a)", or "b | X(b M a)".
for (unsigned n = 0; n < s; ++n)
{
if (!(*res)[n])
@@ -2032,17 +2121,30 @@ namespace spot
std::set::const_iterator g;
for (g = s.begin(); g != s.end(); ++g)
{
- // a & (Xa W b) = b R a
- // a & (Xa U b) = b M a
unsigned pos = *g;
- binop* wu = down_cast((*res)[pos]);
- binop::type t = (wu->op() == binop::U)
- ? binop::M : binop::R;
- unop* xa = down_cast(wu->first());
- formula* a = xa->child()->clone();
- formula* b = wu->second()->clone();
- wu->destroy();
- (*res)[pos] = binop::instance(t, b, a);
+ binop* wu = is_binop((*res)[pos]);
+ if (wu)
+ {
+ // a & (Xa W b) = b R a
+ // a & (Xa U b) = b M a
+ binop::type t = (wu->op() == binop::U)
+ ? binop::M : binop::R;
+ unop* xa = down_cast(wu->first());
+ formula* a = xa->child()->clone();
+ formula* b = wu->second()->clone();
+ wu->destroy();
+ (*res)[pos] = binop::instance(t, b, a);
+ }
+ else
+ {
+ // a & (b | X(b R a)) = b R a
+ // a & (b | X(b M a)) = b M a
+ wu = is_bXbRM((*res)[pos]);
+ assert(wu);
+ wu->clone();
+ (*res)[pos]->destroy();
+ (*res)[pos] = wu;
+ }
// Remember to kill "a".
tokill[n] = true;
}
@@ -2596,6 +2698,8 @@ namespace spot
// a | X(F(a) | c...) = Fa | X(c...)
// a | (Xa R b) = b W a
// a | (Xa M b) = b U a
+ // a | (b & X(b W a)) = b W a
+ // a | (b & X(b U a)) = b U a
if (!mo->is_X_free())
{
typedef Sgi::hash_set > fmap_t;
fset_t xfset; // XF(...)
fset_t xset; // X(...)
- fmap_t rmset; // (X...)R(...) or (X...)M(...)
+ fmap_t rmset; // (X...)R(...) or (X...)M(...) or
+ // b & X(b W ...) or b & X(b U ...)
unsigned s = res->size();
std::vector tokill(s);
@@ -2623,6 +2728,21 @@ namespace spot
continue;
}
+ // Now we are looking for
+ // - X(...)
+ // - b & X(b W ...)
+ // - b & X(b U ...)
+ if ((*res)[n]->is_X_free())
+ continue;
+
+ binop* barg = is_bXbWU((*res)[n]);
+ if (barg)
+ {
+ rmset[barg->second()].insert(n);
+ continue;
+ }
+
+
unop* uo = is_X((*res)[n]);
if (!uo)
continue;
@@ -2682,7 +2802,8 @@ namespace spot
--allofthem;
assert(allofthem != -1U);
// At the same time, check if "a" can also
- // be used to simplify "Xa R b" or "Xa M b".
+ // be used to simplify "Xa R b", "Xa M b".
+ // "b & X(b W a)", or "b & X(b U a)".
fmap_t::const_iterator gs = rmset.find(x);
if (gs == rmset.end())
continue;
@@ -2690,17 +2811,30 @@ namespace spot
std::set::const_iterator g;
for (g = s.begin(); g != s.end(); ++g)
{
- // a | (Xa R b) = b W a
- // a | (Xa M b) = b U a
unsigned pos = *g;
- binop* rm = down_cast((*res)[pos]);
- binop::type t =
- (rm->op() == binop::M) ? binop::U : binop::W;
- unop* xa = down_cast(rm->first());
- formula* a = xa->child()->clone();
- formula* b = rm->second()->clone();
- rm->destroy();
- (*res)[pos] = binop::instance(t, b, a);
+ binop* rm = is_binop((*res)[pos]);
+ if (rm)
+ {
+ // a | (Xa R b) = b W a
+ // a | (Xa M b) = b U a
+ binop::type t = (rm->op() == binop::M)
+ ? binop::U : binop::W;
+ unop* xa = down_cast(rm->first());
+ formula* a = xa->child()->clone();
+ formula* b = rm->second()->clone();
+ rm->destroy();
+ (*res)[pos] = binop::instance(t, b, a);
+ }
+ else
+ {
+ // a | (b & X(b W a)) = b W a
+ // a | (b & X(b U a)) = b U a
+ rm = is_bXbWU((*res)[pos]);
+ assert(rm);
+ rm->clone();
+ (*res)[pos]->destroy();
+ (*res)[pos] = rm;
+ }
// Remember to kill "a".
tokill[n] = true;
}