From 9a698bf66ffa8d14a70bc5556c94be291a71ec4e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 3 Jul 2016 19:56:29 +0200
Subject: [PATCH] fix a weird typo
---
docs/constructions.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 8481c53f1..03e331a13 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -395,7 +395,7 @@ The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
\begin{align*}
(s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
- s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
+ s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \land (s, T_1) \stsstep (s', T_2)
\end{align*}
We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
--
GitLab