From fddfafcd60ab1c67059a0ab89e3f171443348651 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 5 Jun 2012 18:10:13 +0200 Subject: [PATCH] * doc/tl/tl.tex: Typos. --- doc/tl/tl.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 7936c3fc3..23e2e59ce 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1120,7 +1120,7 @@ methods \texttt{is\_syntactic\_safety()}, page~\pageref{property-methods}). 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. $\varphi_F$ denotes a finite LTL formula (the unnamed class at the 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 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 -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. The form on the left of the table syntactically implies the form on