alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Implement a favor_even_univ option in the rewriting rules.

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-11 19:09:34 +02:00
parent 969d927145
commit 9caa9ad134
9 changed files with 489 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

48
doc/tl/tl.tex
View file

@ -108,6 +108,9 @@
% rewriting rules that enlarge the formula % rewriting rules that enlarge the formula
\newcommand{\equiV}{\stackrel{\star}{\equiv}} \newcommand{\equiV}{\stackrel{\star}{\equiv}}
% rewriting rules that favors event/univ
\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}}
\newcommand{\equivNeu}{\stackrel{\smalltriangledown}{\equiv}}
% marked rewriting rules % marked rewriting rules
\newcommand{\equivM}{\stackrel{\dag}{\equiv}} \newcommand{\equivM}{\stackrel{\dag}{\equiv}}
@ -1298,6 +1301,13 @@ The goals in most of these simplification are to:
limit the sources of indeterminism. limit the sources of indeterminism.
\end{itemize} \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} \subsection{Basic Simplifications}\label{sec:basic-simp}
These simplifications are enabled with These simplifications are enabled with
@ -1356,10 +1366,10 @@ $\OR$):
(\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g) \\ (\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) \AND(\X g) &\equiv \X(f\AND g) &
(\X f) \OR (\X g) &\equiv \X(f\OR 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) \AND(\F\G g) &\equivNeu \X(f\AND \F\G g) &
(\X f) \OR (\G\F g) &\equiv \X(f\OR \G\F g) \\ (\X f) \OR (\G\F g) &\equivNeu \X(f\OR \G\F g) \\
(\G f) \AND(\G g) &\equiv \G(f\AND g) & (\G f) \AND(\G g) &\equivNeu \G(f\AND g) &
(\F f) \OR (\F g) &\equiv \F(f\OR 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)\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)\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& (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 Finally the following rule is applied only when no other terms are present
in the OR arguments: in the OR arguments:
\begin{align*} \begin{align*}
\F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m) \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g)
&\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\ &\equivNeu \F(f_1\OR \ldots \OR f_n \OR \G\F(g)) \\
\end{align*} \end{align*}
\subsubsection{Basic Simplifications for SERE Operators} \subsubsection{Basic Simplifications for SERE Operators}
@ -1558,17 +1568,29 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\
\end{center} \end{center}
\begin{align*} \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 \\ \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 \\
\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 \\ \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 \\
\X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f) & & 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*} \end{align*}
\begin{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 \intertext{Finally the following rule is applied only when no other
terms are present in the OR arguments:} 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) \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)
\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)
\end{align*} \end{align*}
\subsection{Simplifications Based on Implications} \subsection{Simplifications Based on Implications}

6
src/ltltest/Makefile.am
View file

@ -36,6 +36,7 @@ check_PROGRAMS = \
nenoform \ nenoform \
reduc \ reduc \
reduccmp \ reduccmp \
reduceu \
reductau \ reductau \
reductaustr \ reductaustr \
syntimpl \ syntimpl \
@ -58,6 +59,8 @@ nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
reduc_SOURCES = reduc.cc reduc_SOURCES = reduc.cc
reduccmp_SOURCES = equals.cc reduccmp_SOURCES = equals.cc
reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
reduceu_SOURCES = equals.cc
reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
reductau_SOURCES = equals.cc reductau_SOURCES = equals.cc
reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
reductaustr_SOURCES = equals.cc reductaustr_SOURCES = equals.cc
@ -99,7 +102,8 @@ TESTS = \
reduc0.test \ reduc0.test \
reducpsl.test \ reducpsl.test \
reduccmp.test \ reduccmp.test \
uwrm.test uwrm.test \
eventuniv.test
distclean-local: distclean-local:
rm -rf $(TESTS:.test=.dir) rm -rf $(TESTS:.test=.dir)

3
src/ltltest/equals.cc
View file

@ -104,6 +104,9 @@ main(int argc, char** argv)
#endif #endif
#ifdef REDUC #ifdef REDUC
spot::ltl::ltl_simplifier_options opt(true, true, true, false, false); 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); spot::ltl::ltl_simplifier simp(opt);
{ {
const spot::ltl::formula* tmp; const spot::ltl::formula* tmp;

60
src/ltltest/eventuniv.test Executable file
View file

@ -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 <http://www.gnu.org/licenses/>.
. ./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'

7
src/ltltest/reduc.cc
View file

@ -134,6 +134,13 @@ main(int argc, char** argv)
o.containment_checks = true; o.containment_checks = true;
o.containment_checks_stronger = true; o.containment_checks_stronger = true;
break; 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: default:
return 2; return 2;
} }

376
src/ltlvisit/simplify.cc
View file

