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

Small documentation fixes.

Browse source 
* doc/tl/tl.tex: Fix a few typos, and comment a missplaced paragraph.
* doc/tl/tl.bib: Typos.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-02 13:08:03 +02:00
parent 1a50ae3bf8
commit dadfbdad9d
2 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/tl/tl.bib
View file

@ -18,11 +18,11 @@
@InProceedings{ beer.01.cav,
author = {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
Fisman and Anna Gringauze and Yoav Rodeh},
title = {The Temporal Logic Sugar},
title = {The Temporal Logic {S}ugar},
booktitle = {Proceedings of the 13th international conferance on
Computer Aided Verification (CAV'01)},
series = {Lecture Notes in Computer Science},
editor = {Berry, Gérard and Comon, Hubert and Finkel, Alain},
editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
publisher = {Springer},
isbn = {978-3-540-42345-4},
pages = {363--367},

32
doc/tl/tl.tex
View file

@ -193,7 +193,7 @@
\section{Finite and Infinite Sequences}
Let $\N=\{0,1,2,\ldots\}$ designate the set of natural numbers and
Let $\N=\{0,1,2,\ldots\}$ denote the set of natural numbers and
$\omega\not\in\N$ the first transfinite ordinal. We extend the $<$
relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\,
n<\omega$. Similarly let us extend the addition and subtraction with
@ -1005,8 +1005,8 @@ suffix-closed, i.e., if you remove any finite prefix of an accepted
$\varphi$ is a suffix-closed formula, then $\G\varphi \equiv \varphi$.
Let $\varphi$ designate any arbitrary formula and $\varphi_E$
(resp. $\varphi_U$) designate any instance of a pure eventuality
Let $\varphi$ denote any arbitrary formula and $\varphi_E$
(resp. $\varphi_U$) denote any instance of a pure eventuality
(resp. a purely universal) formula. We have the following grammar
rules:
@ -1108,9 +1108,9 @@ methods \texttt{is\_syntactic\_safety()},
page~\pageref{property-methods}).
The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
$\varphi_R$ designate any formula belonging respectively to the
$\varphi_R$ denot any formula belonging respectively to the
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
$\varphi_F$ designates a finite LTL formula (the unnamed class at the
$\varphi_F$ denotes a finite LTL formula (the unnamed class at the
intersection of Safety and Guarantee formul\ae{} on
Fig.~\ref{fig:hierarchy}). $v$ denotes any variable, $r$ any SERE,
$r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE.
@ -1164,7 +1164,7 @@ $r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE.
\mid{}& \X\varphi_R \mid \G\varphi_R \mid
\varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid
\varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\
\mid{}& \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\mid \sere{r}\Asuffix \varphi_P\\
\mid{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\\
\end{align*}
It should be noted that a formula can belong to a class of the
@ -1293,16 +1293,16 @@ from left to right, as usual):
\G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
\end{align*}
Note that the latter three rewriting rules for $\G$ have no dual:
rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested
by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$
operator in front of the formula. Conceptually, it is also easier to
understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified,
there is no need to worry about the $\G\F g$ term.
% Note that the latter three rewriting rules for $\G$ have no dual:
% rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (as suggested
% by~\citet{somenzi.00.cav}) goes against our goal of moving the $\F$
% operator in front of the formula. Conceptually, it is also easier to
% understand $\F(f \AND \G\F g)$: has long as $f$ has not been verified,
% there is no need to worry about the $\G\F g$ term.
Here are the basic rewriting rules for binary operators (excluding
$\OR$ and $\AND$ which are considered in Spot as $n$-ary operators).
$b$ denotes a Boolean formula.
$b$ denotes any Boolean formula.
\begin{align*}
\1 \U f & \equiv \F f & f \W \0 & \equiv \G f \\
@ -1684,8 +1684,8 @@ f)\implies(\pi\VDash g)$.
The recursive rules for syntactic implication are rules are described
in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic
implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ designate any PSL
formula in negative normal form, and $f_U$ and $g_E$ designate a
implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ denote any PSL
formula in negative normal form, and $f_U$ and $g_E$ denot a
purely universal formula and a pure eventuality.
The form on the left of the table syntactically implies the form on
@ -1704,7 +1704,7 @@ conclusion by chaining two rules: ``$\F f \simp \underbrace{\F
``$f \simp \F g$ \textit{if} $f\simp g$''.
The rules from table~\ref{tab:syntimpl} should be completed by the
following cases, where $f_b$ and $g_b$ designate Boolean formul\ae{}:
following cases, where $f_b$ and $g_b$ denote Boolean formul\ae{}:
\begin{center}
\begin{tabular}{rl}
we have & if \\