alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: add support for X[n], F[n:m] and G[n:m]

Browse source 
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
* spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
* spot/gen/formulas.cc: Use it.
* tests/core/sugar.test: New file.
* tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2018-07-05 17:29:25 +02:00
parent 2616ea7c80
commit e7aa334a71
10 changed files with 364 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

14
NEWS
View file

@ -1,6 +1,18 @@
New in spot 2.6.0.dev (not yet released)
Nothing yet.
- The LTL parser learned syntactic sugar for nested ranges of X
using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These
correspond to the next!, next_e!, and next_a! operators of PSL,
but we do not support those under these names currently.)
X[6]a = XXXXXXa
F[2:4]a = XX(a | X(a | Xa))
G[2:4]a = XX(a & X(a & Xa))
The corresponding constructors (for C++ and Python) are
formula::X(unsigned, formula)
formula::F(unsigned, unsigned, formula)
formula::G(unsigned, unsigned, formula)
New in spot 2.6 (2018-07-04)

12
doc/tl/tl.bib
View file

@ -1,3 +1,4 @@
@InProceedings{ babiak.12.tacas,
author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
@ -157,6 +158,17 @@
about this problem.}
}
@InProceedings{ jacobs.16.synt,
author = {Swen Jacobs and Felix Klein and Sebastian Schirmer},
title = {A High-Level {LTL} Synthesis Format: {TLSF} v1.1},
booktitle = {Proceedings Fifth Workshop on Synthesis (SYNT@CAV'16)},
pages = {112--132},
year = {2016},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {229},
doi = {10.4204/EPTCS.229.10}
}
@InProceedings{ manna.87.podc,
author = {Zohar Manna and Amir Pnueli},
title = {A hierarchy of temporal properties},

20
doc/tl/tl.tex
View file

@ -55,12 +55,15 @@
\DeclareMathOperator{\F}{\texttt{F}}
\DeclareMathOperator{\FALT}{\texttt{<>}}
\newcommand{\FREP}[1]{\texttt{F[#1]}}
\DeclareMathOperator{\G}{\texttt{G}}
\DeclareMathOperator{\GALT}{\texttt{[]}}
\newcommand{\GREP}[1]{\texttt{G[#1]}}
\newcommand{\U}{\mathbin{\texttt{U}}}
\newcommand{\R}{\mathbin{\texttt{R}}}
\newcommand{\RALT}{\mathbin{\texttt{V}}}
\DeclareMathOperator{\X}{\texttt{X}}
\newcommand{\XREP}[1]{\texttt{X[#1]}}
\DeclareMathOperator{\XALT}{\texttt{()}}
\newcommand{\M}{\mathbin{\texttt{M}}}
\newcommand{\W}{\mathbin{\texttt{W}}}
@ -512,6 +515,23 @@ operators using only $\X$ and one operator chosen among $\U$, $\W$,
$\M$,and $\R$. This could be useful to understand the operators $\R$,
$\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}
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.
\begin{align*}
\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}}) \\
\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}}) \\
\end{align*}
\subsection{Trivial Identities (Occur Automatically)}
\begin{align*}

5
spot/gen/formulas.cc
View file

@ -261,10 +261,7 @@ namespace spot
X_n(formula p, int n)
{
assert(n >= 0);
formula res = p;
while (n--)
res = X_(res);
return res;
return formula::X(n, p);
}
static formula

51
spot/parsetl/parsetl.yy
View file

@ -206,6 +206,7 @@ using namespace spot;
%token OP_W "weak until operator" OP_M "strong release operator"
%token OP_F "sometimes operator" OP_G "always operator"
%token OP_X "next operator" OP_NOT "not operator"
%token OP_XREP "X[.] operator" OP_FREP "F[.] operator" OP_GREP "G[.] operator"
%token OP_STAR "star operator" OP_BSTAR "bracket star operator"
%token OP_BFSTAR "bracket fusion-star operator"
%token OP_PLUS "plus operator"
@ -250,8 +251,8 @@ using namespace spot;
/* LTL operators. */
%right OP_U OP_R OP_M OP_W
%nonassoc OP_F OP_G
%nonassoc OP_X
%nonassoc OP_F OP_G OP_FREP OP_GREP
%nonassoc OP_X OP_XREP
/* High priority regex operator. */
%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS
@ -822,14 +823,60 @@ subformula: booleanatom
{ $$ = fnode::unop(op::F, $2); }
| OP_F error
{ missing_right_op($$, @1, "sometimes operator"); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4);
error_list.emplace_back(@1 + @3,
"F[n:m] expects two parameters");
}
| 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 OP_SQBKT_NUM OP_SQBKT_CLOSE
error
{ missing_right_op($$, @1 + @5, "F[.] operator"); }
| OP_FREP error_opt END_OF_INPUT
{ error_list.emplace_back(@$, "missing closing bracket for F[.]");
$$ = fnode::ff(); }
| OP_FREP error OP_SQBKT_CLOSE subformula %prec OP_FREP
{ error_list.emplace_back(@1 + @3,
"treating this F[.] as a simple F");
$$ = fnode::unop(op::F, $4); }
| OP_G subformula
{ $$ = fnode::unop(op::G, $2); }
| OP_G error
{ missing_right_op($$, @1, "always operator"); }
| 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_CLOSE subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4);
error_list.emplace_back(@1 + @3,
"G[n:m] expects two parameters");
}
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
error
{ missing_right_op($$, @1 + @5, "G[.] operator"); }
| OP_GREP error_opt END_OF_INPUT
{ error_list.emplace_back(@$, "missing closing bracket for G[.]");
$$ = fnode::ff(); }
| OP_GREP error OP_SQBKT_CLOSE subformula %prec OP_GREP
{ error_list.emplace_back(@1 + @3,
"treating this G[.] as a simple G");
$$ = fnode::unop(op::F, $4); }
| OP_X subformula
{ $$ = fnode::unop(op::X, $2); }
| OP_X error
{ missing_right_op($$, @1, "next operator"); }
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_XREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); }
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE error
{ missing_right_op($$, @1 + @3, "X[.] operator"); }
| OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP
{ error_list.emplace_back(@$, "treating this X[.] as a simple X");
$$ = fnode::unop(op::X, $4); }
| OP_XREP error_opt END_OF_INPUT
{ error_list.emplace_back(@$, "missing closing bracket for X[.]");
$$ = fnode::ff(); }
| OP_NOT subformula
{ $$ = fnode::unop(op::Not, $2); }
| OP_NOT error

