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

Document recognized utf8 characters.

Browse source 
* doc/tl/tl.tex: Here.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-28 21:02:43 +02:00
parent 7e4787da22
commit 5eae815a1c
1 changed files with 41 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

68
doc/tl/tl.tex
View file

@ -11,6 +11,8 @@
\usepackage{xspace} \usepackage{xspace}
\usepackage{dsfont} \usepackage{dsfont}
\usepackage{mathabx} % vDash \usepackage{mathabx} % vDash
\usepackage{wasysym}
\usepackage{stmaryrd}
\usepackage{showlabels} \usepackage{showlabels}
\usepackage{tabulary} \usepackage{tabulary}
\usepackage[numbers]{natbib} \usepackage[numbers]{natbib}
@ -36,6 +38,8 @@
\newcommand{\spottodo}[2][]{\stodo[color=green!40,caption={#2},#1]{#2}} \newcommand{\spottodo}[2][]{\stodo[color=green!40,caption={#2},#1]{#2}}
\newcommand{\ltltodo}[2][]{\stodo[color=red!40,caption={#2},#1]{#2}} \newcommand{\ltltodo}[2][]{\stodo[color=red!40,caption={#2},#1]{#2}}
\newcommand{\uni}[1]{\texttt{\small U+#1}}
%% ---------------------- %% %% ---------------------- %%
%% Mathematical symbols. %% %% Mathematical symbols. %%
@ -359,16 +363,16 @@ Two temporal formul\ae{} $f$ and $g$ can be combined using the
following Boolean operators: following Boolean operators:
\begin{center} \begin{center}
\begin{tabular}{ccccc} \begin{tabular}{cccccrl}
& preferred & \multicolumn{2}{c}{other supported} \\ & preferred & \multicolumn{2}{c}{other supported}&& \multicolumn{2}{l}{UTF8 characters supported}\\
operation & syntax & \multicolumn{2}{c}{syntaxes}\\ operation & syntax & \multicolumn{2}{c}{syntaxes} && preferred & others\\
\midrule \cmidrule(r){1-5} \cmidrule(l){6-7}
negation & $\NOT f$ & $\NOTALT f$ \\ negation & $\NOT f$ & $\NOTALT f$ & & & $\lnot$ \uni{00AC} \\
disjunction & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ \\ 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$ \\ conjunction & $f\AND g$ & $f\ANDALT g$ & $f\ANDALTT g$ & & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
implication & $f\IMPLIES g$ & $f\IMPLIESALT g$ & $f\IMPLIESALTT g$\\ 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$ \\ exclusion & $f\XOR g$ & $f\XORALT g$ & & & $\oplus$ \uni{2295} \\
equivalence & $f\EQUIV g$ & $f\EQUIVALT g$ & $f\EQUIVALTT g$ \\ equivalence & $f\EQUIV g$ & $f\EQUIVALT g$ & $f\EQUIVALTT g$ & & $\liff$ \uni{2194} & $\Leftrightarrow$ \uni{21D4}\\
\end{tabular} \end{tabular}
\end{center} \end{center}
@ -455,19 +459,19 @@ following rewritings:
f\XOR g &\equiv (f\AND\NOT g)\OR (g\AND\NOT f)\\ f\XOR g &\equiv (f\AND\NOT g)\OR (g\AND\NOT f)\\
\end{align*} \end{align*}
\section{Temporal Operators} \section{Temporal Operators}\label{sec:ltlops}
Given two temporal formul\ae{} $f$, and $g$, the following Given two temporal formul\ae{} $f$, and $g$, the following
temporal operators can be used to construct another temporal formula. temporal operators can be used to construct another temporal formula.
\begin{center} \begin{center}
\begin{tabular}{ccc} \begin{tabular}{cccrl}
& preferred & \multicolumn{1}{c}{other supported} \\ & preferred & \multicolumn{1}{c}{other supported} & \multicolumn{2}{l}{UTF8 characters supported} \\
operator & syntax & \multicolumn{1}{c}{syntaxes}\\ operator & syntax & \multicolumn{1}{c}{syntaxes} & preferred & others \\
\midrule \cmidrule(r){1-3} \cmidrule(l){4-5}
Next & $\X f$ & $\XALT f$ \\ Next & $\X f$ & $\XALT f$ & $\Circle$ \uni{25CB} & $\Circle$ \uni{25EF}\\
Eventually & $\F f$ & $\FALT f$ \\ Eventually & $\F f$ & $\FALT f$ & $\Diamond$ \uni{25C7} & $\Diamond$ \uni{22C4} \uni{2662}\\
Always & $\G f$ & $\GALT f$ \\ Always & $\G f$ & $\GALT f$ & $\Square$ \uni{25A1} & $\Square$ \uni{2B1C} \uni{25FB}\\
(Strong) Until & $f \U g$ \\ (Strong) Until & $f \U g$ \\
Weak Until & $f \W g$ \\ Weak Until & $f \W g$ \\
(Weak) Release & $f \R g$ & $f \RALT g$ \\ (Weak) Release & $f \R g$ & $f \RALT g$ \\
@ -562,27 +566,29 @@ be further combined with the following operators, where $f$ and $g$
denote arbitrary SERE and $b$ denotes a Boolean formula. denote arbitrary SERE and $b$ denotes a Boolean formula.
\begin{center} \begin{center}
\begin{tabular}{ccccc} \begin{tabular}{cccccrl}
& preferred & \multicolumn{2}{c}{other supported} \\ & preferred & \multicolumn{2}{c}{other supported} && \multicolumn{2}{l}{UTF8 characters supported}\\
operation & syntax & \multicolumn{2}{c}{syntaxes}\\ operation & syntax & \multicolumn{2}{c}{syntaxes} && preferred & others \\
\midrule \cmidrule(r){1-5}\cmidrule(l){6-7}
empty word & $\eword$ \\ empty word & $\eword$ \\
union & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ \\ union & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ && $\lor$ \uni{2228} $\cup$ \uni{222A}\\
(synchronized) intersection & $f\ANDALT g$ & $f\ANDALTT g$ \\ intersection & $f\ANDALT g$ & $f\ANDALTT g$ &&& $\cap$ \uni{2229} & $\land$ \uni{2227}\\
unsynchronized intersection & $f\AND g$ \\ NLM intersection\footnotemark & $f\AND g$ \\
concatenation & $f\CONCAT g$ \\ concatenation & $f\CONCAT g$ \\
fusion & $f\FUSION g$ \\ fusion & $f\FUSION g$ \\
bounded repetition & $f\STAR{\mvar{i}..\mvar{j}}$ bounded repetition & $f\STAR{\mvar{i}..\mvar{j}}$
& $f\STAR{\mvar{i}:\mvar{j}}$ & $f\STAR{\mvar{i}:\mvar{j}}$
& $f\STAR{\mvar{i} to \mvar{j}}$ & $f\STAR{\mvar{i} to \mvar{j}}$
& $f\STAR{\mvar{i},\mvar{j}}$\\ & $f\STAR{\mvar{i},\mvar{j}}$\\
unbounded repetition & $f\STAR{\mvar{i}..}$ \llap{un}bounded repetition & $f\STAR{\mvar{i}..}$
& $f\STAR{\mvar{i}:}$ & $f\STAR{\mvar{i}:}$
& $f\STAR{\mvar{i} to}$ & $f\STAR{\mvar{i} to}$
& $f\STAR{\mvar{i},}$\\ & $f\STAR{\mvar{i},}$\\
\end{tabular} \end{tabular}
\end{center} \end{center}
\footnotetext{\emph{Non-Length-Matching} interesction.}
The character \samp{\$} or the string \samp{inf} can also be used as The character \samp{\$} or the string \samp{inf} can also be used as
value for $\mvar{j}$ in the above operators to denote an unbounded value for $\mvar{j}$ in the above operators to denote an unbounded
range.\footnote{SVA uses \samp{\$} while PSL uses \samp{inf}.} For range.\footnote{SVA uses \samp{\$} while PSL uses \samp{inf}.} For
@ -772,6 +778,14 @@ For technical reasons, the negated weak closure is actually implemented as
an operator, even if it is syntactically and semantically equal to the an operator, even if it is syntactically and semantically equal to the
combination of $\NOT$ and $\sere{r}$. combination of $\NOT$ and $\sere{r}$.
UTF-8 input may combine one box or diamond character from
section~\ref{sec:ltlops} with one arrow character from
section~\ref{sec:boolops} to replace the operators $\Asuffix$,
$\Esuffix$, as well as the operators $\AsuffixEQ$ and $\EsuffixEQ$
that will be defined in \ref{sec:pslsugar}. Additionally,
$\AsuffixALT$ may be replaced by $\mapsto$ \uni{21A6}, and
$\AsuffixALTEQ$ by $\Mapsto$ \uni{2907}.
\subsection{Semantics} \subsection{Semantics}
The following semantics assume that $r$ is a SERE, The following semantics assume that $r$ is a SERE,
@ -792,7 +806,7 @@ is a model of $r$. An infinite sequence $\texttt{a;a;a;a;a;}\ldots$
is therefore a model of the formula \samp{$\sere{a\PLUS{};\NOT is therefore a model of the formula \samp{$\sere{a\PLUS{};\NOT
a}$} even though it never sees \samp{$\NOT a$}. a}$} even though it never sees \samp{$\NOT a$}.
\subsection{Syntactic Sugar} \subsection{Syntactic Sugar}\label{sec:pslsugar}
The syntax on the left is equivalent to the syntax on the right. The syntax on the left is equivalent to the syntax on the right.
These rewritings are performed from left to right when parsing a These rewritings are performed from left to right when parsing a