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

tl: add support for ##[+] and ##[*]

Browse source 
Suggested by Victor Khomenko.

* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Implement them.
* NEWS, doc/tl/tl.tex: Document them.
* tests/core/sugar.test: Add a couple of tests.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-18 11:59:27 +02:00
parent b726d78cbd
commit f476483f4a
5 changed files with 19 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -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 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 {a:{[*i..j];b}}. The formula::sugar_delay() function implement
this SVA operator in terms of the existing PSL operators. 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 - spot::relabel_apply() make it easier to reverse the effect
of spot::relabel() or spot::relabel_bse() on formula. of spot::relabel() or spot::relabel_bse() on formula.

6
doc/tl/tl.tex
View file

@ -88,6 +88,8 @@
\newcommand{\CONCAT}{\mathbin{\texttt{;}}} \newcommand{\CONCAT}{\mathbin{\texttt{;}}}
\newcommand{\DELAY}[1]{\mathbin{\texttt{\#\##1}}} \newcommand{\DELAY}[1]{\mathbin{\texttt{\#\##1}}}
\newcommand{\DELAYR}[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{\0}{\texttt{0}}
\newcommand{\1}{\texttt{1}} \newcommand{\1}{\texttt{1}}
\newcommand{\STAR}[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\} \\ 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{..} 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{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*} \end{align*}
\subsection{Trivial Identities (Occur Automatically)} \subsection{Trivial Identities (Occur Automatically)}

9
spot/parsetl/parsetl.yy
View file

@ -232,6 +232,8 @@ using namespace spot;
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" %token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
%token <num> OP_DELAY_N "SVA delay operator" %token <num> OP_DELAY_N "SVA delay operator"
%token OP_DELAY_OPEN "opening bracket for SVA delay operator" %token OP_DELAY_OPEN "opening bracket for SVA delay operator"
%token OP_DELAY_PLUS "##[+] operator"
%token OP_DELAY_STAR "##[*] operator"
/* Priorities. */ /* Priorities. */
@ -240,7 +242,7 @@ using namespace spot;
%left OP_CONCAT %left OP_CONCAT
%left OP_FUSION %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. */ /* Logical operators. */
%right OP_IMPLIES OP_EQUIV %right OP_IMPLIES OP_EQUIV
@ -451,7 +453,10 @@ delayargs: OP_DELAY_OPEN sqbracketargs
{ error_list. { error_list.
emplace_back(@$, "missing closing bracket for ##["); emplace_back(@$, "missing closing bracket for ##[");
$$.min = $$.max = 1U; } $$.min = $$.max = 1U; }
| OP_DELAY_PLUS
{ $$.min = 1; $$.max = fnode::unbounded(); }
| OP_DELAY_STAR
{ $$.min = 0; $$.max = fnode::unbounded(); }
atomprop: ATOMIC_PROP atomprop: ATOMIC_PROP
{ {

2
spot/parsetl/scantl.ll
View file

@ -233,6 +233,8 @@ eol2 (\n\r)+|(\r\n)+
} }
return token::OP_DELAY_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; "##[" BEGIN(sqbracket); return token::OP_DELAY_OPEN;
/* PSL operators */ /* PSL operators */

4
tests/core/sugar.test
View file

@ -43,6 +43,8 @@ F[]a|G[]b|X[]c
{a ##[:] b}|->e {a ##[:] b}|->e
{a ##[:1] b}|->e {a ##[:1] b}|->e
{##[..3] b}|->e {##[..3] b}|->e
{a ##[+] b}|->e
{##[*] b}|->e
EOF EOF
ltlfilt -F ok.in > ok.out ltlfilt -F ok.in > ok.out
@ -66,6 +68,8 @@ FGa | Gb | XGc
{a:{[*];b}}[]-> e {a:{[*];b}}[]-> e
{a:{[*0..1];b}}[]-> e {a:{[*0..1];b}}[]-> e
{[*0..3];b}[]-> e {[*0..3];b}[]-> e
{a;[*];b}[]-> e
{[*];b}[]-> e
EOF EOF
diff ok.out expect diff ok.out expect