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

tl: add support for ##n and ##[i:j] from SVA

Browse source 
* spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-04 21:50:59 +02:00
parent 00f70257db
commit 60d488b30c
7 changed files with 213 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -46,6 +46,12 @@ New in spot 2.7.4.dev (not yet released)
acceptance condition. The output can be alternating only if the
input was alternating.
- The parser for SERE learned to recognize the ##n and ##[i:j]
operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another
way to write {[*2];a:b[+];c;1;e}, and {a ##[i:j] b} is parsed as
{a:{[*i..j];b}}. The formula::sugar_delay() function implement
this SVA operator in terms of the existing PSL operators.
New in spot 2.7.4 (2019-04-27)
Bugs fixed:

18
doc/tl/tl.tex
View file

@ -86,6 +86,8 @@
\newcommand{\ANDALTT}{\mathbin{\texttt{/\char`\\}}}
\newcommand{\FUSION}{\mathbin{\texttt{:}}}
\newcommand{\CONCAT}{\mathbin{\texttt{;}}}
\newcommand{\DELAY}[1]{\mathbin{\texttt{\#\##1}}}
\newcommand{\DELAYR}[1]{\mathbin{\texttt{\#\#[#1]}}}
\newcommand{\0}{\texttt{0}}
\newcommand{\1}{\texttt{1}}
\newcommand{\STAR}[1]{\texttt{[*#1]}}
@ -754,6 +756,21 @@ it for output. $b$ must be a Boolean formula.
\PLUS{} &\equiv \1\STAR{1..}
\end{align*}
The following adds input support for the SVA concatenation (or delay)
operator. The simplest equivalence are that $f \DELAY{0} g$,
$f \DELAY{1} g$, $f \DELAY{2} g$ mean respectively $f \FUSION g$,
$f \CONCAT g$, and $f \CONCAT \1\CONCAT g$, but the delay can be a
range, and $f$ can be omitted.
\begin{align*}
f\DELAY{\mvar{i}} g &\equiv f\DELAYR{\mvar{i}..\mvar{i}} g & {}\DELAY{\mvar{i}} g &\equiv {}\DELAYR{\mvar{i}..\mvar{i}} g\\
f\DELAYR{..} g &\equiv f\FUSION\{\STAR{}\CONCAT g\} & f\DELAYR{\mvar{i}..} g &\equiv f\FUSION\{\STAR{\mvar{i}..}\CONCAT g\} \\
f\DELAYR{..\mvar{j}} g &\equiv f\FUSION\{\STAR{0..\mvar{j}}\CONCAT g\} &
f\DELAYR{\mvar{i}..\mvar{j}} g &\equiv f\FUSION\{\STAR{\mvar{i}..\mvar{j}}\CONCAT g\} \\
{}\DELAYR{..} g &\equiv \STAR{}\CONCAT g & {}\DELAYR{\mvar{i}..} g &\equiv \STAR{\mvar{i}..}\CONCAT g \\
{}\DELAYR{..\mvar{j}} g &\equiv \STAR{0..\mvar{j}}\CONCAT g &
{}\DELAYR{\mvar{i}..\mvar{j}} g &\equiv \STAR{\mvar{i}..\mvar{j}}\CONCAT g
\end{align*}
\subsection{Trivial Identities (Occur Automatically)}
The following identities also hold if $j$ or $l$ are missing (assuming
@ -984,6 +1001,7 @@ to the PSL standard~\cite{psl.04.lrm,eisner.06.psl}.
right & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$ & \tikz[remember picture,baseline]\node (lowest){lowest}; \\
left & $\CONCAT$ & \\
left & $\FUSION$ & \\
left & $\DELAY{\mvar{i}},\,\DELAYR{\mvar{i}..\mvar{j}}$ & \\
right & $\IMPLIES,\,\EQUIV$ & \\
left & $\XOR$ & \\
left & $\OR$ & \\

52
spot/parsetl/parsetl.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2009-2018 Laboratoire de Recherche et Développement
** Copyright (C) 2009-2019 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -229,6 +229,8 @@ using namespace spot;
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
%token END_OF_INPUT "end of formula"
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
%token <num> OP_DELAY_N "SVA delay operator"
%token OP_DELAY_OPEN "opening bracket for SVA delay operator"
/* Priorities. */
@ -237,6 +239,7 @@ using namespace spot;
%left OP_CONCAT
%left OP_FUSION
%left OP_DELAY_N OP_DELAY_OPEN
/* Logical operators. */
%right OP_IMPLIES OP_EQUIV
@ -244,6 +247,7 @@ using namespace spot;
%left OP_XOR
%left OP_AND OP_SHORT_AND
/* OP_STAR can be used as an AND when occurring in some LTL formula in
Wring's syntax (so it has to be close to OP_AND), and as a Kleen
Star in SERE (so it has to be close to OP_BSTAR -- luckily
@ -267,7 +271,7 @@ using namespace spot;
%type <ltl> subformula atomprop booleanatom sere lbtformula boolformula
%type <ltl> bracedsere parenthesedsubformula
%type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs
%type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs delayargs
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
@ -437,6 +441,16 @@ equalargs: OP_EQUAL_OPEN sqbracketargs
emplace_back(@$, "missing closing bracket for equal operator");
$$.min = $$.max = 0U; }
delayargs: OP_DELAY_OPEN sqbracketargs
{ $$ = $2; }
| OP_DELAY_OPEN error OP_SQBKT_CLOSE
{ error_list.emplace_back(@$, "treating this delay block as ##1");
$$.min = $$.max = 1U; }
| OP_DELAY_OPEN error_opt END_OF_INPUT
{ error_list.
emplace_back(@$, "missing closing bracket for ##[");
$$.min = $$.max = 1U; }
atomprop: ATOMIC_PROP
{
@ -520,6 +534,40 @@ sere: booleanatom
{ $$ = fnode::multop(op::Fusion, {$1, $3}); }
| sere OP_FUSION error
{ missing_right_binop($$, $1, @2, "fusion operator"); }
| OP_DELAY_N sere
{ $$ = formula::sugar_delay(formula::tt(), formula($2),
$1, $1).to_node_(); }
| OP_DELAY_N error
{ missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); }
| sere OP_DELAY_N sere
{ $$ = formula::sugar_delay(formula($1), formula($3),
$2, $2).to_node_(); }
| sere OP_DELAY_N error
{ missing_right_binop($$, $1, @2, "SVA delay operator"); }
| delayargs sere %prec OP_DELAY_OPEN
{
if ($1.max < $1.min)
{
error_list.emplace_back(@1, "reversed range");
std::swap($1.max, $1.min);
}
$$ = formula::sugar_delay(formula::tt(), formula($2),
$1.min, $1.max).to_node_();
}
| delayargs error
{ missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); }
| sere delayargs sere %prec OP_DELAY_OPEN
{
if ($2.max < $2.min)
{
error_list.emplace_back(@1, "reversed range");
std::swap($2.max, $2.min);
}
$$ = formula::sugar_delay(formula($1), formula($3),
$2.min, $2.max).to_node_();
}
| sere delayargs error
{ missing_right_binop($$, $1, @2, "SVA delay operator"); }
| starargs
{
if ($1.max < $1.min)

16
spot/parsetl/scantl.ll
View file

@ -217,6 +217,22 @@ eol2 (\n\r)+|(\r\n)+
/* ~ comes from Goal, ! from everybody else */
{NOT} BEGIN(0); return token::OP_NOT;
/* SVA operators */
"##"[0-9]+ {
errno = 0;
unsigned long n = strtoul(yytext + 2, 0, 10);
yylval->num = n;
if (errno || yylval->num != n)
{
error_list.push_back(
spot::one_parse_error(*yylloc,
"value too large ignored"));
yylval->num = 1;
}
return token::OP_DELAY_N;
}
"##[" BEGIN(sqbracket); return token::OP_DELAY_OPEN;
/* PSL operators */
{BOXARROW} BEGIN(0); return token::OP_UCONCAT;
{DIAMOND}{ARROWL} BEGIN(0); return token::OP_ECONCAT;

15
spot/tl/formula.cc
View file

@ -1743,6 +1743,21 @@ namespace spot
return Concat({Star(Concat({s, b}), min, max), s});
}
formula formula::sugar_delay(const formula& a, const formula& b,
unsigned min, unsigned max)
{
// In general
// a ##[min:max] b = a:(1[*min:max];b)
// however if min>=1 we prefer the following rule
// a ##[min:max] b = a;1[*min-1:max-1];b
if (min == 0)
return Fusion({a, Concat({Star(tt(), min, max), b})});
--min;
if (max != unbounded())
--max;
return Concat({a, Star(tt(), min, max), b});
}
int atomic_prop_cmp(const fnode* f, const fnode* g)
{
return strverscmp(f->ap_name().c_str(), g->ap_name().c_str());

25
spot/tl/formula.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -1220,18 +1220,29 @@ namespace spot
/// \brief Create a SERE equivalent to b[->min..max]
///
/// The operator does not exist: it is handled as sugar by the parser
/// and the printer. This functions is used by the parser to create
/// the equivalent SERE.
/// The operator does not exist: it is handled as syntactic sugar
/// by the parser and the printer. This function is used by the
/// parser to create the equivalent SERE.
static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
/// Create the SERE b[=min..max]
///
/// The operator does not exist: it is handled as sugar by the parser
/// and the printer. This functions is used by the parser to create
/// the equivalent SERE.
/// The operator does not exist: it is handled as syntactic sugar
/// by the parser and the printer. This function is used by the
/// parser to create the equivalent SERE.
static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
/// Create the SERE a ##[n:m] b
///
/// This ##[n:m] operator comes from SVA. When n=m, it is simply
/// written ##n.
///
/// The operator does not exist in Spot it is handled as syntactic
/// sugar by the parser. This function is used by the parser to
/// create the equivalent SERE.
static formula sugar_delay(const formula& a, const formula& b,
unsigned min, unsigned max);
#ifndef SWIG
/// \brief Return the underlying pointer to the formula.
///

78
tests/core/sugar.test
View file

@ -1,7 +1,7 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -19,7 +19,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# Syntactic sugar X[n] F[n:m] G[n:m]
# Syntactic sugar X[n] F[n:m] G[n:m] ##n ##[i..j]
. ./defs || exit 1
set -e
@ -36,6 +36,13 @@ G [4:2] a | b
F [2:4] a | b
F [4:2]a | F[2:2]b
F[]a|G[]b|X[]c
{a ##0 b ##1 c ##2 d}|->e
{(##2 a)[*] ##1 b}|->e
{a ##[0:3] b}|->e
{a ##[1..] b}|->e
{a ##[:] b}|->e
{a ##[:1] b}|->e
{##[..3] b}|->e
EOF
ltlfilt -F ok.in > ok.out
@ -52,6 +59,13 @@ b | XX(a & X(a & Xa))
b | XX(a | X(a | Xa))
XX(a | X(a | Xa)) | XXb
FGa | Gb | XGc
{{a && b};c;1;d}[]-> e
{{[*2];a}[*];b}[]-> e
{a:{[*0..3];b}}[]-> e
{a;[*];b}[]-> e
{a:{[*];b}}[]-> e
{a:{[*0..1];b}}[]-> e
{[*0..3];b}[]-> e
EOF
diff ok.out expect
@ -70,12 +84,20 @@ X[2
X[2]
X[2:4]a
X[a
{a ## b}
{a ##7}
{a ##[::] b}
{a ##[2:1] b}
{a ##[1:2]}
{##[1:2]}
EOF
# Work around our 80col restriction.
num="number for square bracket operator"
numoreof="$num or end of formula"
sep="separator for square bracket operator"
undefined='$undefined'
closingbkt='square bracket operator, expecting closing bracket'
ltlfilt -F err.in 2>err && exit 1
cat >expect2 <<EOF
@ -183,5 +205,55 @@ syntax error, unexpected $undefined, expecting $numoreof
^^^
missing closing bracket for X[.]
ltlfilt:err.in:13: parse error:
>>> {a ## b}
^
syntax error, unexpected $undefined
>>> {a ## b}
^^^^
ignoring this
ltlfilt:err.in:14: parse error:
>>> {a ##7}
^
syntax error, unexpected closing brace
>>> {a ##7}
^^^
missing right operand for "SVA delay operator"
ltlfilt:err.in:15: parse error:
>>> {a ##[::] b}
^
syntax error, unexpected separator for $closingbkt
>>> {a ##[::] b}
^^^^^^
treating this delay block as ##1
ltlfilt:err.in:16: parse error:
>>> {a ##[2:1] b}
^
reversed range
ltlfilt:err.in:17: parse error:
>>> {a ##[1:2]}
^
syntax error, unexpected closing brace
>>> {a ##[1:2]}
^^^^^^^
missing right operand for "SVA delay operator"
ltlfilt:err.in:18: parse error:
>>> {##[1:2]}
^
syntax error, unexpected closing brace
>>> {##[1:2]}
^^^^^^^
missing right operand for "SVA delay operator"
EOF
diff err expect2