Commit 1a912089 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

More simplifications rules for M.

* src/ltlvisit/reduce.cc (reduce_visitor): Add the following
implication rewriting rules:
a M (b M c) = a M c if a implies b.
a M (b R c) = a M c if a implies b.
a R (b R c) = a R c if a implies b.
a R (b M c) = b M c if b implies a.
a M (b M c) = b M c if b implies a.
The latter rule was fixed from an incorrectly copied&pasted
rule for a M (b R c) = b R c if b implies a (this is wrong).
* src/ltltest/reduccmp.test: Add more tests.
parent 946f305f
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
More simplifications rules for M.
* src/ltlvisit/reduce.cc (reduce_visitor): Add the following
implication rewriting rules:
a M (b M c) = a M c if a implies b.
a M (b R c) = a M c if a implies b.
a R (b R c) = a R c if a implies b.
a R (b M c) = b M c if b implies a.
a M (b M c) = b M c if b implies a.
The latter rule was fixed from an incorrectly copied&pasted
rule for a M (b R c) = b R c if b implies a (this is wrong).
Also remove the wrong rule for a W (b U c) = b U c if a implies b.
* src/ltltest/reduccmp.test: Add more tests.
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speed up syntactic_implication() for constants.
......
......@@ -143,6 +143,16 @@ for x in ../reduccmp ../reductaustr; do
;;
esac
# 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'
run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
run 0 $x '(a & b) M (a R c)' '(a & b)M c'
run 0 $x '(a & b) M (a M c)' '(a & b)M c'
run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
# Eventuality and universality class reduction
run 0 $x 'FFa' 'Fa'
run 0 $x 'FGFa' 'GFa'
......
......@@ -201,9 +201,10 @@ namespace spot
return;
}
/* b < a => a R (b R c) = b R c */
/* b < a => a R (b M c) = b M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::R
if (bo && (bo->op() == binop::R || bo->op() == binop::M)
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
......@@ -211,6 +212,18 @@ namespace spot
return;
}
}
/* a < b => a R (b R c) = a R c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::R
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::R, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
case binop::W:
......@@ -229,11 +242,10 @@ namespace spot
f2->destroy();
return;
}
/* a < b => a W (b U c) = (b U c) */
/* a < b => a W (b W c) = (b W c) */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && (bo->op() == binop::U || bo->op() == binop::W)
if (bo && bo->op() == binop::W
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
......@@ -259,10 +271,10 @@ namespace spot
f2->destroy();
return;
}
/* b < a => a R (b R c) = b R c */
/* b < a => a M (b M c) = b M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::R
if (bo && bo->op() == binop::M
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
......@@ -270,6 +282,19 @@ namespace spot
return;
}
}
/* a < b => a M (b M c) = a M c */
/* a < b => a M (b R c) = a M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && (bo->op() == binop::M || bo->op() == binop::R)
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::M, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
}
}
......
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