diff --git a/NEWS b/NEWS index 0321826b1..e3560c1e7 100644 --- a/NEWS +++ b/NEWS @@ -58,6 +58,7 @@ New in spot 2.7.4.dev (not yet released) 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. + ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. - spot::relabel_apply() make 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 6db9c2ffe..b0c42ef48 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -88,6 +88,8 @@ \newcommand{\CONCAT}{\mathbin{\texttt{;}}} \newcommand{\DELAY}[1]{\mathbin{\texttt{\#\##1}}} \newcommand{\DELAYR}[1]{\mathbin{\texttt{\#\#[#1]}}} +\newcommand{\DELAYP}[1]{\mathbin{\texttt{\#\#[+]}}} +\newcommand{\DELAYS}[1]{\mathbin{\texttt{\#\#[*]}}} \newcommand{\0}{\texttt{0}} \newcommand{\1}{\texttt{1}} \newcommand{\STAR}[1]{\texttt{[*#1]}} @@ -779,7 +781,9 @@ omitted. 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 + {}\DELAYR{\mvar{i}..\mvar{j}} g &\equiv \STAR{\mvar{i}..\mvar{j}}\CONCAT g \\ + f \DELAYP{} g & \equiv f \DELAYR{1..} g & f \DELAYS{} g & \equiv f \DELAYR{0..} g \\ + \DELAYP{} g & \equiv \DELAYR{1..} g & \DELAYS{} g & \equiv \DELAYR{0..} g \end{align*} \subsection{Trivial Identities (Occur Automatically)} diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 7f353c31c..0d7e7dd87 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -232,6 +232,8 @@ using namespace spot; %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" +%token OP_DELAY_PLUS "##[+] operator" +%token OP_DELAY_STAR "##[*] operator" /* Priorities. */ @@ -240,7 +242,7 @@ using namespace spot; %left OP_CONCAT %left OP_FUSION -%left OP_DELAY_N OP_DELAY_OPEN +%left OP_DELAY_N OP_DELAY_OPEN OP_DELAY_PLUS OP_DELAY_STAR /* Logical operators. */ %right OP_IMPLIES OP_EQUIV @@ -451,7 +453,10 @@ delayargs: OP_DELAY_OPEN sqbracketargs { error_list. emplace_back(@$, "missing closing bracket for ##["); $$.min = $$.max = 1U; } - + | OP_DELAY_PLUS + { $$.min = 1; $$.max = fnode::unbounded(); } + | OP_DELAY_STAR + { $$.min = 0; $$.max = fnode::unbounded(); } atomprop: ATOMIC_PROP { diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 4c0a6cb11..53d971a81 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -233,6 +233,8 @@ eol2 (\n\r)+|(\r\n)+ } return token::OP_DELAY_N; } +"##[+]" BEGIN(0); return token::OP_DELAY_PLUS; +"##[*]" BEGIN(0); return token::OP_DELAY_STAR; "##[" BEGIN(sqbracket); return token::OP_DELAY_OPEN; /* PSL operators */ diff --git a/tests/core/sugar.test b/tests/core/sugar.test index 4666fe299..83fef3ef7 100755 --- a/tests/core/sugar.test +++ b/tests/core/sugar.test @@ -43,6 +43,8 @@ F[]a|G[]b|X[]c {a ##[:] b}|->e {a ##[:1] b}|->e {##[..3] b}|->e +{a ##[+] b}|->e +{##[*] b}|->e EOF ltlfilt -F ok.in > ok.out @@ -66,6 +68,8 @@ FGa | Gb | XGc {a:{[*];b}}[]-> e {a:{[*0..1];b}}[]-> e {[*0..3];b}[]-> e +{a;[*];b}[]-> e +{[*];b}[]-> e EOF diff ok.out expect