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

tl: fix incorrect comment about {r} vs. cl(r)

Browse source 
Fixes #242.

* doc/tl/tl.tex: Remove incorrect claim that {r} does not match the
PSL semantics.
This commit is contained in:
Alexandre Duret-Lutz 2017-03-13 18:09:44 +01:00
parent d6d987bd96
commit d0f92d75a1
1 changed files with 0 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
doc/tl/tl.tex
View file

@ -867,13 +867,6 @@ is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT
a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT
a\STAR{}))}$} because this SERE does not accept any word. a\STAR{}))}$} because this SERE does not accept any word.
Note that the semantics of $\sere{r}$ comes from the
$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}. This
differs from the interpretation of a SERE $r$ in the context of a
temporal formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
item~7]{psl.04.lrm}: the $\sere{r}$ semantics used here corresponds to
$r!\lor r$ in the PSL standard.
\subsection{Syntactic Sugar}\label{sec:pslsugar} \subsection{Syntactic Sugar}\label{sec:pslsugar}
The syntax on the left is equivalent to the syntax on the right. The syntax on the left is equivalent to the syntax on the right.