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

* doc/tl/tl.tex: Typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-06-05 18:10:13 +02:00
parent 57ec1c61c9
commit fddfafcd60
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/tl/tl.tex
View file

@ -1120,7 +1120,7 @@ methods \texttt{is\_syntactic\_safety()},
page~\pageref{property-methods}). page~\pageref{property-methods}).
The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$, The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
$\varphi_R$ denot any formula belonging respectively to the $\varphi_R$ denote any formula belonging respectively to the
Guarantee, Safety, Obligation, Persistence, or Recurrence classes. Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
$\varphi_F$ denotes 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 intersection of Safety and Guarantee formul\ae{} on
@ -1697,7 +1697,7 @@ f)\implies(\pi\VDash g)$.
The recursive rules for syntactic implication are rules are described The recursive rules for syntactic implication are rules are described
in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic
implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ denote any PSL 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 formula in negative normal form, and $f_U$ and $g_E$ denote a
purely universal formula and a pure eventuality. purely universal formula and a pure eventuality.
The form on the left of the table syntactically implies the form on The form on the left of the table syntactically implies the form on