diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index c39df387a..8c19a45c0 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -96,6 +96,9 @@ \newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}} \newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}} +% rewriting rules that enlarge the formula +\newcommand{\equiV}{\stackrel{\star}{\equiv}} + \def\limplies{\rightarrow} \def\simp{\rightrightharpoons} \def\Simp{\stackrel{+}{\simp}} @@ -1088,11 +1091,11 @@ presented by~\citet{chang.92.icalp}, but other presentations have been done including negation~\citep{cerna.03.mfcs} and weak until~\citep{schneider.01.lpar}. -The following grammar rules describes extend the aforementioned -work slightly by dealing with PSL operators. These are the -rules used by Spot to decide upon -construction to which class a formula belongs (see the methods -\texttt{is\_syntactic\_safety()}, \texttt{is\_syntactic\_guarantee()}, +The following grammar rules extend the aforementioned work slightly by +dealing with PSL operators. These are the rules used by Spot to +decide upon construction to which class a formula belongs (see the +methods \texttt{is\_syntactic\_safety()}, +\texttt{is\_syntactic\_guarantee()}, \texttt{is\_syntactic\_obligation()}, \texttt{is\_syntactic\_recurrence()}, and \texttt{is\_syntactic\_persistence()} listed on @@ -1231,12 +1234,12 @@ Section~\ref{sec:unabbbool}. Therefore it is never necessary to apply `\verb|ltl_simplifier::negative_normal_form|`. If the option `\verb|nenoform_stop_on_boolean|' is set, the above -recursive rewritings will not be applied to subformul\ae{} that are -Boolean formul\ae. For instance calling -`\verb|ltl_simplifier::negative_normal_form|` on $\NOT\F\G(a \XOR b)$ -will produce $\G\F(((\NOT a)\AND(\NOT b))\OR(a\AND b))$ if -`\verb|nenoform_stop_on_boolean|' is unset, while it will produce -$\G\F(\NOT(a \XOR b))$ if `\verb|nenoform_stop_on_boolean|' is set. +recursive rewritings are not applied to Boolean subformul\ae{}. For +instance calling `\verb|ltl_simplifier::negative_normal_form|` on +$\NOT\F\G(a \XOR b)$ will produce $\G\F(((\NOT a)\AND(\NOT +b))\OR(a\AND b))$ if `\verb|nenoform_stop_on_boolean|' is unset, while +it will produce $\G\F(\NOT(a \XOR b))$ if +`\verb|nenoform_stop_on_boolean|' is set. \section{Simplifications} @@ -1264,7 +1267,11 @@ The goals in most of these simplification are to: \subsection{Basic Simplifications} These simplifications are enabled with -\verb|ltl_simplifier_options::reduce_basics|'. +\verb|ltl_simplifier_options::reduce_basics|'. A couple of them may +enlarge the size of the formula: they are denoted using $\equiV$ +instead of $\equiv$, and they can be disabled by setting the +\verb|ltl_simplifier_options::reduce_size_strictly|' option to +\texttt{true}. \subsubsection{Basic Simplifications for Temporal Operators} \label{sec:basic-simp-ltl} @@ -1280,25 +1287,29 @@ from left to right, as usual): \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m) \end{align*} -Note that the latter rewriting rules for $\G$ has no dual: -rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as -suggested by~\citet{somenzi.00.cav}) goes against our goal of moving -the $\F$ operator in front of the formula. Conceptually, it is also -easier to understand $\F(f \AND \G\F g)$: has long as $f$ has not been -verified, there is no need to worry about the $\G\F g$ term. +Note that the latter three rewriting rules for $\G$ have no dual: +rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested +by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$ +operator in front of the formula. Conceptually, it is also easier to +understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified, +there is no need to worry about the $\G\F g$ term. + +Here are the basic rewriting rules for binary operators (excluding +$\OR$ and $\AND$ which are considered in Spot as $n$-ary operators). +$b$ denotes a Boolean formula. -Here are the basic rewriting rules for binary operators (excluding $\OR$ and -$\AND$ which are considered in Spot as $n$-ary operators): \begin{align*} - \1 \U f & \equiv \F f & f \W \0 & \equiv \G f \\ - f \M \1 & \equiv \F f & \0 \R f & \equiv \G f \\ - (\X f)\U (\X g) & \equiv \X(f\U g) & (\X f)\W(\X g) & \equiv \X(f\W g) \\ - (\X f)\M (\X g) & \equiv \X(f\M g) & (\X f)\R(\X g) & \equiv \X(f\R g) \\ - f \U(\G f) & \equiv \G f & f \W(\G f) & \equiv \G f \\ - f \M(\F f) & \equiv \F f & f \R(\F f) & \equiv \F f \\ - f \U (g \OR \G(f)) & \equiv f\W g & f \W (g \OR \G(f)) & \equiv f\W g \\ - f \M (g \AND \F(f)) & \equiv f\M g & f \R (g \AND \F(f)) & \equiv f\M g \\ - f \U (g \AND f) & \equiv g\M f & f \W (g \AND f) & \equiv g\R f + \1 \U f & \equiv \F f & f \W \0 & \equiv \G f \\ + f \M \1 & \equiv \F f & \0 \R f & \equiv \G f \\ + (\X f)\U (\X g) & \equiv \X(f\U g) & (\X f)\W(\X g) & \equiv \X(f\W g) \\ + (\X f)\M (\X g) & \equiv \X(f\M g) & (\X f)\R(\X g) & \equiv \X(f\R g) \\ + (\X f)\U b & \equiV b\OR \X(b\M f) & (\X f)\W b & \equiV b\OR \X(f\R b) \\ + (\X f)\M b & \equiV b\AND \X(b\U f) & (\X f)\R b & \equiV b\AND \X(f\W b) \\ + f \U(\G f) & \equiv \G f & f \W(\G f) & \equiv \G f \\ + f \M(\F f) & \equiv \F f & f \R(\F f) & \equiv \F f \\ + f \U (g \OR \G(f)) & \equiv f\W g & f \W (g \OR \G(f)) & \equiv f\W g \\ + f \M (g \AND \F(f)) & \equiv f\M g & f \R (g \AND \F(f)) & \equiv f\M g \\ + f \U (g \AND f) & \equiv g\M f & f \W (g \AND f) & \equiv g\R f \end{align*} Here are the basic rewriting rules for $n$-ary operators ($\AND$ and @@ -1341,7 +1352,7 @@ The above rules are applied even if more terms are presents in the operator's arguments. For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND \X(d)$ will be rewritten as $\X(d \AND \F\G(a\AND c))\AND \G(b)$. -The following more complicated rules are generalization of $f\AND +The following more complicated rules are generalizations of $f\AND \X\G f\equiv \G f$ and $f\OR \X\F f\equiv \F f$: \begin{align*} f\AND \X(\G(f\AND g\ldots)\AND h\ldots) &\equiv \G(f) \AND \X(\G(g\ldots)\AND h\ldots) \\ @@ -1351,7 +1362,7 @@ The latter rule for $f\OR \X(\F(f)\OR h\ldots)$ is only applied if all $\F$-formul\ae{} can be removed from the argument of $\X$ with the rewriting. For instance $a \OR b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ will be rewritten to $\F(a \OR b \OR c) \OR \X\G d$ but -$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ would only become +$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ will only become $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 @@ -1503,6 +1514,7 @@ sometimes generalized to support operators such as $\M$ and $\W$. \appendix \chapter{Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$} +\label{sec:ltl-equiv} The operators \samp{F}, \samp{G}, \samp{U}, \samp{R}, \samp{M}, and \samp{W} can all be defined using only Boolean operators, \samp{X}, diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index d2a051fb2..a8ec8b520 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -141,6 +141,8 @@ main(int argc, char** argv) } spot::ltl::ltl_simplifier* simp = new spot::ltl::ltl_simplifier(o); + o.reduce_size_strictly = true; + spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o); spot::ltl::formula* f1 = 0; spot::ltl::formula* f2 = 0; @@ -202,24 +204,35 @@ main(int argc, char** argv) spot::ltl::formula* ftmp1; ftmp1 = f1; - f1 = simp->negative_normal_form(f1, false); + f1 = simp_size->negative_normal_form(f1, false); ftmp1->destroy(); int length_f1_before = spot::ltl::length(f1); std::string f1s_before = spot::ltl::to_string(f1); - ftmp1 = f1; - f1 = simp->simplify(f1); - - if (!simp->are_equivalent(ftmp1, f1)) + spot::ltl::formula* input_f = f1; + f1 = simp_size->simplify(input_f); + if (!simp_size->are_equivalent(input_f, f1)) { std::cerr << "Incorrect reduction from `" << f1s_before << "' to `" << spot::ltl::to_string(f1) << "'." << std::endl; exit_code = 3; } + else + { + spot::ltl::formula* maybe_larger = simp->simplify(input_f); + if (!simp->are_equivalent(input_f, maybe_larger)) + { + std::cerr << "Incorrect reduction (reduce_size_strictly=0) from `" + << f1s_before << "' to `" << spot::ltl::to_string(f1) + << "'." << std::endl; + exit_code = 3; + } + maybe_larger->destroy(); + } - ftmp1->destroy(); + input_f->destroy(); int length_f1_after = spot::ltl::length(f1); std::string f1s_after = spot::ltl::to_string(f1); @@ -228,7 +241,7 @@ main(int argc, char** argv) if (f2) { ftmp1 = f2; - f2 = simp->negative_normal_form(f2, false); + f2 = simp_size->negative_normal_form(f2, false); ftmp1->destroy(); f2s = spot::ltl::to_string(f2); } @@ -282,6 +295,7 @@ main(int argc, char** argv) } end: + delete simp_size; delete simp; if (fin) diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 75246b4a7..4fa701cb7 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -1,6 +1,6 @@ #! /bin/sh -# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement -# de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +# Developpement de l'Epita (LRDE). # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -105,6 +105,13 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'Xa & Xb' 'X(a & b)' run 0 $x 'Xa | Xb' 'X(a | b)' + run 0 $x 'X(a) M X(b)' 'X(a M b)' + run 0 $x 'X(a) W X(b)' 'X(a W b)' + run 0 $x 'X(a) M b' 'b & X(b U a)' + run 0 $x 'X(a) R b' 'b & X(b W a)' + run 0 $x 'X(a) U b' 'b | X(b M a)' + run 0 $x 'X(a) W b' 'b | X(b R a)' + run 0 $x '(a U b) & (c U b)' '(a & c) U b' run 0 $x '(a R b) & (a R c)' 'a R (b & c)' run 0 $x '(a U b) | (a U c)' 'a U (b | c)' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 6fdbb0381..1d96e2285 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1747,6 +1747,24 @@ namespace spot } } } + // If b is Boolean: + // (Xc) U b = b | X(b M c) + // (Xc) W b = b | X(b R c) + if (!opt_.reduce_size_strictly + && fu1 && fu1->op() == unop::X && b->is_boolean()) + { + formula* c = fu1->child()->clone();; + fu1->destroy(); + formula* x = + unop::instance(unop::X, + binop::instance(op == binop::U + ? binop::M + : binop::R, + b->clone(), c)); + result_ = + recurse_destroy(multop::instance(multop::Or, b, x)); + return; + } } else if (op == binop::M || op == binop::R) { @@ -1791,6 +1809,25 @@ namespace spot } } } + + // If b is Boolean: + // (Xc) R b = b & X(b W c) + // (Xc) M b = b & X(b U c) + if (!opt_.reduce_size_strictly + && fu1 && fu1->op() == unop::X && b->is_boolean()) + { + formula* c = fu1->child()->clone();; + fu1->destroy(); + formula* x = + unop::instance(unop::X, + binop::instance(op == binop::M + ? binop::U + : binop::W, + b->clone(), c)); + result_ = + recurse_destroy(multop::instance(multop::And, b, x)); + return; + } } } case binop::Xor: diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 0c8929607..880dcb768 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -37,15 +37,15 @@ namespace spot bool event_univ = true, bool containment_checks = false, bool containment_checks_stronger = false, - bool nenoform_stop_on_boolean = false) + bool nenoform_stop_on_boolean = false, + bool reduce_size_strictly = false) : reduce_basics(basics), synt_impl(synt_impl), event_univ(event_univ), containment_checks(containment_checks), containment_checks_stronger(containment_checks_stronger), - // If true, Boolean subformulae will not be put into - // negative normal form. - nenoform_stop_on_boolean(nenoform_stop_on_boolean) + nenoform_stop_on_boolean(nenoform_stop_on_boolean), + reduce_size_strictly(reduce_size_strictly) { } @@ -57,6 +57,10 @@ namespace spot // If true, Boolean subformulae will not be put into // negative normal form. bool nenoform_stop_on_boolean; + // If true, some rules that produce slightly larger formulae + // will be disabled. Those larger formulae are normally easier + // to translate, so we recommend to set this to false. + bool reduce_size_strictly; }; // fwd declaration to hide technical details.