@ -129,6 +129,7 @@ namespace spot
: dict(d), options(opt), lcc(d, true, true, false, false) : dict(d), options(opt), lcc(d, true, true, false, false)
{ {
options.containment_checks |= options.containment_checks_stronger; options.containment_checks |= options.containment_checks_stronger;
options.event_univ |= options.favor_event_univ;
} }
void void
@ -880,6 +881,9 @@ namespace spot
void process(const formula* f) 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()) switch (f->kind())
{ {
case formula::UnOp: case formula::UnOp:
@ -889,21 +893,21 @@ namespace spot
switch (uo->op()) switch (uo->op())
{ {
case unop::X: case unop::X:
if (res_X) if (res_X && !eu)
{ {
res_X->push_back(c->clone()); res_X->push_back(c->clone());
return; return;
} }
break; break;
case unop::F: case unop::F:
if (res_FG) if (res_FG && u)
if (const unop* cc = is_G(c)) if (const unop* cc = is_G(c))
{ {
res_FG->push_back(((split_ & Strip_FG) == Strip_FG res_FG->push_back(((split_ & Strip_FG) == Strip_FG
? cc->child() : f)->clone()); ? cc->child() : f)->clone());
return; return;
} }
if (res_F) if (res_F && !eu)
{ {
res_F->push_back(((split_ & Strip_F) == Strip_F res_F->push_back(((split_ & Strip_F) == Strip_F
? c : f)->clone()); ? c : f)->clone());
@ -911,14 +915,14 @@ namespace spot
} }
break; break;
case unop::G: case unop::G:
if (res_GF) if (res_GF && e)
if (const unop* cc = is_F(c)) if (const unop* cc = is_F(c))
{ {
res_GF->push_back(((split_ & Strip_GF) == Strip_GF res_GF->push_back(((split_ & Strip_GF) == Strip_GF
? cc->child() : f)->clone()); ? cc->child() : f)->clone());
return; return;
} }
if (res_G) if (res_G && !eu)
{ {
res_G->push_back(((split_ & Strip_G) == Strip_G res_G->push_back(((split_ & Strip_G) == Strip_G
? c : f)->clone()); ? c : f)->clone());
@ -966,8 +970,6 @@ namespace spot
} }
if (c_->options.event_univ) if (c_->options.event_univ)
{ {
bool e = f->is_eventual();
bool u = f->is_universal();
if (res_EventUniv && e && u) if (res_EventUniv && e && u)
{ {
res_EventUniv->push_back(f->clone()); res_EventUniv->push_back(f->clone());
@ -1154,12 +1156,28 @@ namespace spot
&& c_->lcc.equal(result_, uo)) && c_->lcc.equal(result_, uo))
return; return;
// Disabled: X(f1 & GF(f2)) = X(f1) & GF(f2) // X(f1 & GF(f2)) = X(f1) & GF(f2)
// Disabled: X(f1 | GF(f2)) = X(f1) | GF(f2) // X(f1 | GF(f2)) = X(f1) | GF(f2)
// Disabled: X(f1 & FG(f2)) = X(f1) & FG(f2) // X(f1 & FG(f2)) = X(f1) & FG(f2)
// Disabled: X(f1 | FG(f2)) = X(f1) | FG(f2) // X(f1 | FG(f2)) = X(f1) | FG(f2)
// The above make more sense when reversed, //
// so see them in the And and Or rewritings. // 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; break;
case unop::F: case unop::F:
@ -1259,7 +1277,8 @@ namespace spot
&& c_->lcc.contained(uo, result_)) && c_->lcc.contained(uo, result_))
return; 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 // As is, these two formulae are translated into
// equivalent Büchi automata so the rewriting is // equivalent Büchi automata so the rewriting is
@ -1272,7 +1291,86 @@ namespace spot
// rule which really helps the translation. F((f1 & // rule which really helps the translation. F((f1 &
// GF(f2)) | (a & GF(b))) is indeed easier to translate. // 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; break;
case unop::G: case unop::G:
@ -1356,6 +1454,52 @@ namespace spot
result_ = mo; 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 | Xb) = GF(a | b)
// GF(a | Fb) = GF(a | b) // GF(a | Fb) = GF(a | b)
@ -1870,7 +2014,6 @@ namespace spot
return; return;
} }
// e₁ W e₂ = Ge₁ | e₂ // e₁ W e₂ = Ge₁ | e₂
// u₁ M u₂ = Fu₁ & u₂ // u₁ M u₂ = Fu₁ & u₂
if (!opt_.reduce_size_strictly) 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; trace << "bo: no eventuniv rule matched" << std::endl;
} }
@ -2785,7 +3035,7 @@ namespace spot
// Xa & Xb & FG(c) = X(a & b & FG(c)) // Xa & Xb & FG(c) = X(a & b & FG(c))
// For Universal&Eventual formulae f1...fn we also have: // For Universal&Eventual formulae f1...fn we also have:
// Xa & Xb & f1...fn = X(a & b & f1...fn) // 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); s.res_X->push_back(allFG);
allFG = 0; allFG = 0;
@ -2794,13 +3044,49 @@ namespace spot
s.res_EventUniv->end()); s.res_EventUniv->end());
} }
else else
// We don't rewrite Ga & f1...fn = G(a & f1..fn) // If f1...fn are event&univ formulae, with at least
// similarly to what we do in the unop::Or case // one formula of the form G(...),
// as it is not clear what we'd gain by doing so. // 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(), multop::vec* eu = new multop::vec;
s.res_EventUniv->begin(), bool seen_g = false;
s.res_EventUniv->end()); 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; delete s.res_EventUniv;
@ -2964,7 +3250,7 @@ namespace spot
// //
// In effect we rewrite // In effect we rewrite
// Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge // 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; multop::vec* event = new multop::vec;
for (multop::vec::iterator i = s.res_G->begin(); for (multop::vec::iterator i = s.res_G->begin();
@ -3511,7 +3797,7 @@ namespace spot
// Xa | Xb | GF(c) = X(a | b | GF(c)) // Xa | Xb | GF(c) = X(a | b | GF(c))
// For Universal&Eventual formula f1...fn we also have: // For Universal&Eventual formula f1...fn we also have:
// Xa | Xb | f1...fn = X(a | b | f1...fn) // 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); s.res_X->push_back(allGF);
allGF = 0; allGF = 0;
@ -3519,7 +3805,8 @@ namespace spot
s.res_EventUniv->begin(), s.res_EventUniv->begin(),
s.res_EventUniv->end()); 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_G->empty()
&& s.res_U_or_W->empty() && s.res_U_or_W->empty()
&& s.res_R_or_M->empty() && s.res_R_or_M->empty()
@ -3538,7 +3825,7 @@ namespace spot
// F(a|GFb) 3st.6tr. with initial self-loop // F(a|GFb) 3st.6tr. with initial self-loop
// Fa|GFb 4st.8tr. without 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 // prevent the formation of a self-loop, and the
// rewriting is unwelcome: // rewriting is unwelcome:
// F(a|GFb)|Gc 5st.11tr. without initial self-loop // F(a|GFb)|Gc 5st.11tr. without initial self-loop
@ -3552,6 +3839,41 @@ namespace spot
s.res_EventUniv->begin(), s.res_EventUniv->begin(),
s.res_EventUniv->end()); 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 else
{ {
s.res_other->insert(s.res_other->end(), s.res_other->insert(s.res_other->end(),

8
src/ltlvisit/simplify.hh
View file

@ -38,7 +38,8 @@ namespace spot
bool containment_checks_stronger = false, bool containment_checks_stronger = false,
bool nenoform_stop_on_boolean = false, bool nenoform_stop_on_boolean = false,
bool reduce_size_strictly = false, bool reduce_size_strictly = false,
bool boolean_to_isop = false) bool boolean_to_isop = false,
bool favor_event_univ = false)
: reduce_basics(basics), : reduce_basics(basics),
synt_impl(synt_impl), synt_impl(synt_impl),
event_univ(event_univ), event_univ(event_univ),
@ -46,7 +47,8 @@ namespace spot
containment_checks_stronger(containment_checks_stronger), containment_checks_stronger(containment_checks_stronger),
nenoform_stop_on_boolean(nenoform_stop_on_boolean), nenoform_stop_on_boolean(nenoform_stop_on_boolean),
reduce_size_strictly(reduce_size_strictly), 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; bool reduce_size_strictly;
// If true, Boolean subformulae will be rewritten in ISOP form. // If true, Boolean subformulae will be rewritten in ISOP form.
bool boolean_to_isop; bool boolean_to_isop;
// Try to isolate subformulae that are eventual and universal.
bool favor_event_univ;
}; };
// fwd declaration to hide technical details. // fwd declaration to hide technical details.

