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.
This commit is contained in:
Alexandre Duret-Lutz
parent
74786324f4
commit
58389bdb80
7 changed files with 57 additions and 16 deletions
3
NEWS
3
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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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)}
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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)")
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue