From 44efc9659586e25c74c4e0686c486f9c925bd2ea Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Jul 2024 17:56:04 +0200 Subject: [PATCH] formula: add a missing trivial rewriting in SERE MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We should have [*0]|f ≡ f when f is a SERE that already accept the empty word. Fixes issue #454. * spot/tl/formula.cc: Implement the rewriting. * tests/core/reduccmp.test: Add a test case. * doc/tl/tl.tex, NEWS: Document it. --- NEWS | 4 ++++ doc/tl/tl.tex | 30 +++++++++++++++--------------- spot/tl/formula.cc | 11 ++++++++++- tests/core/reduccmp.test | 3 ++- 4 files changed, 31 insertions(+), 17 deletions(-) diff --git a/NEWS b/NEWS index cb1129084..56e2040d4 100644 --- a/NEWS +++ b/NEWS @@ -32,6 +32,10 @@ New in spot 2.12.0.dev (not yet released) following "Efficient Normalization of Linear Temporal Logic" by Esparza et al. (J. ACM, 2024). + - Trivial rewritings (those performed everytime at construction) + were missing the rule "[*0]|f ≡ f" when f already accepts the + empty word. (Issue #545.) + New in spot 2.12 (2024-05-16) Build: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 65db63511..9d1b1c2ef 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -839,47 +839,47 @@ The following rules are all valid with the two arguments swapped. %\samp{$\FUSION$}.) \begin{align*} - \0\AND f &\equiv \0 & \0\ANDALT f &\equiv \0 & + \0\AND f &\equiv \0 & \0\OR f &\equiv f & \0 \FUSION f &\equiv \0 & - \0 \CONCAT f &\equiv \0 \\ + \mathllap{\0 \CONCAT f}&\equiv \0 \\ + \1\ANDALT b &\equiv b & \1\AND f&\equiv \begin{cases} 1\mathrlap{\text{~if~} \varepsilon\VDash f} \\ f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\ \end{cases} & - \1\ANDALT b &\equiv b & \1\OR b &\equiv \1 & - \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\ - && + \1 \FUSION f & \equiv \mathrlap{f\text{~if~}\varepsilon\nVDash f}\\ \STAR{} \ANDALT f &\equiv f & + && \STAR{} \OR f &\equiv \mathrlap{\STAR{}} & && - \STAR{} \CONCAT f &\equiv \STAR{}\text{~if~}\varepsilon\VDash f& \\ - && + \mathllap{\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} - \mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\ - \0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\ + \!\eword\text{~if~}\varepsilon\VDash{f} \\ + \0\!\phantom{\STAR{}}\text{~if~}\varepsilon\nVDash{f} \\ \end{cases} & - && + \mathllap{\eword}\AND f &\equiv f & + \eword\OR f &\equiv f \text{~if~} \varepsilon\VDash f& \eword \FUSION f &\equiv \0 & - \eword \CONCAT f &\equiv f\\ - f\AND f &\equiv f& + \mathllap{\eword \CONCAT f}&\equiv f\\ f\ANDALT f &\equiv f & + f\AND f &\equiv f& f\OR f &\equiv f& f\FUSION f&\equiv f\FSTAR{2}& f\CONCAT f&\equiv f\STAR{2}\\ - b_1 \AND b_2 &\equiv b_1\ANDALT b_2 & + b_1 \AND b_2 &\equiv \mathrlap{b_1\ANDALT b_2}& && && b_1:b_2 &\equiv b_1\ANDALT b_2 @@ -890,7 +890,7 @@ f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar 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}}\\ 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}}} +b\STAR{\mvar{i}..\mvar{j}}\FUSION b\STAR{\mvar{k}..\mvar{l}} &\equiv b\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 fe5770931..b905f4464 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -357,7 +357,16 @@ namespace spot break; case op::OrRat: neutral = ff(); - neutral2 = nullptr; + { + // If this OrRat contains an operand that accept [*0] but + // isn't [*0], then any [+0] can be removed. + bool eword_accepted = + std::find_if(v.begin(), v.end(), + [](const fnode* f) { + return f->accepts_eword() && !f->is_eword(); + }) != v.end(); + neutral2 = eword_accepted ? eword() : nullptr; + } abs = one_star(); abs2 = nullptr; weak_abs = one_plus(); diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index 27580cb34..92cc2719f 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -487,7 +487,8 @@ GF(a && GF(b) && c), G(F(a & c) & Fb) {first_match(1:e[*0..3])[*]}[]-> c, c W !e {first_match(first_match(a*;e);b)}[]->a, {first_match(a[*];e)}[]-> X(a | !b) {first_match(first_match(a*;e):b*)}[]->a, {first_match(a[*];e)}[]-> (a | !b) - +# issue 545 +{([*0]|a[*]|b);c}<>->d, {(a[*]|b);c}<>->d # issue 558 (was a false alarm, but still good to test) {(!b)[*3];b}!, !b & X(!b & X(!b & Xb)) {(!b)[+];b}!, !b & XFb