diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index f6c0e07ed..fb8ab6192 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1183,7 +1183,7 @@ would invalidate the results stored in the caches). This is implemented by the `\verb|ltl_simplifier::negative_normal_form|` method. -A formula in negative normal form can only have only have negation +A formula in negative normal form can only have negation operators ($\NOT$) in front of atomic properties, and does not use any of the $\XOR$, $\IMPLIES$ and $\EQUIV$ operators. The following rewriting arrange any PSL formula into negative normal form. @@ -1256,7 +1256,7 @@ The goals in most of these simplification are to: limit the sources of indeterminism. \end{itemize} -\subsection{Basic Simplifications} +\subsection{Basic Simplifications}\label{sec:basic-simp} These simplifications are enabled with \verb|ltl_simplifier_options::reduce_basics|'. A couple of them may @@ -1431,6 +1431,34 @@ that occur in $r$. For instance $\sere{a\STAR{}\CONCAT presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but unfortunately not when the \samp{$\ANDALT$} operator is used. +\subsubsection{Basic Simplifications SERE-LTL Binding Operators} + +The following rewritings are applied to the operators $\Asuffix$ and +$\Esuffix$. They assume that $b$, denote a Boolean formula. + +As noted at the beginning for section~\ref{sec:basic-simp}, rewritings +denoted with $\equiV$ can be disabled by setting the +\verb|ltl_simplifier_options::reduce_size_strictly|' option to +\texttt{true}. + +\begin{align*} + \sere{\STAR{}}\Asuffix f &\equiv \G f\\ + \sere{b\STAR{}}\Asuffix f &\equiv f \W \NOT b\\ + \sere{b\PLUS{}}\Asuffix f &\equiv f \W \NOT b\\ + \sere{r\STAR{\mvar{i}..\mvar{j}}}\Asuffix f &\equiV + \sere{r}\Asuffix \X( + \sere{r}\Asuffix \X(\ldots + \Asuffix\X(r\STAR{\mvar{1}..\mvar{j-i+1}}))) + \text{~if~}i\ge 1\text{~and~}\varepsilon\not\VDash r\\ + \sere{r\CONCAT \STAR{}}\Asuffix f &\equiv \sere{r}\Asuffix \G f\\ + \sere{r\CONCAT b\STAR{}}\Asuffix f &\equiV \sere{r}\Asuffix (f\AND \X(f \W \NOT b)) \text{~if~}\varepsilon\not\VDash r\\ + \sere{\STAR{}\CONCAT r}\Asuffix f &\equiV \G(\sere{r}\Asuffix f)\\ + \sere{b\STAR{}\CONCAT r}\Asuffix f &\equiV (\NOT b)\R(\sere{r}\Asuffix f) \text{~if~}\varepsilon\not\VDash r\\ + \sere{r_1\CONCAT r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix\X(\sere{r_2}\Asuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\ + \sere{r_1\FUSION r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix(\sere{r_2}\Asuffix f)\\ + \sere{r_1\OR r_2}\Asuffix f &\equiV (\sere{r_1}\Asuffix f)\AND(\sere{r_2}\Asuffix f) +\end{align*} + \subsection{Simplifications for Eventual and Universal Formul\ae} \label{sec:eventunivrew} diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 98066564c..e6c6d1620 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -186,6 +186,19 @@ namespace spot return is_bunop(f, bunop::Star); } + /// \brief Cast \a f into a bunop if it is a Star[0..]. + /// + /// Return 0 otherwise. + inline + bunop* + is_KleenStar(const formula* f) + { + if (bunop* b = is_Star(f)) + if (b->min() == 0 && b->max() == bunop::unbounded) + return b; + return 0; + } + } } #endif // SPOT_LTLAST_BUNOP_HH diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index a8ec8b520..16120c121 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -209,6 +209,7 @@ main(int argc, char** argv) int length_f1_before = spot::ltl::length(f1); std::string f1s_before = spot::ltl::to_string(f1); + std::string f1l; spot::ltl::formula* input_f = f1; f1 = simp_size->simplify(input_f); @@ -222,11 +223,11 @@ main(int argc, char** argv) else { spot::ltl::formula* maybe_larger = simp->simplify(input_f); + f1l = spot::ltl::to_string(maybe_larger); 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; + << f1s_before << "' to `" << f1l << "'." << std::endl; exit_code = 3; } maybe_larger->destroy(); @@ -253,8 +254,10 @@ main(int argc, char** argv) if (!f2 && (!hidereduc || (length_f1_after > length_f1_before))) { std::cout << length_f1_before << " " << length_f1_after - << " '" << f1s_before << "' reduce to '" << f1s_after << "'" - << std::endl; + << " '" << f1s_before << "' reduce to '" << f1s_after << "'"; + if (f1l != "" && f1l != f1s_after) + std::cout << " or (w/o rss) to '" << f1l << "'"; + std::cout << std::endl; } if (f2) diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 936429754..e97409aa7 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -290,8 +290,22 @@ for x in ../reduccmp ../reductaustr; do '{{r1*&r2*}:{b1&&b2}} <>-> x' run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}} <>-> x' \ '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}} <>-> x' - run 0 $x '{a&b&c*}|->!Xb' '{(a&&b)|((a&&b):c*)}|-> X!b' + run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))' run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!' + run 0 $x '{[*]}[]->b' 'Gb' + run 0 $x '{a;[*]}[]->b' 'Gb | !a' + run 0 $x '{[*];a}[]->b' 'G(b | !a)' + run 0 $x '{a;b;[*]}[]->c' '!a | X(!b | Gc)' + run 0 $x '{a;a;[*]}[]->c' '!a | X(!a | Gc)' + run 0 $x '{s[*]}[]->b' 'b W !s' + run 0 $x '{s[+]}[]->b' 'b W !s' + run 0 $x '{s[*2..]}[]->b' '!s | X(b W !s)' + run 0 $x '{a;b*;c;d*}[]->e' '!a | X(!b R ((e & X(e W !d)) | !c))' + run 0 $x '{a:b*:c:d*}[]->e' '!a | ((!c | (e W !d)) W !b)' + run 0 $x '{a|b*|c|d*}[]->e' '(e | !(a | c)) & (e W !b) & (e W !d)' + run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \ + '{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)' + # not reduced run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \ '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index e2dc353b6..3d1e961f2 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1772,11 +1772,236 @@ namespace spot } } } + case binop::UConcat: + if (!opt_.reduce_basics) + break; + if (bunop* bu = is_Star(a)) + { + // {[*]}[]->b = Gb + if (a == bunop::one_star()) + { + a->destroy(); + result_ = recurse_destroy(unop::instance(unop::G, b)); + return; + } + formula* s = bu->child(); + unsigned min = bu->min(); + unsigned max = bu->max(); + // {s[*]}[]->b = b W !s if s is Boolean. + // {s[+]}[]->b = b W !s if s is Boolean. + if (s->is_boolean() && max == bunop::unbounded && min <= 1) + { + formula* ns = // !s + unop::instance(unop::Not, s->clone()); + result_ = // b W !s + binop::instance(binop::W, b, ns); + bu->destroy(); + result_ = recurse_destroy(result_); + return; + } + if (opt_.reduce_size_strictly) + break; + // {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b + // = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b))) + // if i>0 and s does not accept the empty word + if (min == 0 || s->accepts_eword()) + break; + --min; + if (max != bunop::unbounded) + max -= min; // j-i+1 + // Don't rewrite s[1..]. + if (min == 0) + break; + formula* tail = // {s[*1..j-i]}[]->b + binop::instance(binop::UConcat, + bunop::instance(bunop::Star, + s->clone(), 1, max), + b); + for (unsigned n = 0; n < min; ++n) + tail = // {s}[]->X(tail) + binop::instance(binop::UConcat, + s->clone(), + unop::instance(unop::X, tail)); + result_ = tail; + bu->destroy(); + result_ = recurse_destroy(result_); + return; + } + else if (multop* mo = is_Concat(a)) + { + unsigned s = mo->size() - 1; + formula* last = mo->nth(s); + // {r;[*]}[]->b = {r}[]->Gb + if (last == bunop::one_star()) + { + result_ = binop::instance(binop::UConcat, + mo->all_but(s), + unop::instance(unop::G, b)); + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + + formula* first = mo->nth(0); + // {[*];r}[]->b = G({r}[]->b) + if (first == bunop::one_star()) + { + result_ = + unop::instance(unop::G, + binop::instance(binop::UConcat, + mo->all_but(0), + b)); + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + + if (opt_.reduce_size_strictly) + break; + + // {r;s[*]}[]->b = {r}[]->(b & X(b W !s)) + // if s is Boolean and r does not accept [*0]; + if (bunop* l = is_KleenStar(last)) // l = s[*] + if (l->child()->is_boolean()) + { + formula* r = mo->all_but(s); + if (!r->accepts_eword()) + { + formula* ns = // !s + unop::instance(unop::Not, l->child()->clone()); + formula* w = // b W !s + binop::instance(binop::W, b->clone(), ns); + formula* x = // X(b W !s) + unop::instance(unop::X, w); + formula* d = // b & X(b W !s) + multop::instance(multop::And, b, x); + result_ = // {r}[]->(b & X(b W !s)) + binop::instance(binop::UConcat, r, d); + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + } + // {s[*];r}[]->b = !s R ({r}[]->b) + // if s is Boolean and r does not accept [*0]; + if (bunop* l = is_KleenStar(first)) + if (l->child()->is_boolean()) + { + formula* r = mo->all_but(0); + if (!r->accepts_eword()) + { + formula* ns = // !s + unop::instance(unop::Not, l->child()->clone()); + formula* u = // {r}[]->b + binop::instance(binop::UConcat, r, b); + result_ = // !s R ({r}[]->b) + binop::instance(binop::R, ns, u); + mo->destroy(); + result_ = recurse_destroy(result_); + return; + } + } + + // {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b)) + // if r₁, r₂, r₃ do not accept [*0]. + if (!mo->accepts_eword()) + { + unsigned count = 0; + for (unsigned n = 0; n <= s; ++n) + count += !mo->nth(n)->accepts_eword(); + assert(count > 0); + if (count == 1) + break; + // Let e denote a term that accepts [*0] + // and let f denote a term that do not. + // A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b + // in which count==2 will be grouped + // as follows: r₁ = e₁;f₁;e₂;e₃ + // r₂ = f₂;e₄ + // this way we have + // {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b + // where r₁ and r₂ do not accept [*0]. + unsigned pos = s + 1; + + // We compute the r formulas from the right + // (i.e., r₂ before r₁.) + multop::vec* r = new multop::vec; + do + r->insert(r->begin(), mo->nth(--pos)->clone()); + while (r->front()->accepts_eword()); + formula* tail = // {r₂}[]->b + binop::instance(binop::UConcat, + multop::instance(multop::Concat, r), + b); + while (--count) + { + multop::vec* r = new multop::vec; + do + r->insert(r->begin(), mo->nth(--pos)->clone()); + while (r->front()->accepts_eword()); + // If it's the last block, take all leading + // formulae as well. + if (count == 1) + while (pos > 0) + { + r->insert(r->begin(), mo->nth(--pos)->clone()); + assert(r->front()->accepts_eword()); + } + + tail = // X({r₂}[]->b) + unop::instance(unop::X, tail); + tail = // {r₁}[]->X({r₂}[]->b) + binop::instance(binop::UConcat, + multop::instance(multop::Concat, r), + tail); + } + mo->destroy(); + result_ = recurse_destroy(tail); + return; + } + } + else if (opt_.reduce_size_strictly) + { + break; + } + else if (multop* mo = is_Fusion(a)) + { + // {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b)) + unsigned s = mo->size(); + formula* tail = b; + do + { + --s; + tail = binop::instance(binop::UConcat, + mo->nth(s)->clone(), tail); + } + while (s != 0); + mo->destroy(); + result_ = recurse_destroy(tail); + return; + } + else if (multop* mo = is_OrRat(a)) + { + // {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b) + unsigned s = mo->size(); + multop::vec* v = new multop::vec; + for (unsigned n = 0; n < s; ++n) + { + formula* x = // {r₁}[]->b + binop::instance(binop::UConcat, + mo->nth(n)->clone(), b->clone()); + v->push_back(x); + } + mo->destroy(); + b->destroy(); + result_ = recurse_destroy(multop::instance(multop::And, v)); + return; + } + break; case binop::Xor: case binop::Equiv: case binop::Implies: case binop::EConcat: - case binop::UConcat: case binop::EConcatMarked: // No simplification... Yet? break;