From 58389bdb8048798feed88f700f19630fcc22807d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 2 Jun 2019 14:36:07 +0200 Subject: [PATCH] tl: extend F[n:m] and G[n:m] to the case of m=$ Suggested by Victor Khomenko. * spot/tl/formula.cc, spot/tl/formula.hh, spot/parsetl/parsetl.yy: Implement this. * NEWS, doc/tl/tl.tex: Document it. * tests/core/sugar.test, tests/python/ltlparse.py: Add some tests. --- NEWS | 3 +++ doc/tl/tl.tex | 8 +++++--- spot/parsetl/parsetl.yy | 8 ++++++++ spot/tl/formula.cc | 13 ++++++++----- spot/tl/formula.hh | 10 ++++++++-- tests/core/sugar.test | 18 +++++++++++++----- tests/python/ltlparse.py | 13 ++++++++++++- 7 files changed, 57 insertions(+), 16 deletions(-) diff --git a/NEWS b/NEWS index d4dc4daf8..06a736191 100644 --- a/NEWS +++ b/NEWS @@ -93,6 +93,9 @@ New in spot 2.7.4.dev (not yet released) terms of the existing PSL operators. ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. + - The F[n:m] and G[n:m] operators introduced in Spot 2.7 now + support the case where m=$. + - spot::relabel_apply() makes it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b358ec940..9598aaa33 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -523,7 +523,7 @@ $\M$, and $\W$ if you are only familiar with $\X$ and $\U$. \subsection{Syntactic Sugar} The syntax on the left is equivalent to the syntax on the right. -These rewritings taken from the syntax of TSLF~\citep{jacobs.16.synt} +Some of rewritings taken from the syntax of TSLF~\citep{jacobs.16.synt} are performed from left to right when parsing a formula. They express the fact that some formula $f$ has to be true in $n$ steps, or at some or all times between $n$ and $m$ steps. @@ -532,9 +532,11 @@ or all times between $n$ and $m$ steps. \XREP{\mvar{n}} f & \equiv \underbrace{\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occurrences of~}\X}} f \\ \FREP{\mvar{n}:\mvar{m}}f - & \equiv \underbrace{\vphantom{(}\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occ. of~}\X}} (f \OR \underbrace{\X(f \OR \X(\ldots \OR \X f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\X}}) \\ + & \equiv \underbrace{\vphantom{(}\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occ. of~}\X}} (f \OR \underbrace{\X(f \OR \X(\ldots \OR \X f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\X}}) + & \FREP{\mvar{n}:}f &\equiv \XREP{\mvar{n}}\F{}f\\ \GREP{\mvar{n}:\mvar{m}}f - & \equiv \underbrace{\vphantom{(}\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occ. of~}\X}} (f \AND \underbrace{\X(f \AND \X(\ldots \AND \X f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\X}}) \\ + & \equiv \underbrace{\vphantom{(}\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occ. of~}\X}} (f \AND \underbrace{\X(f \AND \X(\ldots \AND \X f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\X}}) + & \GREP{\mvar{n}:}f &\equiv \XREP{\mvar{n}}\G{}f\\ \end{align*} \subsection{Trivial Identities (Occur Automatically)} diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 64c97ae1e..e6dc18323 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -887,6 +887,10 @@ subformula: booleanatom | OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_FREP { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $4, $6); } + | OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE + subformula %prec OP_FREP + { $$ = fnode::nested_unop_range(op::X, op::Or, $2, + fnode::unbounded(), $5); } | OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE error { missing_right_op($$, @1 + @5, "F[.] operator"); } @@ -904,6 +908,10 @@ subformula: booleanatom | OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_GREP { $$ = fnode::nested_unop_range(op::X, op::And, $2, $4, $6); } + | OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE + subformula %prec OP_GREP + { $$ = fnode::nested_unop_range(op::X, op::And, $2, + fnode::unbounded(), $5); } | OP_GREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_GREP { $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4); error_list.emplace_back(@1 + @3, diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index b72a61a34..b0840fe0b 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1657,11 +1657,14 @@ namespace spot const fnode* res = f; if (max < min) std::swap(min, max); - for (unsigned i = min; i < max; ++i) - { - const fnode* a = f->clone(); - res = fnode::multop(bo, {a, fnode::unop(uo, res)}); - } + if (max != unbounded()) + for (unsigned i = min; i < max; ++i) + { + const fnode* a = f->clone(); + res = fnode::multop(bo, {a, fnode::unop(uo, res)}); + } + else + res = fnode::unop(bo == op::Or ? op::F : op::G, res); for (unsigned i = 0; i < min; ++i) res = fnode::unop(uo, res); return res; diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index f45681103..7a70a9d97 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -906,7 +906,8 @@ namespace spot /// \brief Construct F[n:m] /// - /// F[2:3] = XX(a | Xa) + /// F[2:3]a = XX(a | Xa) + /// F[2:$]a = XXFa /// /// This syntax is from TSLF; the operator is called next_e![n..m] in PSL. static formula F(unsigned min_level, unsigned max_level, const formula& f) @@ -916,7 +917,8 @@ namespace spot /// \brief Construct G[n:m] /// - /// G[2:3] = XX(a & Xa) + /// G[2:3]a = XX(a & Xa) + /// G[2:$]a = XXGa /// /// This syntax is from TSLF; the operator is called next_a![n..m] in PSL. static formula G(unsigned min_level, unsigned max_level, const formula& f) @@ -1217,6 +1219,10 @@ namespace spot /// /// For instance nested_unup_range(op::X, op::Or, 2, 4, a) returns /// XX(a | X(a | Xa)). + /// + /// For `max==unbounded()`, \a uo is repeated \a min times, and + /// its child is set to `F(a)` if \a bo is `op::Or` or to `G(a)` + /// otherwise. static const formula nested_unop_range(op uo, op bo, unsigned min, unsigned max, formula f) { diff --git a/tests/core/sugar.test b/tests/core/sugar.test index 12cdfe0a2..cbdf7ec84 100755 --- a/tests/core/sugar.test +++ b/tests/core/sugar.test @@ -30,9 +30,13 @@ G[2:4]a G[4:2]a F[2:4]a F[4:2]a +F[2:$]a +F[2..]a X [4]a | b G [2:4] a | b G [4:2] a | b +G [2:] a | b +G [2..] a | b F [2:4] a | b F [4:2]a | F[2:2]b F[]a|G[]b|X[]c @@ -61,9 +65,13 @@ XX(a & X(a & Xa)) XX(a & X(a & Xa)) XX(a | X(a | Xa)) XX(a | X(a | Xa)) +XXFa +XXFa b | XXXXa b | XX(a & X(a & Xa)) b | XX(a & X(a & Xa)) +b | XXGa +b | XXGa b | XX(a | X(a | Xa)) XX(a | X(a | Xa)) | XXb FGa | Gb | XGc @@ -93,7 +101,7 @@ F[3:1] F[3:1][2:1] F[a G[2:4] -G[2:]a +G[2:.]a G[4]a G[a X[2 @@ -163,12 +171,12 @@ syntax error, unexpected end of formula missing right operand for "G[.] operator" ltlfilt:err.in:6: parse error: ->>> G[2:]a +>>> G[2:.]a ^ -syntax error, unexpected closing bracket, expecting $num +syntax error, unexpected $undefined, expecting closing bracket ->>> G[2:]a - ^^^^^ +>>> G[2:.]a + ^^^^^^ treating this G[.] as a simple G ltlfilt:err.in:7: parse error: diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index a4585134a..29404f0c9 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009-2012, 2014-2017 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2017, 2019 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 @@ -199,3 +199,14 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""), del f9 assert spot.fnode_instances_check() + +f = spot.formula_F(2, 4, spot.formula_ap("a")) +assert f == spot.formula("XX(a | X(a | X(a)))") +f = spot.formula_G(2, 4, spot.formula_ap("a")) +assert f == spot.formula("XX(a & X(a & X(a)))") +f = spot.formula_X(2, spot.formula_ap("a")) +assert f == spot.formula("XX(a)") +f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a")) +assert f == spot.formula("XXG(a)") +f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a")) +assert f == spot.formula("XXF(a)")