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

Fix semantics of [*i..j] and [:*i..j]

Browse source 
* doc/tl/tl.tex: After a discussion with Antoin, it appears that the
semantics previously given for f[*0..j] was not considering that f[*0]
should accept any sequence of one letter.
This commit is contained in:
Alexandre Duret-Lutz 2022-12-07 11:26:51 +01:00
parent 5dbf601afb
commit 4629d074ab
1 changed files with 9 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

24
doc/tl/tl.tex
View file

@ -668,20 +668,17 @@ $a$ is an atomic proposition.
\sigma\VDash f\FUSION g&\iff \exists k\in\N,\,(\sigma^{0..k} \VDash f)\land(\sigma^{k..} \VDash g)\\ \sigma\VDash f\FUSION g&\iff \exists k\in\N,\,(\sigma^{0..k} \VDash f)\land(\sigma^{k..} \VDash g)\\
\sigma\VDash f\STAR{\mvar{i}..\mvar{j}}& \iff \sigma\VDash f\STAR{\mvar{i}..\mvar{j}}& \iff
\begin{cases} \begin{cases}
\text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\ \text{either} & \mvar{i}=0 \land\mvar{j}=0\land \sigma=\varepsilon \\
\text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land \bigl((\sigma = \varepsilon) \lor (\sigma
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} \VDash f\STAR{\mvar{1}..\mvar{j}})\bigr)\\
\VDash f\STAR{\mvar{0}..\mvar{j-1}}))\\
\text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
\VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\ \VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\
\end{cases}\\ \end{cases}\\
\sigma\VDash f\STAR{\mvar{i}..} & \iff \sigma\VDash f\STAR{\mvar{i}..} & \iff
\begin{cases} \begin{cases}
\text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\ \text{either} & \mvar{i}=0 \land \bigl((\sigma=\varepsilon)\lor(\sigma
\text{or} & \mvar{i}=0 \land (\exists k\in\N,\, \VDash f\STAR{\mvar{1}..})\bigr)\\
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
\VDash f\STAR{\mvar{0}..}))\\
\text{or} & \mvar{i}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
\VDash f\STAR{\mvar{i-1}..}))\\ \VDash f\STAR{\mvar{i-1}..}))\\
@ -689,19 +686,16 @@ $a$ is an atomic proposition.
\sigma\VDash f\FSTAR{\mvar{i}..\mvar{j}}& \iff \sigma\VDash f\FSTAR{\mvar{i}..\mvar{j}}& \iff
\begin{cases} \begin{cases}
\text{either} & \mvar{i}=0 \land \mvar{j}=0 \land \sigma\VDash\1 \\ \text{either} & \mvar{i}=0 \land \mvar{j}=0 \land \sigma\VDash\1 \\
\text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land \bigl((\sigma\VDash\1)\lor(\sigma
(\sigma^{0..k}\VDash f) \land (\sigma^{k..} \VDash f\FSTAR{\mvar{1}..\mvar{j}})\bigr)\\
\VDash f\FSTAR{\mvar{0}..\mvar{j-1}}))\\
\text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..} (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{i-1}..\mvar{j-1}}))\\ \VDash f\FSTAR{\mvar{i-1}..\mvar{j-1}}))\\
\end{cases}\\ \end{cases}\\
\sigma\VDash f\FSTAR{\mvar{i}..} & \iff \sigma\VDash f\FSTAR{\mvar{i}..} & \iff
\begin{cases} \begin{cases}
\text{either} & \mvar{i}=0 \land \sigma\VDash\1 \\ \text{either} & \mvar{i}=0 \land \bigl((\sigma\VDash\1)
\text{or} & \mvar{i}=0 \land (\exists k\in\N,\, \lor(\sigma \VDash f\FSTAR{\mvar{1}..})\bigr)\\
(\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{0}..}))\\
\text{or} & \mvar{i}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..} (\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{i-1}..}))\\ \VDash f\FSTAR{\mvar{i-1}..}))\\