diff --git a/NEWS b/NEWS index 068be3a4d..775bb710c 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,14 @@ New in spot 2.11.2.dev (not yet released) + Library: + + - The following new trivial simplifications have been implemented for SEREs: + - f|[+] = [+] if f rejects [*0] + - f|[*] = [*] if f accepts [*0] + - f&&[+] = f if f rejects [*0] + - b:b[*i..j] = b[*max(i,1)..j] + - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1,1), j+l-1] + Bug fixes: - Automata-based implication checks, used to simplify formulas were diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index f9205cced..288a5da0c 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -853,10 +853,18 @@ The following rules are all valid with the two arguments swapped. \1\OR b &\equiv \1 & \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\ && - \STAR{} \AND f &\equiv f & - \STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} & + \STAR{} \ANDALT f &\equiv f & + \STAR{} \OR f &\equiv \mathrlap{\STAR{}} & && - \STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\ + \STAR{} \CONCAT f &\equiv \STAR{}\text{~if~}\varepsilon\VDash f& \\ + && + \PLUS{} \ANDALT f &\equiv f \text{~if~}\varepsilon\nVDash f& + \PLUS{} \OR f &\equiv \begin{cases} + \mathrlap{\STAR{}\text{~if~} \varepsilon\VDash f} \\ + \mathrlap{\PLUS{}\text{~if~} \varepsilon\nVDash f} \\ + \end{cases} & + && + && \\ \eword\AND f &\equiv f & \eword\ANDALT f &\equiv \begin{cases} @@ -880,7 +888,9 @@ The following rules are all valid with the two arguments swapped. f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}} & f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\ f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f&\equiv f\FSTAR{\mvar{i+1}..\mvar{j+1}} & -f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}} +f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}}\\ +b\STAR{\mvar{i}..\mvar{j}}\FUSION b &\equiv b\STAR{\mvar{\max(i,1)}..\mvar{j}} & +b\STAR{\mvar{i}..\mvar{j}}\FUSION b\STAR{\mvar{k}..\mvar{l}} &\equiv b\mathrlap{\STAR{\mvar{\max(i,1)+\max(k,1)-1}..\mvar{j+l-1}}} \end{align*} \section{SERE-LTL Binding Operators} diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index a3145884d..370a50e8f 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -307,11 +307,14 @@ namespace spot unsigned orig_size = v.size(); - const fnode* neutral; - const fnode* neutral2; - const fnode* abs; - const fnode* abs2; - const fnode* weak_abs; + const fnode* neutral; // neutral element + const fnode* neutral2; // second neutral element (if any) + const fnode* abs; // absorbent element + const fnode* abs2; // second absorbent element (if any) + const fnode* weak_abs; // almost absorbent element (if any) + // The notion of "almost absorbent" captures situation where the + // present of the element can be simplified in itself or another + // element depending on a condition on the rest of the formula. switch (o) { case op::And: @@ -323,7 +326,17 @@ namespace spot break; case op::AndRat: neutral = one_star(); - neutral2 = nullptr; + { + // If this AndRat contains an operand that does not accept + // the empty word, and that is not [+], then any [+] can be + // removed. + bool one_non_eword_non_plus = + std::find_if(v.begin(), v.end(), + [o = one_plus()](const fnode* f) { + return !f->accepts_eword() && f != o; + }) != v.end(); + neutral2 = one_non_eword_non_plus ? one_plus() : nullptr; + } abs = ff(); abs2 = nullptr; weak_abs = eword(); @@ -349,7 +362,7 @@ namespace spot neutral2 = nullptr; abs = one_star(); abs2 = nullptr; - weak_abs = nullptr; + weak_abs = one_plus(); gather_bool(v, op::Or); break; case op::Concat: @@ -506,11 +519,10 @@ namespace spot else return abs; } - else + else if (o == op::AndNLM) { // Similarly, a* & 1 & (c;d) = c;d // a* & 1 & c* = 1 - assert(o == op::AndNLM); vec tmp; for (auto i: v) { @@ -527,6 +539,27 @@ namespace spot tmp.emplace_back(weak_abs); v.swap(tmp); } + else if (o == op::OrRat) + { + // We have a[*] | [+] | c = [*] + // and a | [+] | c = [+] + // So if [+] has been seen, check if some term + // recognize the empty word. + bool acc_eword = false; + for (i = v.begin(); i != v.end(); ++i) + { + acc_eword |= (*i)->accepts_eword(); + (*i)->destroy(); + } + if (acc_eword) + return abs; + else + return weak_abs; + } + else + { + SPOT_UNREACHABLE(); + } } else if (o == op::Concat || o == op::Fusion) { @@ -613,6 +646,81 @@ namespace spot *fpos = newfs; } } + // also + // b[*i..j]:b -> b[*max(1,i),j] + // b:b[*i..j] -> b[*max(1,i),j] + // b[*i..j]:b[*k..l] -> b[*max(i,1)+max(j,1)-1,j+l-1] + if (o == op::Fusion && v.size() > 1) + { + i = v.begin(); + while (i != v.end()) + { + if (!(((*i)->is(op::Star) && (*i)->nth(0)->is_boolean()) + || (*i)->is_boolean())) + { + ++i; + continue; + } + const fnode *b; + unsigned min; + unsigned max; + if ((*i)->is_boolean()) + { + min = max = 1; + b = *i; + } + else + { + b = (*i)->nth(0); + min = (*i)->min(); + max = (*i)->max(); + } + vec::iterator prev = i; + ++i; + bool changed = false; + while (i != v.end()) + { + unsigned min2; + unsigned max2; + if ((*i)->is_boolean()) + { + if (*i != b) + break; + min2 = max2 = 1; + } + else if ((*i)->is(op::Star) && (*i)->nth(0)->is_boolean()) + { + if ((*i)->nth(0) != b) + break; + min2 = (*i)->min(); + max2 = (*i)->max(); + } + else + { + break; + } + // Now we can merge prev and i. + min = min + (min == 0) + min2 + (min2 == 0) - 1; + assert(max != 0 && max2 != 0); + if (max2 == unbounded() || max == unbounded()) + max = unbounded(); + else if (max + max2 < unbounded()) + max = max + max2 - 1; + else + break; + changed = true; + (*i)->destroy(); + i = v.erase(i); + } + if (changed) + { + const fnode* newf = + fnode::bunop(op::Star, b->clone(), min, max); + (*prev)->destroy(); + *prev = newf; + } + } + } } } diff --git a/tests/core/equals.test b/tests/core/equals.test index f00216347..a67c4b1ef 100755 --- a/tests/core/equals.test +++ b/tests/core/equals.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2012, 2014-2015, 2021 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2015, 2021, 2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -196,6 +196,12 @@ G({1}<>->1), 1 {(a*;b|c)[:*0]}, 1 {(a*;b|c)[:*1]}, {(a*;b|c)} {(a;b):(a;b):(a;b)[:*2]:(a;b):b*:b*:(c;d)[:*1]}, {(a;b)[:*5]:b*[:*2]:(c;d)} +{((a;b)|[+]|(c;d[*]));a}, {[+];a} +{((a;b)|[+]|(d[*]));a}, {[*];a} +{((a;b)&&[+]&&(d[*]));a}, {((a;b)&&(d[*]));a} +{((a;b|[*0])&&[+]&&(d[*]));a}, {((a;b|[*0])&&[+]&&(d[*]));a} +{(a;c):b[*3..5]:b[*10]:(a;c)}, {(a;c):b[*12..14]:(a;c)} +{(a;c):b:b[*3..5]:b:b[*0..4]:(a;c)}, {(a;c):b[*3..8]:(a;c)} EOF