8
src/tgbatest/ltl2tgba.cc
View file

@ -192,6 +192,8 @@ syntax(char* prog)
<< " -rd display the reduced formula" << std::endl << " -rd display the reduced formula" << std::endl
<< " -rD dump statistics about the simplifier cache" << std::endl << " -rD dump statistics about the simplifier cache" << std::endl
<< " -rL disable basic rewritings producing larger formulas" << " -rL disable basic rewritings producing larger formulas"
<< std::endl
<< " -ru lift formulae that are eventual and universal"
<< std::endl << std::endl << std::endl << std::endl
<< "Automaton degeneralization (after translation):" << "Automaton degeneralization (after translation):"
@ -778,6 +780,12 @@ main(int argc, char** argv)
{ {
opt_bisim_ta = true; 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")) else if (!strcmp(argv[formula_index], "-M"))
{ {
opt_monitor = true; opt_monitor = true;

16
src/tgbatest/spotlbtt.test
View file

@ -110,6 +110,14 @@ Algorithm
Enabled = yes 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 Algorithm
{ {
Name = "Spot (Couvreur -- FM), reduction of formula in FM" Name = "Spot (Couvreur -- FM), reduction of formula in FM"
@ -256,6 +264,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Compositional Suspension (-r4 -ru)"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -u -r4 -ru -F -f -t'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), degeneralized on states" Name = "Spot (Couvreur -- FM), degeneralized on states"