From 6cd6802acec5511178c15727b14dbbc5e80ffeb9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 2 Sep 2017 19:54:07 +0200 Subject: [PATCH] simplify: rewrite GF(a & Fb) as G(Fa & Fb) This addresses part of #35, and is just a generalization of the rules from 646c5170 for #263 (hence, no new documentation). * spot/tl/simplify.cc: Implement this. * tests/core/reduccmp.test: Add test cases. * tests/core/stutter-tgba.test: Adjust to expect smaller automata. --- spot/tl/simplify.cc | 84 +++++++++++++++++++++++++----------- tests/core/reduccmp.test | 2 + tests/core/stutter-tgba.test | 6 +-- 3 files changed, 64 insertions(+), 28 deletions(-) diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 783a1a48c..e06c44411 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -910,6 +910,23 @@ namespace spot if (opt_.event_univ && c.is_eventual()) return c; + auto g_in_f = [this](formula g, std::vector* to) + { + if (g[0].is(op::Or)) + { + mospliter s2(mospliter::Split_Univ, 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))); + } + else + { + to->push_back(g); + } + }; + if (opt_.reduce_basics) { // F(a U b) = F(b) @@ -927,6 +944,17 @@ namespace spot if (c.is(op::X)) return recurse(unop_unop(op::X, op::F, c[0])); + // G(F(a & Fb)) = G(Fa & Fb) + if (c.is({op::G, op::Or})) + { + std::vector toadd; + g_in_f(c, &toadd); + formula res = unop_multop(op::F, op::Or, + std::move(toadd)); + if (res != f) + return recurse(res); + } + // FG(a & Xb) = FG(a & b) // FG(a & Gb) = FG(a & b) if (c.is({op::G, op::And})) @@ -1018,18 +1046,7 @@ namespace spot std::vector* to = opt_.favor_event_univ ? s.res_Univ.get() : s.res_other.get(); for (formula g: *s.res_G) - if (g[0].is(op::Or)) - { - mospliter s2(mospliter::Split_Univ, g[0], c_); - for (formula u: *s2.res_Univ) - to->push_back(u.is(op::X) ? u[0] : u); - to->push_back(unop_multop(op::G, op::Or, - std::move(*s2.res_other))); - } - else - { - to->push_back(g); - } + g_in_f(g, to); formula res = unop_multop(op::F, op::Or, std::move(*s.res_other)); if (s.res_Univ) @@ -1057,6 +1074,23 @@ namespace spot if (opt_.event_univ && c.is_universal()) return c; + auto f_in_g = [this](formula f, std::vector* to) + { + if (f[0].is(op::And)) + { + mospliter s2(mospliter::Split_Event, 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))); + } + else + { + to->push_back(f); + } + }; + if (opt_.reduce_basics) { // G(a R b) = G(b) @@ -1074,6 +1108,17 @@ namespace spot if (c.is(op::X)) return recurse(unop_unop(op::X, op::G, c[0])); + // G(F(a & Fb)) = G(Fa & Fb) + if (c.is({op::F, op::And})) + { + std::vector toadd; + f_in_g(c, &toadd); + formula res = unop_multop(op::G, op::And, + std::move(toadd)); + if (res != f) + return recurse(res); + } + // G(f1|f2|GF(f3)|GF(f4)|f5|f6) = // G(f1|f2) | GF(f3|f4) | f5 | f6 // if f5 and f6 are both eventual and universal. @@ -1118,19 +1163,8 @@ namespace spot std::vector* to = opt_.favor_event_univ ? s.res_Event.get() : s.res_other.get(); for (formula f: *s.res_F) - if (f[0].is(op::And)) - { - mospliter s2(mospliter::Split_Event, 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))); - } - else - { - to->push_back(f); - } + f_in_g(f, to); + formula res = unop_multop(op::G, op::And, std::move(*s.res_other)); if (s.res_Event) diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index 42e62a3fe..66e5b185c 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -302,8 +302,10 @@ GFa M b, GFa & b G(a & XFb), G(a & Fb) G(a & XF(b & XFc & Fd)), G(a & Fb & Fc & Fd) +GF(a & XF(b & Fc)), G(Fa & Fb & Fc) F(a | XGb), F(a | Gb) F(a | XG(b | XGc | Gd)), F(a | Gb | Gc | Gd) +FG(a | XG(b | Gc)), F(Ga | Gb | Gc) Fa|Xb|GFc, Fa | X(b|GFc) Fa|GFc, F(a|GFc) diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test index 4cd1ed508..9967d2f21 100755 --- a/tests/core/stutter-tgba.test +++ b/tests/core/stutter-tgba.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2014-2017 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -29,13 +29,13 @@ $ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa $ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa $autfilt pos.hoa --product neg.hoa -H > prod.hoa $autfilt --is-empty prod.hoa -q && exit 1 -$autfilt --states=10 prod.hoa -q +$autfilt --states=7 prod.hoa -q $ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa $ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa $autfilt pos.hoa --product neg.hoa -H > prod.hoa $autfilt --is-empty prod.hoa -q && exit 1 -$autfilt --states=12 prod.hoa -q +$autfilt --states=9 prod.hoa -q # Check for issue #7.