diff --git a/NEWS b/NEWS index 5884c2869aaee9b9f76bfc920e515d0188510537..0321826b10fbb89df1f03b632e0f1d379c67d442 100644 --- a/NEWS +++ b/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 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) Bugs fixed: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 6232463c0f9f560b305ce2c5b246d214da52b2c0..6db9c2ffe0c3cb040bd9137ee0e3df1905ad6485 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1451,11 +1451,13 @@ instead of $\equiv$, and they can be disabled by setting the 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 & \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) \\ - & & \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 \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\ + \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\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) \\ +\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\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*} \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) diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 89d3ab7aee981b046587873fd9856895b8881287..82e354796d9d0e777ffb238d5df7791d40ed359a 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -913,16 +913,21 @@ namespace spot if (opt_.event_univ && c.is_eventual()) return c; - auto g_in_f = [this](formula g, std::vector* to) + auto g_in_f = [this](formula g, std::vector* to, + std::vector* eventual = nullptr) { 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) to->push_back(e.is(op::X) ? e[0] : e); to->push_back (unop_multop(op::G, op::Or, std::move(*s2.res_other))); + if (eventual) + std::swap(*s2.res_Event, *eventual); } else { @@ -947,13 +952,37 @@ namespace spot if (c.is(op::X)) 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})) { - std::vector toadd; - g_in_f(c, &toadd); + std::vector toadd, eventual; + g_in_f(c, &toadd, + opt_.favor_event_univ ? &eventual : nullptr); formula res = unop_multop(op::F, op::Or, 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) return recurse(res); } @@ -1077,16 +1106,21 @@ namespace spot if (opt_.event_univ && c.is_universal()) return c; - auto f_in_g = [this](formula f, std::vector* to) + auto f_in_g = [this](formula f, std::vector* to, + std::vector* univ = nullptr) { 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) to->push_back(e.is(op::X) ? e[0] : e); to->push_back (unop_multop(op::F, op::And, std::move(*s2.res_other))); + if (univ) + std::swap(*s2.res_Univ, *univ); } else { @@ -1112,12 +1146,36 @@ namespace spot return recurse(unop_unop(op::X, op::G, c[0])); // G(F(a & Fb)) = G(Fa & Fb) + // G(F(a & Gb)) = GFa & FGb // !opt_.reduce_size_strictly if (c.is({op::F, op::And})) { - std::vector toadd; - f_in_g(c, &toadd); + std::vector toadd, univ; + f_in_g(c, &toadd, + opt_.reduce_size_strictly ? nullptr : &univ); formula res = unop_multop(op::G, op::And, 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) return recurse(res); } diff --git a/tests/core/degenscc.test b/tests/core/degenscc.test index 47abfc7174f57fab334bbbf3d5b7040ada9fb239..f50a58cac5584c4196be991272a1c6e5a655273d 100644 --- a/tests/core/degenscc.test +++ b/tests/core/degenscc.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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). # # This file is part of Spot, a model checking library. @@ -28,28 +28,34 @@ set -e # The following cases were found with # # % randltl -n -1 3 | ltl2tgba | autfilt --acc-sets=3.. | -# autfilt -B --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. +# autfilt -Bx'!degen-remscc' --stats='%C,%c,%M' | +# awk -F, '{ if ($1 < $2) { print$0; } }' cat >input < 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 # of some of these formulas. In that case, regenerate the list of test # formula using the command displayed above. diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 9c9e695bff50f883abed28d4ca78b09aac785a2a..650399bd0f09fcc59001869e3717c99841815a6e 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -365,22 +365,31 @@ diff output expected # The first four formulas appear in a NEWS entry for Spot 2.6 # The 5th one is from issue #267. # The 6th one is from issue #358. +# formula 7-12 are from issue #385. cat >formulas <. Issue #380. -ltl2tgba -Fformulas/1 --stats='%f, %s,%t' | - ltl2tgba -D -F-/1 --stats='%f,%>, %s,%t' | - perl -pi -e 's/$/\r/' | - ltl2tgba -B -F-/1 --stats='%f,%>, %s,%t' | - ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output +ltlfilt -Fformulas/1 --stats='%f,%f,%>' | +ltl2tgba -F-/2 --stats='%<,%<, %s,%t' | + ltl2tgba -D -F-/2 --stats='%<,%<,%>, %s,%t' | + perl -p -e 's/$/\r/' | + 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 --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index f53cd5c269fc009de5cf3a24560c469bd8725ad2..9db10e04b400267fbd1c9612e9b11841ae98d00a 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -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) 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, # this also check for an old bug in ltl2tgba_fm. {(c&!c)[->0..1]}!, 0