From 646c5170edf1e18234254d91bca9defa6b1266bf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 2 Sep 2017 09:30:26 +0200 Subject: [PATCH] simplify: some new simplification rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For #263, reported by Mikuláš Klokočka. G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2) F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2) * spot/tl/simplify.cc: Implement the rules. * doc/tl/tl.tex, NEWS: Document them. * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases. * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect smaller automata. * THANKS: Add Mikuláš. --- NEWS | 4 ++ THANKS | 1 + doc/tl/tl.tex | 4 ++ spot/tl/simplify.cc | 82 +++++++++++++++++++++++++++++++-------- tests/core/det.test | 2 +- tests/core/eventuniv.test | 7 +++- tests/core/ltl2tgba2.test | 4 +- tests/core/reduccmp.test | 5 +++ 8 files changed, 89 insertions(+), 20 deletions(-) diff --git a/NEWS b/NEWS index d52455021..45dda07fa 100644 --- a/NEWS +++ b/NEWS @@ -173,6 +173,10 @@ New in spot 2.3.5.dev (not yet released) more (this threshold can be changed, see -x relabel-bool=N in the spot-x(7) man page). + - The LTL simplification routines learned that an LTL formula like + G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd), + and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd). + - The new function spot::to_weak_alternating() is able to take an input automaton with generalized Büchi/co-Büchi acceptance and convert it to a weak alternating automaton. diff --git a/THANKS b/THANKS index b182df63f..7a4d7d938 100644 --- a/THANKS +++ b/THANKS @@ -26,6 +26,7 @@ Martin Dieguez Lodeiro Matthias Heizmann Michael Tautschnig Michael Weber +Mikuláš Klokočka Ming-Hsien Tsai Nikos Gorogiannis Reuben Rowe diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 62eab9f40..09eea55f8 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1682,6 +1682,10 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\ \end{align*} \begin{align*} + \G(f_1\AND\ldots\AND f_n \AND \X e_1 \AND \ldots \AND \X e_p)&\equiv \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_p) \\ + \G(f_1\AND\ldots\AND f_n \AND \F (g_1 \AND \ldots \AND g_p \AND \X e_1 \AND \X e_m))&\equiv \G(f_1\AND\ldots\AND f_n \AND \F(g_1 \AND \ldots \AND g_p) \AND e_1 \AND \ldots \AND e_m) \\ + \F(f_1\OR\ldots\OR f_n \OR \X u_1 \OR \ldots \OR \X u_p)&\equiv \F(f_1\OR\ldots\OR f_n \OR u_1 \OR \ldots \AND u_p) \\ + \F(f_1\OR\ldots\OR f_n \OR \G (g_1 \OR \ldots \OR g_p \OR \X u_1 \OR \X u_m))&\equiv \F(f_1\OR\ldots\AND f_n \OR \G(g_1 \OR \ldots \OR g_p) \OR u_1 \OR \ldots \OR u_m) \\ \G(f_1\OR\ldots\OR f_n \OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR q_1 \OR \ldots \OR q_p \\ \F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\ \G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\ diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 6732c36bc..4bd4c52a3 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -995,28 +995,52 @@ namespace spot return recurse(res); } // If u3 and u4 are universal formulae and h is not: - // F(f1 | f2 | Fu3 | u4 | FGg | Fh) - // = F(f1 | f2 | u3 | u4 | Gg | h) + // F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5 | G(f6 | Xu7 | u8)) + // = F(f1 | f2 | u3 | u4 | Gg | h | u5 | Gf6 | u7 | u8) // or - // F(f1 | f2 | Fu3 | u4 | FGg | Fh) - // = F(f1 | f2 | h) | F(u3 | u4 | Gg) + // F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5) + // = F(f1 | f2 | h) | F(u3 | u4 | Gg | u5 | Gf6 | u7 | u8) // depending on whether favor_event_univ is set. if (c.is(op::Or)) { - int w = mospliter::Strip_F; + int w = mospliter::Strip_F + | mospliter::Strip_X | mospliter::Split_G; if (opt_.favor_event_univ) w |= mospliter::Split_Univ; mospliter s(w, c, c_); s.res_other->insert(s.res_other->end(), s.res_F->begin(), s.res_F->end()); + for (formula f: *s.res_X) + if (f.is_universal()) + s.res_other->push_back(f); + else + s.res_other->push_back(formula::X(f)); + 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); + } formula res = unop_multop(op::F, op::Or, std::move(*s.res_other)); if (s.res_Univ) { - // Strip any F. + std::vector toadd; for (auto& g: *s.res_Univ) - if (g.is(op::F)) + // Strip any F or X + if (g.is(op::F, op::X)) g = g[0]; + s.res_Univ->insert(s.res_Univ->end(), + toadd.begin(), toadd.end()); formula fu = unop_multop(op::F, op::Or, std::move(*s.res_Univ)); res = formula::Or({res, fu}); @@ -1071,29 +1095,55 @@ namespace spot return recurse(res); } // If e3 and e4 are eventual formulae and h is not: - // G(f1 & f2 & Ge3 & e4 & GFg & Gh) - // = G(f1 & f2 & e3 & e4 & Fg & h) + // G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8)) + // = G(f1 & f2 & e3 & e4 & Fg & h & e5 & Ff6 & e7 & e8) // or - // G(f1 & f2 & Ge3 & e4 & GFg & Gh) - // = G(f1 & f2 & h) & G(e3 & e4 & Fg) + // G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8)) + // = G(f1 & f2 & h) & G(e3 & e4 & Fg & e5 & Ff6 & e7 & e8) // depending on whether favor_event_univ is set. else if (c.is(op::And)) { - int w = mospliter::Strip_G; + int w = mospliter::Strip_G | + mospliter::Strip_X | mospliter::Split_F; if (opt_.favor_event_univ) w |= mospliter::Split_Event; mospliter s(w, c, c_); s.res_other->insert(s.res_other->end(), s.res_G->begin(), s.res_G->end()); + for (formula f: *s.res_X) + if (f.is_eventual()) + s.res_other->push_back(f); + else + s.res_other->push_back(formula::X(f)); + 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); + } formula res = unop_multop(op::G, op::And, std::move(*s.res_other)); - if (s.res_Event) { - // Strip any G. + std::vector toadd; + // Strip any G or X for (auto& g: *s.res_Event) - if (g.is(op::G)) - g = g[0]; + if (g.is(op::G, op::X)) + { + g = g[0]; + } + s.res_Event->insert(s.res_Event->end(), + toadd.begin(), toadd.end()); formula ge = unop_multop(op::G, op::And, std::move(*s.res_Event)); diff --git a/tests/core/det.test b/tests/core/det.test index 20837504c..af634876e 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -51,7 +51,7 @@ cat >formulas <<'EOF' 1,2,Ga R Fb 1,3,G(a U (b | X((!a & !c) | (a & c)))) 1,5,XG((G!a & F!b) | (Fa & (a | Gb))) -1,10,(a U X!a) | XG(!b & XFc) +1,9,(a U X!a) | XG(!b & Fc) 1,4,X(G!a | GFa) 1,4,G(G!a | F!c | G!b) EOF diff --git a/tests/core/eventuniv.test b/tests/core/eventuniv.test index 91d15489d..223b811bc 100755 --- a/tests/core/eventuniv.test +++ b/tests/core/eventuniv.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +# Copyright (C) 2012, 2013, 2014, 2017 Laboratoire de Recherche et # Developpement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -41,6 +41,11 @@ G(Ga & GXFb & c & FGd & FGe & Fc), G(Fb & FG(d & e)) & G(a & c) Ga & Gb & GFd & FGe & FGf, G(Fd & FG(e & f)) & G(a & b) G(Ga & Gb & GFd & FGe) & FGf, G(Fd & FG(e & f)) & G(a & b) +G(a & XFb), Ga & GFb +G(a & XF(b & XFc & Fd)), Ga & G(Fb & Fc & Fd) +F(a | XGb), Fa | FGb +F(a | XG(b | XGc | Gd)), Fa | F(Gb | Gc | Gd) + a U (b | Fc), (a U b) | Fc a W (b | Fc), (a W b) | Fc a U (b & GFc), (a U b) & GFc diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index c9bd08a22..f88e5dd73 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -100,7 +100,7 @@ eh-patterns,5, 4,32, 4,32, 4,32, 4,32 eh-patterns,6, 3,24, 3,24, 3,24, 3,24 eh-patterns,7, 3,14, 3,14, 4,18, 4,18 eh-patterns,8, 2,13, 2,13, 2,13, 2,13 -eh-patterns,9, 5,58, 5,58, 8,80, 8,80 +eh-patterns,9, 1,8, 1,8, 4,32, 4,32 eh-patterns,10, 1,32, 1,32, 6,192, 6,192 eh-patterns,11, 2,15, 2,15, 2,15, 2,15 eh-patterns,12, 4,60, 4,60, 4,60, 4,60 @@ -264,7 +264,7 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24 !eh-patterns,6, 2,12, 2,12, 2,12, 2,12 !eh-patterns,7, 2,7, 2,7, 3,9, 3,9 !eh-patterns,8, 3,21, 3,21, 3,21, 3,21 -!eh-patterns,9, 5,80, 5,80, 5,80, 5,80 +!eh-patterns,9, 5,68, 5,68, 5,68, 5,68 !eh-patterns,10, 6,192, 6,192, 6,192, 6,192 !eh-patterns,11, 2,9, 2,9, 2,9, 2,9 !eh-patterns,12, 6,103, 6,103, 8,135, 8,135 diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index 74308ecba..5572fa71e 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -300,6 +300,11 @@ a W ((a&b) W c), a W c Fa M b, Fa & b GFa M b, GFa & b +G(a & XFb), G(a & Fb) +G(a & XF(b & XFc & Fd)), G(a & Fb & Fc & Fd) +F(a | XGb), F(a | Gb) +F(a | XG(b | XGc | Gd)), F(a | Gb | Gc | Gd) + Fa|Xb|GFc, Fa | X(b|GFc) Fa|GFc, F(a|GFc) FGa|GFc, F(Ga|GFc)