Commit 5939d6f4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add back the '*' syntax for And.

This somehow revert changes from 2010-01-30 which killed this use of
star to make room for the Kleen star.  Here we only allow '*' in the
temporal formula, so that it can still be the Kleen star in SERE.  The
motivation for '*' available as And is better compatibility with Wring
and VIS.

* src/ltlparse/ltlscan.ll: Distinguish * from [*].
* src/ltlparse/ltlparse.yy: Allows * to be used as AND between
temporal formulae.
* src/ltltest/equals.test, src/ltltest/parse.test: Add a few
tests.
* doc/tl/tl.tex: Document it.
parent 60ec3ace
......@@ -83,6 +83,7 @@
\newcommand{\1}{\texttt{1}}
\newcommand{\STAR}[1]{\texttt{[*#1]}}
\newcommand{\STARALT}{\texttt{*}}
\newcommand{\STARBIN}{\mathbin{\texttt{*}}}
\newcommand{\EQUAL}[1]{\texttt{[=#1]}}
\newcommand{\GOTO}[1]{\texttt{[->#1]}}
\newcommand{\PLUS}{\texttt{[+]}}
......@@ -361,12 +362,17 @@ following Boolean operators:
\cmidrule(r){1-5} \cmidrule(l){6-7}
negation & $\NOT f$ & $\NOTALT f$ & & & $\lnot$ \uni{00AC} \\
disjunction & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ & $\lor$ \uni{2228} & $\cup$ \uni{222A}\\
conjunction & $f\AND g$ & $f\ANDALT g$ & $f\ANDALTT g$ & & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
conjunction & $f\AND g$ & $f\ANDALT g$ & $f\ANDALTT g$ & $f\STARBIN g$\rlap{\footnotemark} & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
implication & $f\IMPLIES g$ & $f\IMPLIESALT g$ & $f\IMPLIESALTT g$ & & $\limplies$ \uni{2192} & $\rightarrow$ \uni{27F6}, $\Rightarrow$ \uni{21D2} \uni{27F9} \\
exclusion & $f\XOR g$ & $f\XORALT g$ & & & $\oplus$ \uni{2295} \\
equivalence & $f\EQUIV g$ & $f\EQUIVALT g$ & $f\EQUIVALTT g$ & & $\liff$ \uni{2194} & $\Leftrightarrow$ \uni{21D4}\\
\end{tabular}
\end{center}
\footnotetext{The $\STARALT$-form of the conjunction operator
(allowing better compatibility with Wring and VIS) may only used in
temporal formul\ae. Boolean expressions that occur inside SERE (see
Section~\ref{sec:sere}) may not use this form because the $\STARALT$
symbol is used as the Kleen star.}
Additionally, an atomic proposition $a$ can be negated using the
syntax \samp{$a$=0}, which is equivalent to \samp{$\NOT a$}. Also
......@@ -558,7 +564,7 @@ Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv})
those two were chosen because they are easier to translate in a
tableau construction~\cite[Fig.~11]{duret.11.vecos}.
\section{SERE Operators}
\section{SERE Operators}\label{sec:sere}
The ``SERE'' acronym will be translated to different word depending on
the source. It can mean either ``\textit{Sequential Extended Regular
......
......@@ -104,7 +104,8 @@ using namespace spot::ltl;
%token OP_U "until operator" OP_R "release operator"
%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" OP_STAR "star operator"
%token OP_X "next operator" OP_NOT "not operator"
%token OP_STAR "star operator" OP_BSTAR "bracket star operator"
%token OP_PLUS "plus operator"
%token OP_STAR_OPEN "opening bracket for star operator"
%token OP_EQUAL_OPEN "opening bracket for equal operator"
......@@ -137,13 +138,19 @@ using namespace spot::ltl;
%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
U/R/M/W/F/G/X are not used in SERE). */
%left OP_STAR
/* LTL operators. */
%right OP_U OP_R OP_M OP_W
%nonassoc OP_F OP_G
%nonassoc OP_X
/* High priority regex operator. */
%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN
%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN
/* Not has the most important priority after Wring's `=0' and `=1'. */
%nonassoc OP_NOT
......@@ -248,7 +255,9 @@ gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
"missing closing bracket for goto operator"));
$$.min = $$.max = 0U; }
starargs: OP_STAR
kleen_star: OP_STAR | OP_BSTAR
starargs: kleen_star
{ $$.min = 0U; $$.max = bunop::unbounded; }
| OP_PLUS
{ $$.min = 1U; $$.max = bunop::unbounded; }
......@@ -606,6 +615,10 @@ subformula: booleanatom
{ $$ = multop::instance(multop::And, $1, $3); }
| subformula OP_SHORT_AND error
{ missing_right_binop($$, $1, @2, "and operator"); }
| subformula OP_STAR subformula
{ $$ = multop::instance(multop::And, $1, $3); }
| subformula OP_STAR error
{ missing_right_binop($$, $1, @2, "and operator"); }
| subformula OP_OR subformula
{ $$ = multop::instance(multop::Or, $1, $3); }
| subformula OP_OR error
......
......@@ -106,7 +106,8 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
{DIAMOND}{DARROWL} BEGIN(0); return token::OP_ECONCAT_NONO;
";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION;
"*"|"[*]" BEGIN(0); return token::OP_STAR;
"*" BEGIN(0); return token::OP_STAR;
"[*]" BEGIN(0); return token::OP_BSTAR;
"[+]" BEGIN(0); return token::OP_PLUS;
"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN;
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
......@@ -141,7 +142,8 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
/* & and | come from Spin. && and || from LTL2BA.
/\, \/, and xor are from LBTT.
--> and <--> come from Goal. */
--> and <--> come from Goal.
+,*,^ are from Wring. */
"||"|"|"|"+"|"\\/"|"∨"|"∪" BEGIN(0); return token::OP_OR;
"&&"|"/\\"|"∧"|"∩" BEGIN(0); return token::OP_AND;
"&" BEGIN(0); return token::OP_SHORT_AND;
......
......@@ -51,6 +51,7 @@ run 0 ../equals 'a & a & true' 'a'
run 0 ../equals 'a & false & a' 'false'
run 0 ../equals 'a | false | a' 'a'
run 0 ../equals 'true | a | a' 'true'
run 0 ../equals 'Ga=1*Gb=0' '(G(a)) & (G(!b))'
# other formulae which are not
run 1 ../equals 'a' 'b'
......
#! /bin/sh
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -38,7 +38,7 @@ for f in \
'p11011' \
'(p11011)' \
'a & b' \
'a & _b12' \
'a * _b12' \
'a && .b.' \
'a + b' \
'a3214 | b' \
......@@ -73,6 +73,8 @@ for f in \
'a R ome V anille' \
'p=0Uq=1' \
'((p=1Rq=1)+p=0)UXq=0' \
'((p=1Rq=1)*p=0)UXq=0' \
'(Gq=1*Fp=0)UXq=0' \
'((p=1Mq=1)Wx+p=0)RXq=0' \
'((p=1Vq=1)Rx+p=0)WXq=0' \
'((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)'
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment