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

* doc/tl/tl.tex: Fix a couple of typos detected by ispell.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2022-09-22 16:19:07 +02:00
parent 3729dfad90
commit 383128d983
1 changed files with 16 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

21
doc/tl/tl.tex
View file

@ -395,7 +395,7 @@ following Boolean operators:
(allowing better compatibility with Wring and VIS) may only used in
temporal formulas. 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.}
symbol is used as the Kleene star.}
Additionally, an atomic proposition $a$ can be negated using the
syntax \samp{$a$=0}, which is equivalent to \samp{$\NOT a$}. Also
@ -600,7 +600,7 @@ the source. It can mean either ``\textit{Sequential Extended Regular
``\textit{Semi-Extended Regular Expression}''~\citep{eisner.08.hvc}.
In any case, the intent is the same: regular expressions with
traditional operations (union `$\OR$', concatenation `$\CONCAT$',
Kleen star `$\STAR{}$') are extended with operators such as
Kleene star `$\STAR{}$') are extended with operators such as
intersection `$\ANDALT$', and fusion `$\FUSION$'.
Any Boolean formula (section~\ref{def:boolform}) is a SERE. SERE can
@ -638,7 +638,7 @@ denote arbitrary SERE.
\end{tabular}
\end{center}
\footnotetext{\emph{Non-Length-Matching} interesction.}
\footnotetext{\emph{Non-Length-Matching} intersection.}
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
@ -1069,7 +1069,7 @@ psl2ba, Modella, and NuSMV all have $\U$ and $\R$ as left-associative,
while Goal (hence Büchi store), LTL2AUT, and LTL2Büchi (from
JavaPathFinder) have $\U$ and $\R$ as right-associative. Vis and LBTT
have these two operators as non-associative (parentheses required).
Similarly the tools do not aggree on the associativity of $\IMPLIES$
Similarly the tools do not agree on the associativity of $\IMPLIES$
and $\EQUIV$: some tools handle both operators as left-associative, or
both right-associative, other have only $\IMPLIES$ as right-associative.
@ -1429,7 +1429,7 @@ $\NOT$ operator.
\end{align*}
Note that the above rules include the ``unabbreviation'' of operators
``$\EQUIV$'', ``$\IMPLIES$'', and ``$\XOR$'', correspondings to the
``$\EQUIV$'', ``$\IMPLIES$'', and ``$\XOR$'', corresponding to the
rules \texttt{"ei\^"} of function `\verb=unabbreviate()= as described
in Section~\ref{sec:unabbrev}. Therefore it is never necessary to
apply these abbreviations before or after
@ -2097,3 +2097,14 @@ $f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g} & & &
%%% TeX-master: t
%%% coding: utf-8
%%% End:
% LocalWords: tabu Alexandre Duret Lutz toc subsequence Kripke unary
% LocalWords: LTL GFa INISHED ZX FX cccccrl UTF syntaxes disjunction
% LocalWords: VIS Kleene overline overbar ary cccrl EF sep FB LTLf
% LocalWords: rewritings TSLF NLM iter un SVA PSL SEREs DFA ccccc ba
% LocalWords: SystemVerilog clc ltl psl Modella NuSMV Büchi AUT Vis
% LocalWords: JavaPathFinder LBTT AST subtrees boolean nenoform lbt
% LocalWords: eword nn LBT's automata subformulas ottom unabbreviate
% LocalWords: Unabbreviations ei GRW RW WR unabbreviator simplifier
% LocalWords: tl unabbreviation indeterminism dnf cnf SNF rl iff BDD
% LocalWords: subformula