tl: new simplification rules
Related to issue #385. * doc/tl/tl.tex, NEWS: Document the rules. * spot/tl/simplify.cc: Implement the rules. * tests/core/reduccmp.test, tests/core/ltl2tgba2.test: Add tests. * tests/core/degenscc.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
066133b829
commit
b726d78cbd
6 changed files with 129 additions and 36 deletions
6
NEWS
6
NEWS
|
|
@ -62,6 +62,12 @@ New in spot 2.7.4.dev (not yet released)
|
||||||
- spot::relabel_apply() make it easier to reverse the effect
|
- spot::relabel_apply() make it easier to reverse the effect
|
||||||
of spot::relabel() or spot::relabel_bse() on formula.
|
of spot::relabel() or spot::relabel_bse() on formula.
|
||||||
|
|
||||||
|
- The LTL simplifier learned the following optional rules:
|
||||||
|
F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ")
|
||||||
|
G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ")
|
||||||
|
F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
|
||||||
|
G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly")
|
||||||
|
|
||||||
New in spot 2.7.4 (2019-04-27)
|
New in spot 2.7.4 (2019-04-27)
|
||||||
|
|
||||||
Bugs fixed:
|
Bugs fixed:
|
||||||
|
|
|
||||||
|
|
@ -1451,11 +1451,13 @@ instead of $\equiv$, and they can be disabled by setting the
|
||||||
The following are simplification rules for unary operators (applied
|
The following are simplification rules for unary operators (applied
|
||||||
from left to right, as usual):
|
from left to right, as usual):
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
\X\F\G f & \equiv \F\G f & \F\X f & \equiv \X\F f & \G\X f & \equiv \X\G f \\
|
\X\F\G f & \equiv \F\G f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
|
||||||
\X\G\F f & \equiv \G\F f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
|
\X\G\F f & \equiv \G\F f & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\
|
||||||
& & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\
|
\F\X f & \equiv \X\F f & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\
|
||||||
& & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\
|
\G\X f & \equiv \X\G f & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\
|
||||||
& & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\
|
& & \F\G(f\OR\G g) & \equiv \F(\G f\OR\G g) & \G\F(f\AND\F g) & \equiv \G(\F f\AND\F g) \\
|
||||||
|
& & \F\G(f\AND\F g) & \equiV \F\G f\AND\G\F g & \G\F(f\AND\G g) & \equiV \G\F f\AND\F\G g \\
|
||||||
|
& & \F\G(f\OR\F g) & \equivEU \F\G f\OR\G\F g & \G\F(f\OR\G g) & \equivEU \G\F f\OR\F\G g
|
||||||
\end{align*}
|
\end{align*}
|
||||||
\begin{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)
|
||||||
|
|
|
||||||
|
|
@ -913,16 +913,21 @@ namespace spot
|
||||||
if (opt_.event_univ && c.is_eventual())
|
if (opt_.event_univ && c.is_eventual())
|
||||||
return c;
|
return c;
|
||||||
|
|
||||||
auto g_in_f = [this](formula g, std::vector<formula>* to)
|
auto g_in_f = [this](formula g, std::vector<formula>* to,
|
||||||
|
std::vector<formula>* eventual = nullptr)
|
||||||
{
|
{
|
||||||
if (g[0].is(op::Or))
|
if (g[0].is(op::Or))
|
||||||
{
|
{
|
||||||
mospliter s2(mospliter::Split_Univ, g[0], c_);
|
mospliter s2(mospliter::Split_Univ |
|
||||||
|
(eventual ? mospliter::Split_Event : 0),
|
||||||
|
g[0], c_);
|
||||||
for (formula e: *s2.res_Univ)
|
for (formula e: *s2.res_Univ)
|
||||||
to->push_back(e.is(op::X) ? e[0] : e);
|
to->push_back(e.is(op::X) ? e[0] : e);
|
||||||
to->push_back
|
to->push_back
|
||||||
(unop_multop(op::G, op::Or,
|
(unop_multop(op::G, op::Or,
|
||||||
std::move(*s2.res_other)));
|
std::move(*s2.res_other)));
|
||||||
|
if (eventual)
|
||||||
|
std::swap(*s2.res_Event, *eventual);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -947,13 +952,37 @@ namespace spot
|
||||||
if (c.is(op::X))
|
if (c.is(op::X))
|
||||||
return recurse(unop_unop(op::X, op::F, c[0]));
|
return recurse(unop_unop(op::X, op::F, c[0]));
|
||||||
|
|
||||||
// G(F(a & Fb)) = G(Fa & Fb)
|
// F(G(a | Gb)) = F(Ga | Gb)
|
||||||
|
// F(G(a | Fb)) = FGa | GFb // opt_.favor_event_univ
|
||||||
if (c.is({op::G, op::Or}))
|
if (c.is({op::G, op::Or}))
|
||||||
{
|
{
|
||||||
std::vector<formula> toadd;
|
std::vector<formula> toadd, eventual;
|
||||||
g_in_f(c, &toadd);
|
g_in_f(c, &toadd,
|
||||||
|
opt_.favor_event_univ ? &eventual : nullptr);
|
||||||
formula res = unop_multop(op::F, op::Or,
|
formula res = unop_multop(op::F, op::Or,
|
||||||
std::move(toadd));
|
std::move(toadd));
|
||||||
|
if (!eventual.empty())
|
||||||
|
{
|
||||||
|
formula ev = unop_multop(op::G, op::Or,
|
||||||
|
std::move(eventual));
|
||||||
|
res = formula::Or({res, ev});
|
||||||
|
}
|
||||||
|
if (res != f)
|
||||||
|
return recurse(res);
|
||||||
|
}
|
||||||
|
|
||||||
|
// F(G(a & Fb) = FGa & GFb // !opt_.reduce_size_strictly
|
||||||
|
if (c.is({op::G, op::And}) && !opt_.reduce_size_strictly)
|
||||||
|
{
|
||||||
|
mospliter s2(mospliter::Split_Event, c[0], c_);
|
||||||
|
for (formula& e: *s2.res_Event)
|
||||||
|
while (e.is(op::X))
|
||||||
|
e = e[0];
|
||||||
|
formula fg = unop_unop_multop(op::F, op::G, op::And,
|
||||||
|
std::move(*s2.res_other));
|
||||||
|
formula gf = unop_multop(op::G, op::And,
|
||||||
|
std::move(*s2.res_Event));
|
||||||
|
formula res = formula::And({fg, gf});
|
||||||
if (res != f)
|
if (res != f)
|
||||||
return recurse(res);
|
return recurse(res);
|
||||||
}
|
}
|
||||||
|
|
@ -1077,16 +1106,21 @@ namespace spot
|
||||||
if (opt_.event_univ && c.is_universal())
|
if (opt_.event_univ && c.is_universal())
|
||||||
return c;
|
return c;
|
||||||
|
|
||||||
auto f_in_g = [this](formula f, std::vector<formula>* to)
|
auto f_in_g = [this](formula f, std::vector<formula>* to,
|
||||||
|
std::vector<formula>* univ = nullptr)
|
||||||
{
|
{
|
||||||
if (f[0].is(op::And))
|
if (f[0].is(op::And))
|
||||||
{
|
{
|
||||||
mospliter s2(mospliter::Split_Event, f[0], c_);
|
mospliter s2(mospliter::Split_Event |
|
||||||
|
(univ ? mospliter::Split_Univ : 0),
|
||||||
|
f[0], c_);
|
||||||
for (formula e: *s2.res_Event)
|
for (formula e: *s2.res_Event)
|
||||||
to->push_back(e.is(op::X) ? e[0] : e);
|
to->push_back(e.is(op::X) ? e[0] : e);
|
||||||
to->push_back
|
to->push_back
|
||||||
(unop_multop(op::F, op::And,
|
(unop_multop(op::F, op::And,
|
||||||
std::move(*s2.res_other)));
|
std::move(*s2.res_other)));
|
||||||
|
if (univ)
|
||||||
|
std::swap(*s2.res_Univ, *univ);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -1112,12 +1146,36 @@ namespace spot
|
||||||
return recurse(unop_unop(op::X, op::G, c[0]));
|
return recurse(unop_unop(op::X, op::G, c[0]));
|
||||||
|
|
||||||
// G(F(a & Fb)) = G(Fa & Fb)
|
// G(F(a & Fb)) = G(Fa & Fb)
|
||||||
|
// G(F(a & Gb)) = GFa & FGb // !opt_.reduce_size_strictly
|
||||||
if (c.is({op::F, op::And}))
|
if (c.is({op::F, op::And}))
|
||||||
{
|
{
|
||||||
std::vector<formula> toadd;
|
std::vector<formula> toadd, univ;
|
||||||
f_in_g(c, &toadd);
|
f_in_g(c, &toadd,
|
||||||
|
opt_.reduce_size_strictly ? nullptr : &univ);
|
||||||
formula res = unop_multop(op::G, op::And,
|
formula res = unop_multop(op::G, op::And,
|
||||||
std::move(toadd));
|
std::move(toadd));
|
||||||
|
if (!univ.empty())
|
||||||
|
{
|
||||||
|
formula un = unop_multop(op::F, op::And,
|
||||||
|
std::move(univ));
|
||||||
|
res = formula::And({res, un});
|
||||||
|
}
|
||||||
|
if (res != f)
|
||||||
|
return recurse(res);
|
||||||
|
}
|
||||||
|
|
||||||
|
// G(F(a | Gb)) = GFa | FGb // opt_.favor_event_univ
|
||||||
|
if (c.is({op::F, op::Or}) && opt_.favor_event_univ)
|
||||||
|
{
|
||||||
|
mospliter s2(mospliter::Split_Univ, c[0], c_);
|
||||||
|
for (formula& u: *s2.res_Univ)
|
||||||
|
while (u.is(op::X))
|
||||||
|
u = u[0];
|
||||||
|
formula gf = unop_unop_multop(op::G, op::F, op::Or,
|
||||||
|
std::move(*s2.res_other));
|
||||||
|
formula fg = unop_multop(op::F, op::Or,
|
||||||
|
std::move(*s2.res_Univ));
|
||||||
|
formula res = formula::Or({gf, fg});
|
||||||
if (res != f)
|
if (res != f)
|
||||||
return recurse(res);
|
return recurse(res);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2017 Laboratoire de Recherche et Développement de
|
# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement de
|
||||||
# l'Epita (LRDE).
|
# l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -28,28 +28,34 @@ set -e
|
||||||
# The following cases were found with
|
# The following cases were found with
|
||||||
#
|
#
|
||||||
# % randltl -n -1 3 | ltl2tgba | autfilt --acc-sets=3.. |
|
# % randltl -n -1 3 | ltl2tgba | autfilt --acc-sets=3.. |
|
||||||
# autfilt -B --stats='%C,%c,%M' | awk -F, '{ if ($1 < $2) { print $0; } }'
|
# autfilt -Bx'!degen-remscc' --stats='%C,%c,%M' |
|
||||||
#
|
# awk -F, '{ if ($1 < $2) { print $0; } }'
|
||||||
# before patching degeneralize, but today replacing -B by -Bx'!degen-remscc'
|
|
||||||
# should do the same.
|
|
||||||
cat >input <<EOF
|
cat >input <<EOF
|
||||||
p2 & GF(G(p0 & !p1) | (F!p0 & Fp1))
|
|
||||||
GF((Fp2 & X((p0 & Gp1) | (!p0 & F!p1))) | (G!p2 & X((p0 & F!p1) | (!p0 & Gp1))))
|
GF((Fp2 & X((p0 & Gp1) | (!p0 & F!p1))) | (G!p2 & X((p0 & F!p1) | (!p0 & Gp1))))
|
||||||
GF(p0 | GF((p2 M p1) | (Fp1 & F!p0) | G(p0 & !p1)))
|
|
||||||
((Gp2&FG((Gp1&Xp0)|(F!p1&X!p0)))|(F!p2 & GF((Gp1 & X!p0) | (Xp0 & F!p1)))) W !p0
|
((Gp2&FG((Gp1&Xp0)|(F!p1&X!p0)))|(F!p2 & GF((Gp1 & X!p0) | (Xp0 & F!p1)))) W !p0
|
||||||
|
G(Fp0 & (F!p1 U (G!p2 M !p0)))
|
||||||
G(((Fp1 & (p1 W Fp0)) | (G!p1 & (!p1 M G!p0))) M FG!p2)
|
G(((Fp1 & (p1 W Fp0)) | (G!p1 & (!p1 M G!p0))) M FG!p2)
|
||||||
Xp0 R F((p0 & FG(Gp2 U p1)) | (!p0 & GF(F!p2 R !p1)))
|
Xp0 R F((p0 & FG(Gp2 U p1)) | (!p0 & GF(F!p2 R !p1)))
|
||||||
GF(p0 & (((p1 & Fp2) | (!p1 & G!p2)) M Gp1))
|
GF(p0 & (((p1 & Fp2) | (!p1 & G!p2)) M Gp1))
|
||||||
|
F(G!p0 | GF((Gp0 & (!p2 R !p1)) | ((p2 U p1) & F!p0)))
|
||||||
|
p1|X(p1 R F((((p2&G!p0)|(!p2&Fp0))&FGp0)|(((p2 & Fp0) | (!p2 & G!p0)) & GF!p0)))
|
||||||
G(!p1 | (!p2 & F!p1) | (GFp2 U p0))
|
G(!p1 | (!p2 & F!p1) | (GFp2 U p0))
|
||||||
X(p1 | GF((Fp2 & F!p1) | G(p1 & !p2)))
|
GF((Fp2&(p0 U((p1&GFp0)|(!p1&FG!p0))))|(G!p2&(!p0 R((p1&FG!p0)|(!p1&GFp0)))))
|
||||||
|
GF((XFp1 & ((p0 & G!p2) | (!p0 & Fp2))) | (XG!p1 & ((p0 & Fp2) | (!p0 & G!p2))))
|
||||||
|
F(!p2 | GF((Fp0 & ((p0 & Gp1)|(!p0&F!p1)))|(G!p0&((p0&F!p1)|(!p0&Gp1)))))
|
||||||
|
G(XF((p2 & F!p1) | (!p2 & Gp1)) | (p1 & Fp0))
|
||||||
|
!p0 | GF((p1 & (Xp2 W Gp2)) | (!p1 & (X!p2 M F!p2)))
|
||||||
|
G!p0 | G((Fp1 U p2) & F!p2)
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
# We want to make sure the degeneralized automaton as less SCCs
|
|
||||||
|
|
||||||
|
# We want to make sure the degeneralized automaton has fewer SCCs
|
||||||
# (it can be less if the simulation on the BA is lukier than on the TGBA)
|
# (it can be less if the simulation on the BA is lukier than on the TGBA)
|
||||||
ltl2tgba < input | autfilt -B --stats=": '%M'; test %C -ge %c" > test.sh
|
ltl2tgba < input | autfilt -B --stats=": '%M'; test %C -ge %c" > test.sh
|
||||||
sh -x -e test.sh
|
sh -x -e test.sh
|
||||||
|
|
||||||
# Make sur that this degen-remscc optimizition is actually doing something.
|
# Make sure that this degen-remscc optimizition is actually doing something.
|
||||||
# The following test could fail in the future if we improve the translation
|
# The following test could fail in the future if we improve the translation
|
||||||
# of some of these formulas. In that case, regenerate the list of test
|
# of some of these formulas. In that case, regenerate the list of test
|
||||||
# formula using the command displayed above.
|
# formula using the command displayed above.
|
||||||
|
|
|
||||||
|
|
@ -365,22 +365,31 @@ diff output expected
|
||||||
# The first four formulas appear in a NEWS entry for Spot 2.6
|
# The first four formulas appear in a NEWS entry for Spot 2.6
|
||||||
# The 5th one is from issue #267.
|
# The 5th one is from issue #267.
|
||||||
# The 6th one is from issue #358.
|
# The 6th one is from issue #358.
|
||||||
|
# formula 7-12 are from issue #385.
|
||||||
cat >formulas <<EOF
|
cat >formulas <<EOF
|
||||||
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14
|
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14, 4,8
|
||||||
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30
|
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30, 8,16
|
||||||
GF(((a & Xb) | XXc) & Xd), 4,64, 4,64, 5,80, 5,80
|
GF(((a & Xb) | XXc) & Xd), 4,64, 4,64, 5,80, 5,80, 4,64
|
||||||
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12
|
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12, 2,4
|
||||||
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8
|
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8, 3,6
|
||||||
G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0
|
G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0, 1,0
|
||||||
|
FG(a | Fb), 3,15, 3,15, 3,15, 3,15, 1,4
|
||||||
|
FG(a & Fb), 2,7, 2,7, 3,9, 3,9, 1,4
|
||||||
|
GF(a & Gb), 2,7, 2,7, 3,9, 3,9, 1,4
|
||||||
|
GF(a | Gb), 2,7, 2,7, 3,12, 3,12, 1,4
|
||||||
|
Ge | GF(Ge & X(c & Fd)), 4,31, 4,31, 6,39, 6,39, 2,16
|
||||||
|
F(GF(b & Gc) | Ge), 3,22, 3,22, 4,26, 4,26, 1,8
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
# Call perl in the middle of all this to make sure
|
# Call perl in the middle of all this to make sure
|
||||||
# \r is removed fom %>. Issue #380.
|
# \r is removed fom %>. Issue #380.
|
||||||
ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
|
ltlfilt -Fformulas/1 --stats='%f,%f,%>' |
|
||||||
ltl2tgba -D -F-/1 --stats='%f,%>, %s,%t' |
|
ltl2tgba -F-/2 --stats='%<,%<, %s,%t' |
|
||||||
perl -pi -e 's/$/\r/' |
|
ltl2tgba -D -F-/2 --stats='%<,%<,%>, %s,%t' |
|
||||||
ltl2tgba -B -F-/1 --stats='%f,%>, %s,%t' |
|
perl -p -e 's/$/\r/' |
|
||||||
ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output
|
ltl2tgba -B -F-/2 --stats='%<,%<,%>, %s,%t' |
|
||||||
|
ltl2tgba -BD -F-/2 --stats='%<,%<,%>, %s,%t' |
|
||||||
|
ltl2tgba -GD -F-/2 --stats='%<,%>, %s,%t' > output
|
||||||
|
|
||||||
diff formulas output
|
diff formulas output
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -335,6 +335,18 @@ Xa&Xb&GFc&GFd&Ge, X(a&b&G(Fc&Fd))&Ge
|
||||||
GFc|GFd|FGe|FGf, F(GF(c|d)|Ge|Gf)
|
GFc|GFd|FGe|FGf, F(GF(c|d)|Ge|Gf)
|
||||||
G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
|
G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
|
||||||
|
|
||||||
|
F(G(a | Gb)), F(Ga | Gb)
|
||||||
|
G(F(a & Fb)), G(Fa & Fb)
|
||||||
|
# These two are not reduced by default
|
||||||
|
F(G(a | Fb)), F(G(a | Fb))
|
||||||
|
G(F(a | Gb)), G(F(a | Gb))
|
||||||
|
|
||||||
|
# issue #385
|
||||||
|
F(G(a & Fb)), G(Fb & FGa)
|
||||||
|
G(F(a & Gb)), G(Fa & FGb)
|
||||||
|
Ge | XGF(Ge & X(c & Fd)), Ge | G(Fd & FGe & Fc)
|
||||||
|
G!GXXe -> GF(b & c & Gc), F(G(Fb & FGc) | Ge)
|
||||||
|
|
||||||
# Because reduccmp will translate the formula,
|
# Because reduccmp will translate the formula,
|
||||||
# this also check for an old bug in ltl2tgba_fm.
|
# this also check for an old bug in ltl2tgba_fm.
|
||||||
{(c&!c)[->0..1]}!, 0
|
{(c&!c)[->0..1]}!, 0
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue