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

Rewrite "a U (a&b)" as "b M a", and "a W (a&b)" as "b R a".

Browse source 
* src/ltlvisit/simplify.cc (simplify_visitor): Implement these
rules.
* doc/tl/tl.tex: Document these rules.
This commit is contained in:
Alexandre Duret-Lutz 2012-01-05 13:13:32 +01:00
parent 55a1c6c12f
commit c2ab4e781b
2 changed files with 41 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

17
doc/tl/tl.tex
View file

@ -1326,14 +1326,15 @@ verified, there is no need to worry about the $\G\F g$ term.
Here are the basic rewriting rules for binary operators (excluding $\OR$ and
$\AND$ which are considered in Spot as $n$-ary operators):
\begin{align*}
\1 \U f &\equiv \F f & f \W \0 &\equiv \G f \\
f \M \1 &\equiv \F f & \0 \R f &\equiv \G f \\
(\X f)\U (\X g) &\equiv \X(f\U g) & (\X f)\W(\X g) &\equiv \X(f\W g) \\
(\X f)\M (\X g) &\equiv \X(f\M g) & (\X f)\R(\X g) &\equiv \X(f\R g) \\
f \U(\G f) &\equiv \G f & f \W(\G f) &\equiv \G f \\
f \M(\F f) &\equiv \F f & f \R(\F f) &\equiv \F f \\
f \U (g \OR \G(f)) &\equiv f\W g & f \W (g \OR \G(f)) &\equiv f\W g\\
f \M (g \AND \F(f)) &\equiv f\M g & f \R (g \AND \F(f)) &\equiv f\M g
\1 \U f & \equiv \F f & f \W \0 & \equiv \G f \\
f \M \1 & \equiv \F f & \0 \R f & \equiv \G f \\
(\X f)\U (\X g) & \equiv \X(f\U g) & (\X f)\W(\X g) & \equiv \X(f\W g) \\
(\X f)\M (\X g) & \equiv \X(f\M g) & (\X f)\R(\X g) & \equiv \X(f\R g) \\
f \U(\G f) & \equiv \G f & f \W(\G f) & \equiv \G f \\
f \M(\F f) & \equiv \F f & f \R(\F f) & \equiv \F f \\
f \U (g \OR \G(f)) & \equiv f\W g & f \W (g \OR \G(f)) & \equiv f\W g \\
f \M (g \AND \F(f)) & \equiv f\M g & f \R (g \AND \F(f)) & \equiv f\M g \\
f \U (g \AND f) & \equiv g\M f & f \W (g \AND f) & \equiv g\R f
\end{align*}
Here are the basic rewriting rules for $n$-ary operators ($\AND$ and

35
src/ltlvisit/simplify.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -1509,10 +1509,15 @@ namespace spot
// a U (b | c | G(a)) = a W (b | c)
// a W (b | c | G(a)) = a W (b | c)
// a U (a & b & c) = (b & c) M a
// a W (a & b & c) = (b & c) R a
if (b->kind() == formula::MultOp)
{
multop* fm2 = static_cast<multop*>(b);
if (fm2->op() == multop::Or)
multop::type bt = fm2->op();
// a U (b | c | G(a)) = a W (b | c)
// a W (b | c | G(a)) = a W (b | c)
if (bt == multop::Or)
{
int s = fm2->size();
for (int i = 0; i < s; ++i)
@ -1538,6 +1543,30 @@ namespace spot
}
}
}
// a U (b & a & c) == (b & c) M a
// a W (b & a & c) == (b & c) R a
if (bt == multop::And)
{
int s = fm2->size();
for (int i = 0; i < s; ++i)
{
if (fm2->nth(i) != a)
continue;
multop::vec* v = new multop::vec;
v->reserve(s - 1);
int j;
for (j = 0; j < i; ++j)
v->push_back(fm2->nth(j)->clone());
// skip j=i
for (++j; j < s; ++j)
v->push_back(fm2->nth(j)->clone());
b->destroy();
result_ = recurse_destroy(binop::instance
(op == binop::U ? binop::M : binop::R,
multop::instance(multop::And, v), a));
return;
}
}
}
}
else if (op == binop::M || op == binop::R)