16
spot/parsetl/scantl.ll
View file

@ -273,7 +273,21 @@ eol2 (\n\r)+|(\r\n)+
{ARROWL}|{DARROWL} BEGIN(0); return token::OP_IMPLIES;
{ARROWLR}|{DARROWLR} BEGIN(0); return token::OP_EQUIV;
/* <>, [], and () are used in Spin. */
/* TSLF-like syntactic sugar:
X[3]f = XXXf
F[2..4]f = XX(f | X(f | Xf))
G[2..4]f = XX(f & X(f & Xf))
We also have to deal with the Spin-like notation for G.
X[]f = XGf
*/
"X"[ \t\n]*"[]" yyless(1); return token::OP_X;
"F"[ \t\n]*"[]" yyless(1); return token::OP_F;
"G"[ \t\n]*"[]" yyless(1); return token::OP_G;
"X"[ \t\n]*"[" BEGIN(sqbracket); return token::OP_XREP;
"F"[ \t\n]*"[" BEGIN(sqbracket); return token::OP_FREP;
"G"[ \t\n]*"[" BEGIN(sqbracket); return token::OP_GREP;
/* <> (DIAMOND) and [] (BOX), are used in Spin.
() (CIRCLE) is not, but would make sense. */
"F"|{DIAMOND} BEGIN(0); return token::OP_F;
"G"|{BOX} BEGIN(0); return token::OP_G;
"U" BEGIN(0); return token::OP_U;

