From 75862a3284020fd09947be4344c3066dbb42b246 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 4 Jun 2012 15:47:40 +0200 Subject: [PATCH] * doc/tl/tl.tex: Add a tricky example for the {r} operator. --- doc/tl/tl.tex | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index c7fc1e3f9..7936c3fc3 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -810,12 +810,15 @@ while $f$ is a PSL formula. \end{align*} The $\prec$ symbol should be read as ``\emph{is a prefix of}''. So -the semantic for `$\sigma\vDash \sere{r}$' is that either there is -a (non-empty) finite prefix of $\sigma$ that is a model of $r$, or any +the semantic for `$\sigma\vDash \sere{r}$' is that either there is a +(non-empty) finite prefix of $\sigma$ that is a model of $r$, or any prefix of $\sigma$ can be extended into a finite sequence $\pi$ that 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 - a}$} even though it never sees \samp{$\NOT a$}. +is therefore a model of the formula \samp{$\sere{a\PLUS{}\CONCAT\NOT + a}$} even though it never sees \samp{$\NOT a$}. The same sequence +is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT + a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT + a\STAR{}))}$} because this SERE does accept any word. \subsection{Syntactic Sugar}\label{sec:pslsugar}