Commit 776564cb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Rertite a M (b | a) = b U a and a R (b | a) == b W a.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex: Document it.
parent a09ad6b4
......@@ -1322,7 +1322,8 @@ $b$ denotes a Boolean formula.
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
f \U (g \AND f) & \equiv g\M f & f \W (g \AND f) & \equiv g\R f \\
f \M (g \OR f) & \equiv g\U f & f \R (g \OR f) & \equiv g\W f
\end{align*}
Here are the basic rewriting rules for $n$-ary operators ($\AND$ and
......@@ -1618,23 +1619,19 @@ sometimes generalized to support operators such as $\M$ and $\W$.
The operators \samp{F}, \samp{G}, \samp{U}, \samp{R}, \samp{M}, and
\samp{W} can all be defined using only Boolean operators, \samp{X},
and one of \samp{U}, \samp{W}, \samp{R}, or \samp{M}. This property
is usually used to simplify proofs.
These equivalences can also help to understand the semantics of
section~\ref{sec:opltl:sem} if you are only familiar with some of the
operators.
is usually used to simplify proofs. These equivalences can also help
to understand the semantics of section~\ref{sec:opltl:sem} if you are
only familiar with some of the operators.
{\allowdisplaybreaks
\begin{align*}
\intertext{Equivalences using $\U$:}
\F f &\equiv \1\U f\\
\G f &\equiv \NOT\F\NOT f\equiv \NOT(\1\U\NOT f)\\
f\W g &\equiv (f\U g)\OR(\G f)\equiv (f\U g)\OR\NOT(\1\U\NOT f)\\
f\W g &\equiv (f\U g)\OR\G f\equiv (f\U g)\OR\NOT(\1\U\NOT f)\\
&\equiv f\U (g\OR \G f)\equiv f\U (g\OR\NOT(\1\U\NOT f))\\
f\M g &\equiv g \U (f\AND g)\\
f\R g &\equiv g \W (f\AND g) \equiv (g \U (f\AND g))\OR\NOT(\1\U\NOT g)\\
&\phantom{\equiv g \W (f\AND g)} \equiv g \U ((f\AND g)\OR\NOT(\1\U\NOT g))\\
&\phantom{{}\equiv g \W (f\AND g)} \equiv g \U ((f\AND g)\OR\NOT(\1\U\NOT g))\\
\intertext{Equivalences using $\W$:}
\F f &\equiv \NOT\G\NOT f\equiv \NOT((\NOT f)\W\0)\\
\G f &\equiv \0\R f \equiv f\W \0\\
......@@ -1645,13 +1642,15 @@ operators.
\F f &\equiv \NOT\G\NOT f\equiv \NOT (\0\R\NOT f)\\
\G f &\equiv \0 \R f \\
f\U g&\equiv (((\X g) \R f)\AND\F g)\OR g \equiv (((\X g) \R f)\AND(\NOT (\0\R\NOT g)))\OR g \\
f \W g&\equiv ((\X g)\R f)\OR g\\
f \W g&\equiv g\R(f\OR g)\\
&\equiv ((\X g)\R f)\OR g\\
f \M g&\equiv (f \R g)\AND\F f\equiv (f \R g)\AND\NOT (\0\R\NOT f)\\
&\equiv f \R (g\AND\F g)\equiv f \R (g\AND\NOT (\0\R\NOT f))\\
\intertext{Equivalences using $\M$:}
\F f &\equiv f\M\1\\
\G f &\equiv \NOT\F\NOT f \equiv \NOT((\NOT f)\M\1)\\
f\U g&\equiv ((\X g)\M f)\OR g \\
f\U g&\equiv g\M (f\OR g) \\
&\equiv ((\X g)\M f)\OR g \\
f \W g&\equiv (f\U g)\OR \G f \equiv ((\X g)\M f)\OR g\OR \NOT((\NOT f)\M\1)\\
f \R g&\equiv (f \M g)\OR\G g \equiv (f \M g)\OR \NOT((\NOT g)\M\1)
\end{align*}}
......@@ -1674,7 +1673,7 @@ to have trouble when the $\X$ operator is involved. For instance $(f
which looks like it should be reduced similarly to $f \U \X g$, will
be rewritten instead to $(f \W \X g) \AND \X\F g$, because $\X\F g
\equiv \F\X g$ is another rule that gets applied first during the
bottom up rewriting.
bottom-up rewriting.
\chapter{Syntactic Implications}\label{ann:syntimpl}
......
......@@ -202,6 +202,10 @@ for x in ../reduccmp ../reductaustr; do
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'
run 0 $x 'g R (f|g|h)' '(f|h) W g'
run 0 $x 'g M (f|g|h)' '(f|h) U g'
run 0 $x 'g U (f&g&h)' '(f&h) M g'
run 0 $x 'g W (f&g&h)' '(f&h) R g'
# Syntactic implication
run 0 $x '(a & b) R (a R c)' '(a & b)R c'
......
......@@ -2156,10 +2156,16 @@ namespace spot
// a R (b & c & F(a)) = a M (b & c)
// a M (b & c & F(a)) = a M (b & c)
// a M (b | a | c) == (b | c) U a
// a R (b | a | c) == (b | c) W a
if (b->kind() == formula::MultOp)
{
multop* fm2 = static_cast<multop*>(b);
if (fm2->op() == multop::And)
multop::type bt = fm2->op();
// a R (b & c & F(a)) = a M (b & c)
// a M (b & c & F(a)) = a M (b & c)
if (bt == multop::And)
{
int s = fm2->size();
for (int i = 0; i < s; ++i)
......@@ -2175,8 +2181,23 @@ namespace spot
return;
}
}
// a M (b | a | c) == (b | c) U a
// a R (b | a | c) == (b | c) W a
if (bt == multop::Or)
{
int s = fm2->size();
for (int i = 0; i < s; ++i)
{
if (fm2->nth(i) != a)
continue;
result_ = recurse_destroy(binop::instance
(op == binop::M ? binop::U : binop::W,
fm2->all_but(i), a));
b->destroy();
return;
}
}
}
// If b is Boolean:
// (Xc) R b = b & X(b W c)
// (Xc) M b = b & X(b U c)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment