diff --git a/NEWS b/NEWS index c5f32f663..e6148b7ea 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 41bb87fde..e117adbba 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -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 @@ -979,21 +996,22 @@ to the PSL standard~\cite{psl.04.lrm,eisner.06.psl}. \begin{center} \begin{tabular}{clc} - assoc. & operators & priority \\ + assoc. & operators & priority \\ \midrule -right & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$ & \tikz[remember picture,baseline]\node (lowest){lowest}; \\ -left & $\CONCAT$ & \\ -left & $\FUSION$ & \\ -right & $\IMPLIES,\,\EQUIV$ & \\ -left & $\XOR$ & \\ -left & $\OR$ & \\ -left & $\AND,\,\ANDALT$ & \\ -right & $\U,\,\W,\,\M,\,\R$ & \\ - & $\F,\,\G$ & \\ - & $\X$ & \\ - & $\STAR{\mvar{i}..\mvar{j}},\,\PLUS,\,\FSTAR{\mvar{i}..\mvar{j}},\,\FPLUS,\,\EQUAL{\mvar{i}..\mvar{j}},\,\GOTO{\mvar{i}..\mvar{j}}$ & \\ - & $\NOT$ & \\ - & $\code{=0},\,\code{=1}$ & \tikz[remember picture,baseline]\node (highest){highest}; \\ +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$ & \\ +left & $\AND,\,\ANDALT$ & \\ +right & $\U,\,\W,\,\M,\,\R$ & \\ + & $\F,\,\G$ & \\ + & $\X$ & \\ + & $\STAR{\mvar{i}..\mvar{j}},\,\PLUS,\,\FSTAR{\mvar{i}..\mvar{j}},\,\FPLUS,\,\EQUAL{\mvar{i}..\mvar{j}},\,\GOTO{\mvar{i}..\mvar{j}}$ & \\ + & $\NOT$ & \\ + & $\code{=0},\,\code{=1}$ & \tikz[remember picture,baseline]\node (highest){highest}; \\ \end{tabular} \end{center} \begin{tikzpicture}[remember picture,overlay,>=stealth',semithick] diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index d32535342..3a19b2e6a 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -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 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,7 +247,8 @@ 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 + + /* 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 U/R/M/W/F/G/X are not used in SERE). */ @@ -267,7 +271,7 @@ using namespace spot; %type subformula atomprop booleanatom sere lbtformula boolformula %type bracedsere parenthesedsubformula -%type starargs fstarargs equalargs sqbracketargs gotoargs +%type starargs fstarargs equalargs sqbracketargs gotoargs delayargs %destructor { delete $$; } %destructor { $$->destroy(); } @@ -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) diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 2d5f8b8ac..182e6e044 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -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; diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 707c62d0f..b27a9b2c0 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -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()); diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 113d32ac5..738350b9d 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -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. /// diff --git a/tests/core/sugar.test b/tests/core/sugar.test index e742f2bbc..4666fe299 100755 --- a/tests/core/sugar.test +++ b/tests/core/sugar.test @@ -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 . -# 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 <>> {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