From 418eeacc258d0932c299ab64698691890c7397cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ale=C5=A1=20Bizjak?= <abizjak@cs.au.dk>
Date: Tue, 26 Jul 2016 08:09:15 +0200
Subject: [PATCH] Fixed some typos in the appendix.
---
docs/model.tex | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/docs/model.tex b/docs/model.tex
index d8595b6ba..f6ce77818 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -46,14 +46,13 @@ We introduce an additional logical connective $\ownM\melt$, which will later be
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
-
\subsection{Iris model}
\paragraph{Semantic domain of assertions.}
The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
\begin{align*}
- \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
+ \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
@@ -87,7 +86,7 @@ We only have to define the interpretation of the missing connectives, the most i
\wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
\rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land
\dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
- \All\iname \in \mask, \prop. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
+ \All\iname \in \mask, \prop \in \iProp. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
\end{inbox}\\
\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
\end{align*}
@@ -95,7 +94,7 @@ We only have to define the interpretation of the missing connectives, the most i
\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
\begin{align*}
\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
- \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
+ \All \rs_\f, k, \mask_\f, \state.& 0 < k \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
\Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
\end{aligned}}
\end{align*}
--
GitLab