From 0d9cc29b46e142ac0c31ce8da4fb6368c062a568 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 Jul 2019 10:59:36 +0200 Subject: [PATCH] tl: eight new simplification rules * NEWS, doc/tl/tl.tex: Document the rules. * spot/tl/simplify.cc: Implement them. * tests/core/reduccmp.test: Test them. * tests/core/det.test, tests/core/ltl2tgba2.test, tests/python/stutter-inv.ipynb, tests/core/385.test: Adjust. --- NEWS | 10 ++- doc/tl/tl.tex | 15 ++++ spot/tl/simplify.cc | 142 +++++++++++++++++++++++++++++++++ tests/core/385.test | 2 +- tests/core/det.test | 2 +- tests/core/ltl2tgba2.test | 2 +- tests/core/reduccmp.test | 25 +++++- tests/python/stutter-inv.ipynb | 24 +++--- 8 files changed, 203 insertions(+), 19 deletions(-) diff --git a/NEWS b/NEWS index f61998efc..b2fc91052 100644 --- a/NEWS +++ b/NEWS @@ -112,13 +112,21 @@ New in spot 2.7.5.dev (not yet released) - spot::relabel_apply() makes it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula. - - The LTL simplifier learned the following optional rules: + - The LTL simplifier learned the following 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") GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") + (f & g) R h = f R h if h implies g + (f & g) M h = f M h if h implies g + (f | g) W h = f W h if g implies h + (f | g) U h = f U h if g implies h + Gf | F(g & eventual) = f W (g & eventual) if !f implies g + Ff & G(g | universal) = f M (g | universal) if f implies !g + f U (g & eventual) = F(g & eventual) if !f implies g + f R (g | universal) = G(g | universal) if f implies !g - cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 094d75600..d8b7d9d24 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1857,6 +1857,7 @@ are counted as one. \text{if~} & f\simp h & & \text{~then~} & (f\U g) \U h & \equiv g \U h \\ \text{if~} & f\simp h & & \text{~then~} & (f\W g) \U h & \equiv g \U h \\ \text{if~} & g\simp h & & \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\OR g) \U h & \equiv f \U h \\ \text{if~} & (\NOT f)\simp g & & \text{~then~} & f\W g & \equiv \1 \\ \text{if~} & \flessg & & \text{~then~} & f\W g & \equiv f \\ \text{if~} & f\simp g & & \text{~then~} & f\W g & \equiv g \\ @@ -1868,6 +1869,7 @@ are counted as one. \text{if~} & f\simp h & & \text{~then~} & (f\W g) \W h & \equiv g \W h \\ \text{if~} & g\simp h & & \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ \text{if~} & g\simp h & & \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\OR g) \W h & \equiv f \W h \\ \text{if~} & \flessg & & \text{~then~} & f\R g & \equiv f \\ \text{if~} & g\simp f & & \text{~then~} & f\R g & \equiv g \\ \text{if~} & g\simp \NOT f & & \text{~then~} & f\R g & \equiv \G g \\ @@ -1879,6 +1881,7 @@ are counted as one. \text{if~} & h\simp f & & \text{~then~} & (f\M g) \R h & \equiv g \R h \\ \text{if~} & g\simp h & & \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ \text{if~} & g\simp h & & \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & h\simp g & & \text{~then~} & (f\AND g) \R h & \equiv f \R h \\ \text{if~} & \flessg & & \text{~then~} & f\M g & \equiv f \\ \text{if~} & g\simp f & & \text{~then~} & f\M g & \equiv g \\ \text{if~} & g\simp \NOT f & & \text{~then~} & f\M g & \equiv \0 \\ @@ -1888,6 +1891,7 @@ are counted as one. \text{if~} & h\simp f & & \text{~then~} & (f\M g) \M h & \equiv g \M h \\ \text{if~} & h\simp f & & \text{~then~} & (f\R g) \M h & \equiv g \M h \\ \text{if~} & g\simp h & & \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ +\text{if~} & h\simp g & & \text{~then~} & (f\AND g) \M h & \equiv f \M h \\ \end{alignat*} \endgroup @@ -1895,6 +1899,17 @@ Many of the above rules were collected from the literature~\cite{somenzi.00.cav,tauriainen.03.tr,babiak.12.tacas} and sometimes generalized to support operators such as $\M$ and $\W$. +The following rules mix implication-based checks with formulas that +are pure eventualities ($e$) or that are purely universal ($u$). + +\allowdisplaybreaks +\begin{alignat*}{3} +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f \U (g \AND e) & \equiv \F(g \AND e) \\ +\text{if~} & f\simp \NOT g & & \text{~then~} & f \R (g \OR u) & \equiv \G(g \OR e) \\ +\text{if~} & (\NOT f) \simp g & & \text{~then~} & \G(f) \OR \F(g \AND e) & \equiv f \W (g \AND e) \\ +\text{if~} & f \simp\NOT g & & \text{~then~} & \F(f) \AND \G(g \OR e) & \equiv f \M (g \OR e) \\ +\end{alignat*} + \appendix \chapter{Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$} \label{sec:ltl-equiv} diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index ef144e293..8fd449283 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -2160,6 +2160,31 @@ namespace spot // if c => b, then (a U c) U b = (a U c) | b if (a.is(op::U) && c_->implication(a[1], b)) return recurse(formula::Or({a, b})); + // if g => h, then (f|g) U h = f U h + if (a.is(op::Or)) + { + unsigned n = a.size(); + for (unsigned child = 0; child < n; ++child) + if (c_->implication(a[child], b)) + return recurse(formula::U(a.all_but(child), b)); + } + // a U (b & e) = F(b & e) if !b => a + if (b.is(op::And)) + for (formula c: b) + if (c.is_eventual()) + { + // We know there is one pure eventuality + // formula but we might have more. So lets + // extract everything else. + vec rest; + rest.reserve(c.size()); + for (formula cc: b) + if (!cc.is_eventual()) + rest.emplace_back(cc); + if (c_->implication_neg(formula::And(rest), a, false)) + return recurse(formula::F(b)); + break; + } break; case op::R: @@ -2198,6 +2223,31 @@ namespace spot return recurse(formula::R(ac, b)); } } + // if h => g, then (f&g) R h = f R h + if (a.is(op::And)) + { + unsigned n = a.size(); + for (unsigned child = 0; child < n; ++child) + if (c_->implication(b, a[child])) + return recurse(formula::R(a.all_but(child), b)); + } + // a R (b | u) = G(b | u) if b => !a + if (b.is(op::Or)) + for (formula c: b) + if (c.is_universal()) + { + // We know there is one purely universal + // formula but we might have more. So lets + // extract everything else. + vec rest; + rest.reserve(c.size()); + for (formula cc: b) + if (!cc.is_universal()) + rest.emplace_back(cc); + if (c_->implication_neg(formula::Or(rest), a, true)) + return recurse(formula::G(b)); + break; + } break; case op::W: @@ -2234,6 +2284,14 @@ namespace spot // if c => b, then (a U c) W b = (a U c) | b if (a.is(op::U, op::W) && c_->implication(a[1], b)) return recurse(formula::Or({a, b})); + // if g => h, then (f|g) W h = f M h + if (a.is(op::Or)) + { + unsigned n = a.size(); + for (unsigned child = 0; child < n; ++child) + if (c_->implication(a[child], b)) + return recurse(formula::W(a.all_but(child), b)); + } break; case op::M: @@ -2265,6 +2323,14 @@ namespace spot return recurse(formula::M(formula::And({a[0], a[1]}), b)); + // if h => g, then (f&g) M h = f M h + if (a.is(op::And)) + { + unsigned n = a.size(); + for (unsigned child = 0; child < n; ++child) + if (c_->implication(b, a[child])) + return recurse(formula::M(a.all_but(child), b)); + } break; default: @@ -2680,6 +2746,7 @@ namespace spot // F(a) & (a M b) = a M b // F(b) & (a W b) = a U b // F(b) & (a U b) = a U b + // F(c) & G(phi | e) = c M (phi | e) if c => !phi. typedef std::unordered_map fmap_t; fmap_t uwmap; // associates "b" to "a U b" or "a W b" fmap_t rmmap; // associates "a" to "a R b" or "a M b" @@ -2762,6 +2829,43 @@ namespace spot assert(j->second->is(op::M)); } } + if (opt_.synt_impl | opt_.containment_checks) + { + // if the input looks like o1|u1|u2|o2, + // return o1 | o2. The input must have at + // least on universal formula. + auto extract_not_un = + [&](formula f) { + if (f.is(op::Or)) + for (auto u: f) + if (u.is_universal()) + { + vec phi; + phi.reserve(f.size()); + for (auto uu: f) + if (!uu.is_universal()) + phi.push_back(uu); + return formula::Or(phi); + } + return formula(nullptr); + }; + + // F(c) & G(phi | e) = c M (phi | e) if c => !phi. + for (auto in_g = s.res_G->begin(); + in_g != s.res_G->end();) + { + if (formula phi = extract_not_un(*in_g)) + if (c_->implication_neg(phi, c, true)) + { + s.res_other->push_back(formula::M(c, + *in_g)); + in_g = s.res_G->erase(in_g); + superfluous = true; + continue; + } + ++in_g; + } + } if (superfluous) f = nullptr; } @@ -3273,6 +3377,7 @@ namespace spot // G(a) | (a W b) = a W b // G(b) | (a R b) = a R b. // G(b) | (a M b) = a R b. + // G(c) | F(phi & e) = c W (phi & e) if !c => phi. typedef std::unordered_map fmap_t; fmap_t uwmap; // associates "a" to "a U b" or "a W b" fmap_t rmmap; // associates "b" to "a R b" or "a M b" @@ -3355,6 +3460,43 @@ namespace spot assert(j->second->is(op::R)); } } + if (opt_.synt_impl | opt_.containment_checks) + { + // if the input looks like o1&e1&e2&o2, + // return o1 & o2. The input must have at + // least on eventual formula. + auto extract_not_ev = + [&](formula f) { + if (f.is(op::And)) + for (auto e: f) + if (e.is_eventual()) + { + vec phi; + phi.reserve(f.size()); + for (auto ee: f) + if (!ee.is_eventual()) + phi.push_back(ee); + return formula::And(phi); + } + return formula(nullptr); + }; + + // G(c) | F(phi & e) = c W (phi & e) if !c => phi. + for (auto in_f = s.res_F->begin(); + in_f != s.res_F->end();) + { + if (formula phi = extract_not_ev(*in_f)) + if (c_->implication_neg(c, phi, false)) + { + s.res_other->push_back(formula::W(c, + *in_f)); + in_f = s.res_F->erase(in_f); + superfluous = true; + continue; + } + ++in_f; + } + } if (superfluous) f = nullptr; } diff --git a/tests/core/385.test b/tests/core/385.test index a3ae9cecb..b680c071f 100755 --- a/tests/core/385.test +++ b/tests/core/385.test @@ -36,7 +36,7 @@ EOF # Some of the following are still not optimal. cat >expected <formulas <<'EOF' 1,5,X(((a & b) R (!a U !c)) R b) 1,8,XXG(Fa U Xb) 1,5,(!a M !b) W F!c -1,3,(b & Fa & GFc) R a +1,3,(b & GFc) R a 1,2,(a R (b W a)) W G(!a M (b | c)) 1,11,(Fa W b) R (!a | Fc) 1,6,X(G(!a M !b) | G(a | G!a)) diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 3c52536da..8bcf2bc71 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -77,7 +77,7 @@ dac-patterns,37, 4,56, 4,56, 4,56, 4,56 dac-patterns,38, 4,56, 4,56, 4,56, 4,56 dac-patterns,39, 4,112, 4,112, 4,112, 4,112 dac-patterns,40, 3,88, 3,88, 3,88, 3,88 -dac-patterns,41, 6,54, 6,54, 7,56, 7,56 +dac-patterns,41, 4,32, 4,32, 4,32, 4,32 dac-patterns,42, 6,96, 6,96, 6,96, 6,96 dac-patterns,43, 5,80, 5,80, 5,80, 5,80 dac-patterns,44, 10,300, 10,300, 13,372, 13,372 diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index bad739155..67ef7daaf 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -298,17 +298,36 @@ a W ((a&b) W c), a W c (a R b) M (c&a), b M (c&a) (a M b) M (c&a), b M (c&a) -(a R (b&c)) R (c), (a&b&c) R c -(a M (b&c)) R (c), (a&b&c) R c +(x M y) M y, x M y +(x R y) R y, x R y +(x & y) M y, x M y +(x & y) R y, x R y + +(a R (b&c)) R (c), (a&b) R c +(a M (b&c)) R (c), (a&b) R c # not reduced (a R (b&c)) M (c), (a R (b&c)) M (c) -(a M (b&c)) M (c), (a&b&c) M c +(a M (b&c)) M (c), (a&b) M c (a W (c&b)) W b, (a W (c&b)) | b (a U (c&b)) W b, (a U (c&b)) | b (a U (c&b)) U b, (a U (c&b)) | b # not reduced (a W (c&b)) U b, (a W (c&b)) U b +!x U (x & Fa), F(x & Fa) +!x R (x | Ga), G(x | Ga) +!x U ((x | c) & Fa & Fb), F((x | c) & Fa & Fb) +!x R ((x & c) | Ga | Gb), G((x & c) | Ga | Gb) + +G!f | F((f|g) & Fa & Fb), !f W ((f | g) & Fa & Fb) +F!f & G((f&g) | Ga | Gb), !f M ((f & g) | Ga | Gb) + +(x|b) W (x|a), b W (x|a) +(x|b) U (x|a), b U (x|a) + +!x U ((x | c) & Fa & Fb), F((x | c) & Fa & Fb) +!x R ((x & c) | Ga | Gb), G((x & c) | Ga | Gb) + # Eventuality and universality class reductions Fa M b, Fa & b GFa M b, GFa & b diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index d283decf5..8e86b117f 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f3f0> >" + " *' at 0x7fc090629840> >" ] }, "metadata": {}, @@ -603,7 +603,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c31c360> >" + " *' at 0x7fc090629db0> >" ] }, "metadata": {}, @@ -812,7 +812,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c31c360> >" + " *' at 0x7fc090629db0> >" ] }, "metadata": {}, @@ -964,7 +964,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f840> >" + " *' at 0x7fc0905b5960> >" ] }, "metadata": {}, @@ -1062,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f690> >" + " *' at 0x7fc0905b5840> >" ] }, "metadata": {}, @@ -1272,7 +1272,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f7e0> >" + " *' at 0x7fc0905c34e0> >" ] }, "metadata": {}, @@ -1401,7 +1401,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f780> >" + " *' at 0x7fc0905c3570> >" ] }, "metadata": {}, @@ -1532,7 +1532,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c29f810> >" + " *' at 0x7fc0905c3f90> >" ] }, "metadata": {}, @@ -1792,7 +1792,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c23bb10> >" + " *' at 0x7fc0905c3240> >" ] }, "metadata": {}, @@ -2106,7 +2106,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f691c23bb10> >" + " *' at 0x7fc0905c3240> >" ] }, "metadata": {}, @@ -2192,7 +2192,7 @@ "G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p 4 2 1\n", "G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (! 4 1 1\n", "G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3 3 0 1\n", - "G((p0 & XFp1) -> XF(p1 & Fp2)) 6 1 1\n", + "G((p0 & XFp1) -> XF(p1 & Fp2)) 4 0 1\n", "Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U ( 6 2 1\n", "G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & F 5 0 1\n", "G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> 10 2 1\n", @@ -2318,7 +2318,7 @@ { "data": { "text/plain": [ - "55.749128919860624" + "55.78947368421053" ] }, "execution_count": 31,