From 9caa9ad13450a2c26d8c55f81cce805b2eafba85 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Jun 2012 19:09:34 +0200 Subject: [PATCH] Implement a favor_even_univ option in the rewriting rules. The set of rules enabled by favor_even_univ try to "lift" the subformulae that are both eventual and universal, so they appear higher in the AST. This is contrary to what we used to do (and still do when the option is unset), were we try to postpone such subformulae (by moving them down the AST). It is still a bit experimental. * src/ltlvisit/simplify.hh: Add option favor_event_univ. * src/ltlvisit/simplify.cc: Implement new rewriting rules. * doc/tl/tl.tex: Document them. * src/tgbatest/ltl2tgba.cc: Add option -ra to enable them. * src/tgbatest/spotlbtt.test: Test the translation with this option. * src/ltltest/reduc.cc, src/ltltest/equals.cc: Add option to enable the new rules. * src/ltltest/eventuniv.test: New file to test them. * src/ltltest/Makefile.am: Add it. --- doc/tl/tl.tex | 48 +++-- src/ltltest/Makefile.am | 6 +- src/ltltest/equals.cc | 3 + src/ltltest/eventuniv.test | 60 ++++++ src/ltltest/reduc.cc | 7 + src/ltlvisit/simplify.cc | 376 ++++++++++++++++++++++++++++++++++--- src/ltlvisit/simplify.hh | 8 +- src/tgbatest/ltl2tgba.cc | 8 + src/tgbatest/spotlbtt.test | 16 ++ 9 files changed, 489 insertions(+), 43 deletions(-) create mode 100755 src/ltltest/eventuniv.test diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index c11702450..8947c9cfa 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -108,6 +108,9 @@ % rewriting rules that enlarge the formula \newcommand{\equiV}{\stackrel{\star}{\equiv}} +% rewriting rules that favors event/univ +\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}} +\newcommand{\equivNeu}{\stackrel{\smalltriangledown}{\equiv}} % marked rewriting rules \newcommand{\equivM}{\stackrel{\dag}{\equiv}} @@ -1298,6 +1301,13 @@ The goals in most of these simplification are to: limit the sources of indeterminism. \end{itemize} +Rewritings defined with $\equivEU$ are applied only when +\verb|ltl_simplifier_options::favor_event_univ|' is \texttt{true}: +they try to lift subformulas that are both eventual and universal +\emph{higher} in the syntax tree. Conversely, rules defined with $\equivNeu$ +are applied only when \verb|favor_event_univ|' is \texttt{false}: they +try to \textit{lower} subformulas that are both eventual and universal. + \subsection{Basic Simplifications}\label{sec:basic-simp} These simplifications are enabled with @@ -1356,10 +1366,10 @@ $\OR$): (\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g) \\ (\X f) \AND(\X g) &\equiv \X(f\AND g) & (\X f) \OR (\X g) &\equiv \X(f\OR g) \\ - (\X f) \AND(\F\G g) &\equiv \X(f\AND \F\G g) & - (\X f) \OR (\G\F g) &\equiv \X(f\OR \G\F g) \\ - (\G f) \AND(\G g) &\equiv \G(f\AND g) & - (\F f) \OR (\F g) &\equiv \F(f\OR g) \\ + (\X f) \AND(\F\G g) &\equivNeu \X(f\AND \F\G g) & + (\X f) \OR (\G\F g) &\equivNeu \X(f\OR \G\F g) \\ + (\G f) \AND(\G g) &\equivNeu \G(f\AND g) & + (\F f) \OR (\F g) &\equivNeu \F(f\OR g) \\ (f_1 \U f_2)\AND (f_3 \U f_2)&\equiv (f_1\AND f_3)\U f_2& (f_1 \U f_2)\OR (f_1 \U f_3)&\equiv f_1\U (f_2\OR f_3) \\ (f_1 \U f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\U f_2& @@ -1409,8 +1419,8 @@ $b \OR c\OR \X(\F(a\OR b\OR c)\OR \G d)$. Finally the following rule is applied only when no other terms are present in the OR arguments: \begin{align*} - \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m) - &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\ + \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g) + &\equivNeu \F(f_1\OR \ldots \OR f_n \OR \G\F(g)) \\ \end{align*} \subsubsection{Basic Simplifications for SERE Operators} @@ -1558,17 +1568,29 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\ \end{center} \begin{align*} - \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f & u_1 \M u_2 &\equiV (\F u_1) \AND u_2 \\ - \G u &\equiv u & f \R u &\equiv u & u \W f &\equiv u\OR f & e_1 \W e_2 &\equiV (\G e_1) \OR e_2 \\ - \X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f) + \F e & \equiv e & f \U e & \equiv e & e \M g & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\ + \F(u)\OR q & \equivEU \F(u\OR q) & f \U (g\OR e) & \equivEU (f \U g)\OR e & f\M (g\AND u) & \equivEU (f \M g)\AND u \\ + & & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\ + \G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\ + \G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\ + & & (f\OR u) \W g & \equivEU (f \W g)\OR u \\ + \X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\ + & & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\ \end{align*} + \begin{align*} - \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)\OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)\OR q_1 \OR \ldots q_p \\ + \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 \\ + \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_m \AND \G(e_{m+1}) \AND \ldots\AND \G(e_p))&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\ + \G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\ + \F(f_1 \OR \ldots \OR f_n \OR u_1 \OR \ldots \OR u_m \OR \F(u_{m+1})\OR\ldots\OR \F(u_p)) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\ + \F(f_1 \OR \ldots \OR f_n \OR \F(g_1) \OR \ldots \OR \G(g_m)) &\equiv \F(f_1\OR \ldots\OR f_n \OR g_1 \OR \ldots \OR g_m)\\ + \G(f_1)\AND\ldots\AND \G(f_n) \AND \G(e_1) \AND \ldots\AND \G(e_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\ + \F(f_1) \OR\ldots\OR \F(f_n) \OR \F(u_1)\OR\ldots\OR \F(u_p) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\ \intertext{Finally the following rule is applied only when no other terms are present in the OR arguments:} - \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m) - \OR q_1 \OR \ldots \OR q_p - &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots\OR g_m) \OR q_1\OR \ldots q_p) + \F(f_1) \OR \ldots \OR \F(f_n) \OR q_1 \OR \ldots \OR q_p &\equivNeu \F(f_1\OR \ldots \OR f_n \OR q_1\OR \ldots q_p) \end{align*} \subsection{Simplifications Based on Implications} diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index e985215bd..57b36b5f7 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -36,6 +36,7 @@ check_PROGRAMS = \ nenoform \ reduc \ reduccmp \ + reduceu \ reductau \ reductaustr \ syntimpl \ @@ -58,6 +59,8 @@ nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM reduc_SOURCES = reduc.cc reduccmp_SOURCES = equals.cc reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC +reduceu_SOURCES = equals.cc +reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV reductau_SOURCES = equals.cc reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU reductaustr_SOURCES = equals.cc @@ -99,7 +102,8 @@ TESTS = \ reduc0.test \ reducpsl.test \ reduccmp.test \ - uwrm.test + uwrm.test \ + eventuniv.test distclean-local: rm -rf $(TESTS:.test=.dir) diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 6387fa604..a9b5905f9 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -104,6 +104,9 @@ main(int argc, char** argv) #endif #ifdef REDUC spot::ltl::ltl_simplifier_options opt(true, true, true, false, false); +# ifdef EVENT_UNIV + opt.favor_event_univ = true; +# endif spot::ltl::ltl_simplifier simp(opt); { const spot::ltl::formula* tmp; diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test new file mode 100755 index 000000000..195322795 --- /dev/null +++ b/src/ltltest/eventuniv.test @@ -0,0 +1,60 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs || exit 1 + +check() +{ + run 0 ../reduceu "$@" +} + +check 'Xa | GFb' 'Xa | GFb' +check 'X(a | GXFb)' 'Xa | GFb' +check 'Xa & GFb' 'Xa & GFb' +check 'X(a & GXFb)' 'Xa & GFb' + +check 'F(a & b & GFc & FGd)' 'F(a & b) & G(Fc & FGd)' +check 'Fa | Fb | GFc | GFd' 'F(a|b) | GF(c | d)' +check 'Fa | Fb | GFc | GFd | FGe' 'F(a|b) | F(G(e) | GF(c | d))' +cehck 'Ga | Gb | GFd | FGe | FGf' 'Ga | Gb | F(GFd | Ge | Gf)' + +check 'G(Ga & Fb & c & GFd)' 'G(a&c) & G(Fb & Fd)' +check 'G(Ga & GFb & c & GFd)' 'G(a&c) & G(Fb & Fd)' +check 'G(a & GFb & c & GFd)' 'G(a&c) & G(Fb & Fd)' +check 'G(Ga & Fb & c & GFd & FGe)' 'G(a & c) & G(Fb & Fd & FGe)' +check 'G(Ga & XFGb & c & FGd & FGe)' 'FG(b & d & e) & G(a & c)' +check 'G(Ga & GXFb & c & FGd & FGe & Fc)' 'G(Fb & FG(d & e)) & G(a & c)' +check 'Ga & Gb & GFd & FGe & FGf' 'G(Fd & FG(e & f)) & G(a & b)' +check 'G(Ga & Gb & GFd & FGe) & FGf' 'G(Fd & FG(e & f)) & G(a & b)' + +check 'a U (b | Fc)' '(a U b) | Fc' +check 'a W (b | Fc)' '(a W b) | Fc' +check 'a U (b & GFc)' '(a U b) & GFc' +check 'a W (b & GFc)' 'a W (b & GFc)' # Unchanged +check '(a | Gc) W g' '(a W g) | Gc' +check '(a | Gc) U g' '(a | Gc) U g' # Unchanged + +check '(a & GFc) M b' '(a M b) & GFc' +check '(a | GFc) M b' '(a | GFc) M b' # Unchanged +check '(a & GFc) R b' '(a & GFc) R b' # Unchanged +check '(a | GFc) R b' '(a | GFc) R b' # Unchanged +check 'a R (b & Gc)' '(a R b) & Gc' +check 'a M (b & Gc)' '(a M b) & Gc' + diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 368c30b47..2456e6fc3 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -134,6 +134,13 @@ main(int argc, char** argv) o.containment_checks = true; o.containment_checks_stronger = true; break; + case 15: + o.reduce_basics = true; + o.event_univ = true; + o.containment_checks = true; + o.containment_checks_stronger = true; + o.favor_event_univ = true; + break; default: return 2; } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 873db091a..633346faf 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -129,6 +129,7 @@ namespace spot : dict(d), options(opt), lcc(d, true, true, false, false) { options.containment_checks |= options.containment_checks_stronger; + options.event_univ |= options.favor_event_univ; } void @@ -880,6 +881,9 @@ namespace spot void process(const formula* f) { + bool e = f->is_eventual(); + bool u = f->is_universal(); + bool eu = res_EventUniv && e & u && c_->options.favor_event_univ; switch (f->kind()) { case formula::UnOp: @@ -889,21 +893,21 @@ namespace spot switch (uo->op()) { case unop::X: - if (res_X) + if (res_X && !eu) { res_X->push_back(c->clone()); return; } break; case unop::F: - if (res_FG) + if (res_FG && u) if (const unop* cc = is_G(c)) { res_FG->push_back(((split_ & Strip_FG) == Strip_FG ? cc->child() : f)->clone()); return; } - if (res_F) + if (res_F && !eu) { res_F->push_back(((split_ & Strip_F) == Strip_F ? c : f)->clone()); @@ -911,14 +915,14 @@ namespace spot } break; case unop::G: - if (res_GF) + if (res_GF && e) if (const unop* cc = is_F(c)) { res_GF->push_back(((split_ & Strip_GF) == Strip_GF ? cc->child() : f)->clone()); return; } - if (res_G) + if (res_G && !eu) { res_G->push_back(((split_ & Strip_G) == Strip_G ? c : f)->clone()); @@ -966,8 +970,6 @@ namespace spot } if (c_->options.event_univ) { - bool e = f->is_eventual(); - bool u = f->is_universal(); if (res_EventUniv && e && u) { res_EventUniv->push_back(f->clone()); @@ -1154,12 +1156,28 @@ namespace spot && c_->lcc.equal(result_, uo)) return; - // Disabled: X(f1 & GF(f2)) = X(f1) & GF(f2) - // Disabled: X(f1 | GF(f2)) = X(f1) | GF(f2) - // Disabled: X(f1 & FG(f2)) = X(f1) & FG(f2) - // Disabled: X(f1 | FG(f2)) = X(f1) | FG(f2) - // The above make more sense when reversed, - // so see them in the And and Or rewritings. + // X(f1 & GF(f2)) = X(f1) & GF(f2) + // X(f1 | GF(f2)) = X(f1) | GF(f2) + // X(f1 & FG(f2)) = X(f1) & FG(f2) + // X(f1 | FG(f2)) = X(f1) | FG(f2) + // + // The above usually make more sense when reversed (see + // them in the And and Or rewritings), except when we + // try to maximaze the size of subformula that do not + // have EventUniv formulae. + if (opt_.favor_event_univ) + if (const multop* mo = is_multop(result_, + multop::Or, multop::And)) + { + mospliter s(mospliter::Split_EventUniv, mo, c_); + multop::type op = mo->op(); + s.res_EventUniv->push_back(unop_multop(unop::X, op, + s.res_other)); + result_ = multop::instance(op, s.res_EventUniv); + if (result_ != uo) + result_ = recurse_destroy(result_); + return; + } break; case unop::F: @@ -1259,7 +1277,8 @@ namespace spot && c_->lcc.contained(uo, result_)) return; - // Disabled: F(f1 & GF(f2)) = F(f1) & GF(f2) + // Disabled by default: + // F(f1 & GF(f2)) = F(f1) & GF(f2) // // As is, these two formulae are translated into // equivalent Büchi automata so the rewriting is @@ -1272,7 +1291,86 @@ namespace spot // rule which really helps the translation. F((f1 & // GF(f2)) | (a & GF(b))) is indeed easier to translate. // - // So let's not consider this rewriting rule. + // So we do not consider this rewriting rule by default. + // However if favor_event_univ is set, we want to move + // the GF out of the F. + if (opt_.favor_event_univ) + // F(f1&f2&FG(f3)&FG(f4)&f5&f6) = + // F(f1&f2) & FG(f3&f4) & f5 & f6 + // if f5 and f6 are both eventual and universal. + if (const multop* mo = is_And(result_)) + { + mo->clone(); + mospliter s(mospliter::Strip_FG | + mospliter::Split_EventUniv, + mo, c_); + s.res_EventUniv-> + push_back(unop_multop(unop::F, multop::And, + s.res_other)); + s.res_EventUniv-> + push_back(unop_unop_multop(unop::F, unop::G, + multop::And, s.res_FG)); + result_ = multop::instance(multop::And, s.res_EventUniv); + if (result_ != uo) + { + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + else + { + // Revert to the previous value of result_, + // for the next simplification. + result_->destroy(); + result_ = mo; + } + } + // 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) + // or + // F(f1 | f2 | Fu3 | u4 | FGg | Fh) + // = F(f1 | f2 | h) | F(u3 | u4 | Gg) + // depending on whether favor_event_univ is set. + if (const multop* mo = is_Or(result_)) + { + mo->clone(); + int w = mospliter::Strip_F; + if (opt_.favor_event_univ) + w |= mospliter::Split_Univ; + mospliter s(w, mo, c_); + s.res_other->insert(s.res_other->end(), + s.res_F->begin(), s.res_F->end()); + delete s.res_F; + result_ = unop_multop(unop::F, multop::Or, s.res_other); + if (s.res_Univ) + { + // Strip any F. + for (multop::vec::iterator i = s.res_Univ->begin(); + i != s.res_Univ->end(); ++i) + if (const unop* u = is_F(*i)) + { + *i = u->child()->clone(); + u->destroy(); + } + const formula* fu = + unop_multop(unop::F, multop::Or, s.res_Univ); + result_ = multop::instance(multop::Or, result_, fu); + } + if (result_ != uo) + { + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + else + { + // Revert to the previous value of result_, + // for the next simplification. + result_->destroy(); + result_ = mo; + } + } break; case unop::G: @@ -1356,6 +1454,52 @@ namespace spot result_ = mo; } } + // 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) + // or + // G(f1 & f2 & Ge3 & e4 & GFg & Gh) + // = G(f1 & f2 & h) & G(e3 & e4 & Fg) + // depending on whether favor_event_univ is set. + else if (const multop* mo = is_And(result_)) + { + mo->clone(); + int w = mospliter::Strip_G; + if (opt_.favor_event_univ) + w |= mospliter::Split_Event; + mospliter s(w, mo, c_); + s.res_other->insert(s.res_other->end(), + s.res_G->begin(), s.res_G->end()); + delete s.res_G; + result_ = unop_multop(unop::G, multop::And, s.res_other); + if (s.res_Event) + { + // Strip any G. + for (multop::vec::iterator i = s.res_Event->begin(); + i != s.res_Event->end(); ++i) + if (const unop* u = is_G(*i)) + { + *i = u->child()->clone(); + u->destroy(); + } + const formula* ge = + unop_multop(unop::G, multop::And, s.res_Event); + result_ = multop::instance(multop::And, result_, ge); + } + if (result_ != uo) + { + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + else + { + // Revert to the previous value of result_, + // for the next simplification. + result_->destroy(); + result_ = mo; + } + } // GF(a | Xb) = GF(a | b) // GF(a | Fb) = GF(a | b) @@ -1870,7 +2014,6 @@ namespace spot return; } - // e₁ W e₂ = Ge₁ | e₂ // u₁ M u₂ = Fu₁ & u₂ if (!opt_.reduce_size_strictly) @@ -1893,6 +2036,113 @@ namespace spot } } + // In the following rewritings we assume that + // - e is a pure eventuality + // - u is purely universal + // - q is purely universal pure eventuality + // (a U (b|e)) = (a U b)|e + // (a W (b|e)) = (a W b)|e + // (a U (b&q)) = (a U b)&q + // ((a&q) M b) = (a M b)&q + // ((a|u) W b) = u|(a W b) + // (a R (b&u)) = (a R b)&u + // (a M (b&u)) = (a M b)&u + if (opt_.favor_event_univ) + { + if (op == binop::U || op == binop::W) + if (const multop* mo = is_Or(b)) + { + b->clone(); + mospliter s(mospliter::Split_Event, mo, c_); + const formula* b2 = + multop::instance(multop::Or, s.res_other); + if (b2 != b) + { + b->destroy(); + s.res_Event->push_back(binop::instance(op, a, b2)); + result_ = + recurse_destroy(multop::instance(multop::Or, + s.res_Event)); + return; + } + b2->destroy(); + delete s.res_Event; + } + if (op == binop::W) + if (const multop* mo = is_Or(a)) + { + a->clone(); + mospliter s(mospliter::Split_Univ, mo, c_); + const formula* a2 = + multop::instance(multop::Or, s.res_other); + if (a2 != a) + { + a->destroy(); + s.res_Univ->push_back(binop::instance(op, a2, b)); + result_ = recurse_destroy + (multop::instance(multop::Or, s.res_Univ)); + return; + } + a2->destroy(); + delete s.res_Univ; + } + if (op == binop::U) + if (const multop* mo = is_And(b)) + { + b->clone(); + mospliter s(mospliter::Split_EventUniv, mo, c_); + const formula* b2 = + multop::instance(multop::And, s.res_other); + if (b2 != b) + { + b->destroy(); + s.res_EventUniv->push_back(binop::instance(op, + a, b2)); + result_ = recurse_destroy + (multop::instance(multop::And, s.res_EventUniv)); + return; + } + b2->destroy(); + delete s.res_Event; + } + if (op == binop::M) + if (const multop* mo = is_And(a)) + { + a->clone(); + mospliter s(mospliter::Split_EventUniv, mo, c_); + const formula* a2 = + multop::instance(multop::And, s.res_other); + if (a2 != a) + { + a->destroy(); + s.res_EventUniv->push_back(binop::instance(op, + a2, b)); + result_ = recurse_destroy + (multop::instance(multop::And, s.res_EventUniv)); + return; + } + a2->destroy(); + delete s.res_EventUniv; + } + if (op == binop::R || op == binop::M) + if (const multop* mo = is_And(b)) + { + b->clone(); + mospliter s(mospliter::Split_Univ, mo, c_); + const formula* b2 = + multop::instance(multop::And, s.res_other); + if (b2 != b) + { + b->destroy(); + s.res_Univ->push_back(binop::instance(op, a, b2)); + result_ = recurse_destroy + (multop::instance(multop::And, s.res_Univ)); + return; + } + b2->destroy(); + delete s.res_Univ; + } + } trace << "bo: no eventuniv rule matched" << std::endl; } @@ -2785,7 +3035,7 @@ namespace spot // Xa & Xb & FG(c) = X(a & b & FG(c)) // For Universal&Eventual formulae f1...fn we also have: // Xa & Xb & f1...fn = X(a & b & f1...fn) - if (!s.res_X->empty()) + if (!s.res_X->empty() && !opt_.favor_event_univ) { s.res_X->push_back(allFG); allFG = 0; @@ -2794,13 +3044,49 @@ namespace spot s.res_EventUniv->end()); } else - // We don't rewrite Ga & f1...fn = G(a & f1..fn) - // similarly to what we do in the unop::Or case - // as it is not clear what we'd gain by doing so. + // If f1...fn are event&univ formulae, with at least + // one formula of the form G(...), + // Rewrite g & f1...fn as g & G(f1..fn) while + // stripping any leading G from f1...fn. + // This gathers eventual&universal formulae + // under the same term. { - s.res_other->insert(s.res_other->begin(), - s.res_EventUniv->begin(), - s.res_EventUniv->end()); + multop::vec* eu = new multop::vec; + bool seen_g = false; + for (multop::vec::const_iterator + i = s.res_EventUniv->begin(); + i != s.res_EventUniv->end(); ++i) + { + if ((*i)->is_eventual() && (*i)->is_universal()) + { + if (const unop* g = is_G(*i)) + { + seen_g = true; + eu->push_back(g->child()->clone()); + g->destroy(); + } + else + { + eu->push_back(*i); + } + } + else + s.res_other->push_back(*i); + } + if (seen_g) + { + eu->push_back(allFG); + allFG = 0; + s.res_other->push_back(unop_multop(unop::G, + multop::And, + eu)); + } + else + { + s.res_other->insert(s.res_other->end(), + eu->begin(), eu->end()); + delete eu; + } } delete s.res_EventUniv; @@ -2964,7 +3250,7 @@ namespace spot // // In effect we rewrite // Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge - if (!s.res_X->empty()) + if (!s.res_X->empty() && !opt_.favor_event_univ) { multop::vec* event = new multop::vec; for (multop::vec::iterator i = s.res_G->begin(); @@ -3511,7 +3797,7 @@ namespace spot // Xa | Xb | GF(c) = X(a | b | GF(c)) // For Universal&Eventual formula f1...fn we also have: // Xa | Xb | f1...fn = X(a | b | f1...fn) - if (!s.res_X->empty()) + if (!s.res_X->empty() && !opt_.favor_event_univ) { s.res_X->push_back(allGF); allGF = 0; @@ -3519,7 +3805,8 @@ namespace spot s.res_EventUniv->begin(), s.res_EventUniv->end()); } - else if (!s.res_F->empty() + else if (!opt_.favor_event_univ + && !s.res_F->empty() && s.res_G->empty() && s.res_U_or_W->empty() && s.res_R_or_M->empty() @@ -3538,7 +3825,7 @@ namespace spot // F(a|GFb) 3st.6tr. with initial self-loop // Fa|GFb 4st.8tr. without initial self-loop // - // However, if other term are presents they will + // However, if other terms are presents they will // prevent the formation of a self-loop, and the // rewriting is unwelcome: // F(a|GFb)|Gc 5st.11tr. without initial self-loop @@ -3552,6 +3839,41 @@ namespace spot s.res_EventUniv->begin(), s.res_EventUniv->end()); } + else if (opt_.favor_event_univ) + { + s.res_EventUniv->push_back(allGF); + allGF = 0; + bool seen_f = false; + if (s.res_EventUniv->size() > 1) + { + // If some of the EventUniv formulae start + // with an F, Gather them all under the + // same F. Striping any leading F. + for (multop::vec::iterator i = + s.res_EventUniv->begin(); + i != s.res_EventUniv->end(); ++i) + if (const unop* u = is_F(*i)) + { + *i = u->child()->clone(); + u->destroy(); + seen_f = true; + } + if (seen_f) + { + const formula* eu = + unop_multop(unop::F, multop::Or, + s.res_EventUniv); + s.res_EventUniv = 0; + s.res_other->push_back(eu); + } + } + if (!seen_f) + { + s.res_other->insert(s.res_other->end(), + s.res_EventUniv->begin(), + s.res_EventUniv->end()); + } + } else { s.res_other->insert(s.res_other->end(), diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 3f5133ea1..bed0d0630 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -38,7 +38,8 @@ namespace spot bool containment_checks_stronger = false, bool nenoform_stop_on_boolean = false, bool reduce_size_strictly = false, - bool boolean_to_isop = false) + bool boolean_to_isop = false, + bool favor_event_univ = false) : reduce_basics(basics), synt_impl(synt_impl), event_univ(event_univ), @@ -46,7 +47,8 @@ namespace spot containment_checks_stronger(containment_checks_stronger), nenoform_stop_on_boolean(nenoform_stop_on_boolean), reduce_size_strictly(reduce_size_strictly), - boolean_to_isop(boolean_to_isop) + boolean_to_isop(boolean_to_isop), + favor_event_univ(favor_event_univ) { } @@ -64,6 +66,8 @@ namespace spot bool reduce_size_strictly; // If true, Boolean subformulae will be rewritten in ISOP form. bool boolean_to_isop; + // Try to isolate subformulae that are eventual and universal. + bool favor_event_univ; }; // fwd declaration to hide technical details. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index b109356a2..9e8ba524e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -192,6 +192,8 @@ syntax(char* prog) << " -rd display the reduced formula" << std::endl << " -rD dump statistics about the simplifier cache" << std::endl << " -rL disable basic rewritings producing larger formulas" + << std::endl + << " -ru lift formulae that are eventual and universal" << std::endl << std::endl << "Automaton degeneralization (after translation):" @@ -777,6 +779,12 @@ main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-RT")) { opt_bisim_ta = true; + } + else if (!strcmp(argv[formula_index], "-ru")) + { + simpltl = true; + redopt.event_univ = true; + redopt.favor_event_univ = true; } else if (!strcmp(argv[formula_index], "-M")) { diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 8eb69f9a9..4ac82cf95 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -110,6 +110,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM) reduction7+ru of formula (pre reduction)" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -r7 -ru -F -f -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula in FM" @@ -256,6 +264,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Compositional Suspension (-r4 -ru)" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -u -r4 -ru -F -f -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), degeneralized on states"