20
spot/tl/formula.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -1621,6 +1621,22 @@ namespace spot
}
}
const fnode*
fnode::nested_unop_range(op uo, op bo, unsigned min, unsigned max,
const fnode* f)
{
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)});
}
for (unsigned i = 0; i < min; ++i)
res = fnode::unop(uo, res);
return res;
}
std::ostream& fnode::dump(std::ostream& os) const
{

50
spot/tl/formula.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -155,6 +155,10 @@ namespace spot
static const fnode* bunop(op o, const fnode* f,
uint8_t min, uint8_t max = unbounded());
/// \see formula::nested_unop_range
static const fnode* nested_unop_range(op uo, op bo, unsigned min,
unsigned max, const fnode* f);
/// \see formula::kind
op kind() const
{
@ -887,11 +891,39 @@ namespace spot
SPOT_DEF_UNOP(X);
/// @}
/// \brief Construct an X[n]
///
/// X[3]f = XXXf
static formula X(unsigned level, const formula& f)
{
return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
}
/// \brief Construct an F
/// @{
SPOT_DEF_UNOP(F);
/// @}
/// \brief Construct F[n:m]
///
/// F[2:3] = XX(a | Xa)
///
/// 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)
{
return nested_unop_range(op::X, op::Or, min_level, max_level, f);
}
/// \brief Construct G[n:m]
///
/// G[2:3] = XX(a & Xa)
///
/// 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)
{
return nested_unop_range(op::X, op::And, min_level, max_level, f);
}
/// \brief Construct a G
/// @{
SPOT_DEF_UNOP(G);
@ -1173,6 +1205,20 @@ namespace spot
/// @}
#undef SPOT_DEF_BUNOP
/// \brief Nested operator construction (syntactic sugar).
///
/// Build between min and max nested uo, and chose between the
/// different numbers with bo.
///
/// For instance nested_unup_range(op::X, op::Or, 2, 4, a) returns
/// XX(a | X(a | Xa)).
static const formula nested_unop_range(op uo, op bo, unsigned min,
unsigned max, formula f)
{
return formula(fnode::nested_unop_range(uo, bo, min, max,
f.ptr_->clone()));
}
/// \brief Create a SERE equivalent to b[->min..max]
///
/// The operator does not exist: it is handled as sugar by the parser

1
tests/Makefile.am
View file

@ -264,6 +264,7 @@ TESTS_twa = \
core/sccsimpl.test \
core/sepsets.test \
core/split.test \
core/sugar.test \
core/dbacomp.test \
core/obligation.test \
core/wdba.test \

187
tests/core/sugar.test Executable file
View file

@ -0,0 +1,187 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# Syntactic sugar X[n] F[n:m] G[n:m]
. ./defs || exit 1
set -e
cat >ok.in <<EOF
X[4]a
G[2:4]a
G[4:2]a
F[2:4]a
F[4:2]a
X [4]a | b
G [2:4] a | b
G [4:2] a | b
F [2:4] a | b
F [4:2]a | F[2:2]b
F[]a|G[]b|X[]c
EOF
ltlfilt -F ok.in > ok.out
cat >expect <<EOF
XXXXa
XX(a & X(a & Xa))
XX(a & X(a & Xa))
XX(a | X(a | Xa))
XX(a | X(a | Xa))
b | XXXXa
b | XX(a & X(a & Xa))
b | XX(a & X(a & Xa))
b | XX(a | X(a | Xa))
XX(a | X(a | Xa)) | XXb
FGa | Gb | XGc
EOF
diff ok.out expect
cat >err.in <<EOF
F[
F[3:1]
F[3:1][2:1]
F[a
G[2:4]
G[2:]a
G[4]a
G[a
X[2
X[2]
X[2:4]a
X[a
EOF
num="number for square bracket operator"
numoreof="$num or end of formula"
sep="separator for square bracket operator"
undefined='$undefined'
ltlfilt -F err.in 2>err && exit 1
cat >expect2 <<EOF
ltlfilt:err.in:1: parse error:
>>> F[
^^
missing closing bracket for F[.]
ltlfilt:err.in:2: parse error:
>>> F[3:1]
^
syntax error, unexpected end of formula
>>> F[3:1]
^^^^^^
missing right operand for "F[.] operator"
ltlfilt:err.in:3: parse error:
>>> F[3:1][2:1]
^
syntax error, unexpected $undefined
>>> F[3:1][2:1]
^^^^^^
missing right operand for "F[.] operator"
>>> F[3:1][2:1]
^^^^^
ignoring trailing garbage
ltlfilt:err.in:4: parse error:
>>> F[a
^
syntax error, unexpected $undefined, expecting $numoreof
>>> F[a
^^^
missing closing bracket for F[.]
ltlfilt:err.in:5: parse error:
>>> G[2:4]
^
syntax error, unexpected end of formula
>>> G[2:4]
^^^^^^
missing right operand for "G[.] operator"
ltlfilt:err.in:6: parse error:
>>> G[2:]a
^
syntax error, unexpected closing bracket, expecting $num
>>> G[2:]a
^^^^^
treating this G[.] as a simple G
ltlfilt:err.in:7: parse error:
>>> G[4]a
^^^^
G[n:m] expects two parameters
ltlfilt:err.in:8: parse error:
>>> G[a
^
syntax error, unexpected $undefined, expecting $numoreof
>>> G[a
^^^
missing closing bracket for G[.]
ltlfilt:err.in:9: parse error:
>>> X[2
^
syntax error, unexpected end of formula, expecting closing bracket
>>> X[2
^^^
missing closing bracket for X[.]
ltlfilt:err.in:10: parse error:
>>> X[2]
^
syntax error, unexpected end of formula
>>> X[2]
^^^^
missing right operand for "X[.] operator"
ltlfilt:err.in:11: parse error:
>>> X[2:4]a
^
syntax error, unexpected $sep, expecting closing bracket
>>> X[2:4]a
^^^^^^^
treating this X[.] as a simple X
ltlfilt:err.in:12: parse error:
>>> X[a
^
syntax error, unexpected $undefined, expecting $numoreof
>>> X[a
^^^
missing closing bracket for X[.]
EOF
diff err expect2