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

Rewrite F(a M b) as F(a & b), and G(a W b) as G(a | b).

Browse source 
* src/ltlvisit/simplify.cc: Implement these rules.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document them.
This commit is contained in:
Alexandre Duret-Lutz 2012-01-11 11:15:54 +01:00
parent 212c7ebdd7
commit 54d4a0a093
3 changed files with 65 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

11
doc/tl/tl.tex
View file

@ -1309,14 +1309,15 @@ These simplifications are enabled with
The following are simplification rules for unary operators (applied
from left to right, as usual):
\begin{align*}
\X\F\G f &\equiv \F\G f & \X\G\F f &\equiv \G\F f \\
\F(f\U g) &\equiv \F g & \F\X f &\equiv \X\F f \\
\G(f \R g) &\equiv \G g & \G\X f &\equiv \X\G f
\X\F\G f & \equiv \F\G f & \F\X f & \equiv \X\F f & \G\X f & \equiv \X\G f\\
\X\G\F f & \equiv \G\F f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
& & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g)
\end{align*}
\begin{align*}
\G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m))&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
\G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
\end{align*}
Note that the latter three rewriting rules for $\G$ have no dual:
Note that the latter rewriting rules for $\G$ has no dual:
rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as
suggested by~\citet{somenzi.00.cav}) goes against our goal of moving
the $\F$ operator in front of the formula. Conceptually, it is also

7
src/ltltest/reduccmp.test
View file

@ -1,4 +1,4 @@
#! /bin/sh
#! /bin/sh
# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
@ -166,6 +166,11 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'a R (!a M a)' '0'
run 0 $x 'a W (!a M a)' 'Ga'
run 0 $x 'F(a U b)' 'Fb'
run 0 $x 'F(a M b)' 'F(a & b)'
run 0 $x 'G(a R b)' 'Gb'
run 0 $x 'G(a W b)' 'G(a | b)'
# Syntactic implication
run 0 $x '(a & b) R (a R c)' '(a & b)R c'
run 0 $x 'a R ((a & b) R c)' '(a & b)R c'

51
src/ltlvisit/simplify.cc
View file

@ -736,6 +736,24 @@ namespace spot
return is_binop(f, binop::U);
}
binop*
is_M(formula* f)
{
return is_binop(f, binop::M);
}
binop*
is_R(formula* f)
{
return is_binop(f, binop::R);
}
binop*
is_W(formula* f)
{
return is_binop(f, binop::W);
}
formula*
unop_multop(unop::type uop, multop::type mop, multop::vec* v)
{
@ -1061,6 +1079,20 @@ namespace spot
return;
}
// F(a M b) = F(a & b)
bo = is_M(result_);
if (bo)
{
formula* r =
unop::instance(unop::F,
multop::instance(multop::And,
bo->first()->clone(),
bo->second()->clone()));
bo->destroy();
result_ = recurse_destroy(r);
return;
}
// FX(a) = XF(a)
{
unop* u = is_X(result_);
@ -1113,10 +1145,8 @@ namespace spot
{
// G(a R b) = G(b)
if (result_->kind() == formula::BinOp)
{
binop* bo = static_cast<binop*>(result_);
if (bo->op() == binop::R)
binop* bo = is_R(result_);
if (bo)
{
formula* r =
unop::instance(unop::G, bo->second()->clone());
@ -1124,6 +1154,19 @@ namespace spot
result_ = recurse_destroy(r);
return;
}
// G(a W b) = G(a | b)
bo = is_W(result_);
if (bo)
{
formula* r =
unop::instance(unop::G,
multop::instance(multop::Or,
bo->first()->clone(),
bo->second()->clone()));
bo->destroy();
result_ = recurse_destroy(r);
return;
}
// GX(a) = XG(a)