alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Reduce 'a|(b&X(b U a))' to 'b U a', plus three simular rules.

Browse source 
* src/ltlast/multop.hh, src/ltlast/multop.cc (all_but): New method
used to simplify the removal of one element of a multop.
* src/ltlvisit/simplify.cc: Implement the new rewriting rules.
* doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Test them.
This commit is contained in:
Alexandre Duret-Lutz 2012-02-13 19:14:33 +01:00
parent bb56c26d1c
commit 955fc041ca
5 changed files with 209 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/tl/tl.tex
View file

@ -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

17
src/ltlast/multop.cc
View file

@ -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
{

19
src/ltlast/multop.hh
View file

@ -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<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> 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 <code>a|b|c|d</code> and <code>d</code>
/// is child number 2, then calling <code>f->all_but(2)</code> will
/// return a new formula <code>a|b|d</code>.
formula* all_but(unsigned n) const;
/// Get the type of this operator.
type op() const;
/// Get the type of this operator, as a string.

4
src/ltltest/reduccmp.test
View file

@ -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'

212
src/ltlvisit/simplify.cc
View file

@ -672,6 +672,15 @@ namespace spot
return static_cast<constant*>(f);
}
unop*
is_unop(formula* f)
{
if (f->kind() != formula::UnOp)
return 0;
return static_cast<unop*>(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<binop*>(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<binop*>(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<binop*>(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<binop*>(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<unop*>, only faster.
unop* fu1 =
(a->kind() == formula::UnOp) ? static_cast<unop*>(a) : 0;
unop* fu2 =
(b->kind() == formula::UnOp) ? static_cast<unop*>(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_set<formula*,
@ -1970,6 +2045,20 @@ namespace spot
continue;
}
// Now we are looking for
// - X(...)
// - b | X(b R ...)
// - b | X(b M ...)
if ((*res)[n]->is_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<unsigned>::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<binop*>((*res)[pos]);
binop::type t = (wu->op() == binop::U)
? binop::M : binop::R;
unop* xa = down_cast<unop*>(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<unop*>(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<formula*,
@ -2604,7 +2708,8 @@ namespace spot
ptr_hash<formula> > 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<bool> 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<unsigned>::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<binop*>((*res)[pos]);
binop::type t =
(rm->op() == binop::M) ? binop::U : binop::W;
unop* xa = down_cast<unop*>(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<unop*>(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;
}