Refactor: replace U'_\omega by \tx_\omega

To keep it consistent on how decrement is handled.

spec/fig_offchain_prot.tex

@@ -90,8 +90,11 @@
 										\Req{$\bar{\mc S}.U \applytx \psi \not= \bot$} \;
 										$U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \psi$ \;
 									}
-									\If{$\psi \in U_\omega$} {
-										$U_{\mathsf{active}} \gets \bar{\mc S}.U \cup \psi$ \;
+									\ElseIf{$\psi \in \tx_\alpha$} {
+										$U_{\mathsf{active}} \gets \bar{\mc S}.U \cup \mathsf{outputs}(\psi)$ \;
+									}
+									\Esle {
+										$U_{\mathsf{active}} \gets \bar{\mc S}.U$ \;
 									}
 								}
 								\Req{$\red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \;
@@ -101,13 +104,8 @@
 								% TODO: DRY message creation
 								$\eta \gets \combine(U)$ \;
 								\red{
-									\If{$\psi \in \tx_\omega$}{
-										% TODO: handwavy combine/outputs here
-										$\red{\eta_\omega \gets \mathsf{outputs}(\psi)}$ \;
-									}
-									\If{$\psi \in U_\omega$} {
-										$\red{\eta_\omega \gets \psi}$ \;
-									}
+									% TODO: handwavy combine/outputs here
+									$\red{\eta_\omega \gets \mathsf{outputs}(\psi)}$ \;
 								}
 								% NOTE: WE could make included transactions auditable by adding
 								% a merkle tree root to the (signed) snapshot data \eta
@@ -166,12 +164,12 @@
 
 						%%% REC INC
 						\red{
-							\On{$(\mathtt{reqInc},U'_\omega)$ from $\party_j$}{
-								\Wait{$U_\omega = \bot$}{
-									$U_\omega \gets U'_\omega$\;
+							\On{$(\mathtt{reqInc}, \tx_\alpha)$ from $\party_j$}{
+								\Wait{$U_\omega = \bot ~ \land ~ \hatmL \applytx \tx_\alpha \not= \bot$}{
+									$U_\omega \gets \mathsf{outputs}(\tx_\alpha)$\;
 									% issue snapshot if we are leader
 									\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-										$\psi \gets U'_\omega$ \;
+										$\psi \gets \tx_\alpha$ \;
 										\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT,\psi)$ \;
 									}
 								}
@@ -181,9 +179,9 @@
 						\vspace{12pt}
 
 						%%% INCREMENT
-						\red{\On{$(\mathtt{incrementTx}, U'_\omega, v)$ from chain}{
-							\If{$U_\omega \not= \bot ~ \land ~ U'_\omega = \bar{\mc S}.U_\omega$}{
-								$\hatmL \gets \hatmL \cup U'_\omega$ \;
+						\red{\On{$(\mathtt{incrementTx}, \tx_\alpha, v)$ from chain}{
+							\If{$U_\omega \not= \bot ~ \land ~ \mathsf{outputs}(\tx_\alpha) = \bar{\mc S}.U_\omega$}{
+								$\hatmL \gets \hatmL \cup \mathsf{outputs}(\tx_\alpha)$ \;
 								$U_\omega \gets \bot$\;
 								$\hatv \gets v$ \;
 								% TODO: always snapshot? not strictly needed (to clear pending decommits)?
@@ -231,8 +229,8 @@
 										\If{$\psi \not= \bot ~ \land ~ \psi \in \tx_\omega$}{
 											$\eta_\omega \gets \mathsf{outputs}(\tx_\omega)$ \;
 										}
-										\ElseIf{$\psi \not= \bot ~ \land ~ \psi \in U_\omega$}{
-											$\eta_\omega \gets U_\omega$ \;
+										\ElseIf{$\psi \not= \bot ~ \land ~ \psi \in \tx_\alpha$}{
+											$\eta_\omega \gets \mathsf{outputs}(\tx_\alpha)$ \;
 										}
 										\Else{
 											$\eta_\omega \gets \bot$ \;
@@ -251,7 +249,7 @@
 											$\PostTx{}~(\mathtt{decrementTx}, \hatv, \hats, \eta, \eta_\omega)$ \;
 											$\Out (\hpConf,\psi)$ \;
 										}
-										\If{$\psi \not= \bot ~ \land ~ \psi \in U_\omega$}{
+										\If{$\psi \not= \bot ~ \land ~ \psi \in \tx_\alpha$}{
 											$\PostTx{}~(\mathtt{incrementTx}, \hatv, \hats, \eta, \eta_\omega)$ \;
 											$\Out (\hpConf,\psi)$ \;
 										}

spec/offchain.tex

@@ -135,9 +135,9 @@ \subsection{Variables}
 		The function $\Sno(v,n,T,U,U_\omega)$ initializes a snapshot object with no multi-signature set.
 	 \todo{handwavy; types?}
 	}
-	\item \red{$\tx_{\omega} \in \mathcal{T}$: Pending decrement transaction, whose outputs are to be withdrawn from the head.}
-	\item \red{$U'_\omega \in \gcUTXOset$: Pending increment UTxO to be deposited to the head.}
-	\item \red{$\psi \in \tx_\omega \cup U'_\omega \cup \bot$: Either a decrement transaction, an increment UTxO or $\bot$.
+	\item \red{$\tx_\alpha \in \mathcal{T}$: Pending increment transaction, whose outputs are to be deposited to the head.}
+	\item \red{$\tx_\omega \in \mathcal{T}$: Pending decrement transaction, whose outputs are to be withdrawn from the head.}
+	\item \red{$\psi \in \tx_\alpha \cup \tx_\omega \cup \bot$: Either a decrement transaction, an increment transaction or $\bot$.
 		May be $\bot$ if nothing is pending to be applied.}
 \end{itemize}
 
@@ -172,8 +172,8 @@ \subsubsection{Initializing the head}
 transaction, the parties compute $\Uinit \gets \bigcup_{j=1}^{n} C_j$ using previously
 observed $C_j$ and initialize $\hatmL = \Uinit$. The seen transaction set is
 initialized empty $\hatmT = \emptyset$, \red{seen head state version $\hatv = 0$}, as
-well as snapshot number $\hats = 0$. \red{No increment/decrement transaction is pending
-$U_\omega = \bot$ and} the initial snapshot object is defined accordingly
+well as snapshot number $\hats = 0$. \red{No increment/decrement UTxO is pending
+($U_\omega = \bot$) and} the initial snapshot object is defined accordingly
 $\bar{\mc S} \gets \Sno(0, 0, \Uinit, \emptyset, \red{\bot})$.
 
 \subsubsection{Processing transactions off-chain}
@@ -214,18 +214,18 @@ \subsubsection{Processing transactions off-chain}
 }
 \todo{missing to mention the multicast of $\hpRS$} \\
 
-\red{\dparagraph{$\hpRI$.}\quad Upon receiving request $(\hpRI,U'_\omega)$, if
+\red{\dparagraph{$\hpRI$.}\quad Upon receiving request $(\hpRI,\tx_\alpha)$, if
   another decrement (or increment) is pending to be settled the transaction is
-  rejected. Otherwise the requestd UTxO is kept in the local state ($U_\omega$)
+  rejected. Otherwise the transaction outputs are kept in the local state ($U_\omega$)
   to be posted on-chain in the next snapshot.
   Finally, if there is no current snapshot in flight ($\hats = \bar{\mc S}.s$) and the
   receiving party $\party_{i}$ is the next snapshot leader, a message to request
-  snapshot signatures $\hpRS$ containing the increment UTxO $U'_\omega$ is sent.} \\
+  snapshot signatures $\hpRS$ containing the increment transaction $\tx_\alpha$ is sent.} \\
 
 \red{\dparagraph{$\mathtt{incrementTx}$.}\quad Upon observing the \mtxIncrement{}
 	transaction which outputs are added to the confirmed UTxO in the Head, we include
   the outputs to the \emph{local} ledger state. Finally the corresponding pending increment
-  UTxO is cleared and the observed version is used for future snapshots by setting
+  transaction is cleared and the observed version is used for future snapshots by setting
   $\hatv = v$. The version of the open head state is incremented on each \mtxIncrement{}
   transaction as described in Section~\ref{sec:increment-tx}
 }
@@ -245,7 +245,8 @@ \subsubsection{Processing transactions off-chain}
     there is a pending decrement and we check that $\tx_\omega$ transaction is applicable to the last confirmed
 	  UTxO set $\hat{\mc S}.U$ and it's inputs are removed, yielding the still active UTxO set $U_{\mathsf{active}}$
   \item
-    there is a pending increment and we make sure that $U_\omega$ is part of the active UTxO set $U_{\mathsf{active}}$
+    there is a pending increment and we make sure that the outputs of $\tx_\alpha$ are part of the active UTxO set
+	$U_{\mathsf{active}}$
 \end{itemize}
   Then, all requested transactions $\mT_{\mathsf{req}}$ are $\Req$d to be applicable
   to $U_{\mathsf{active}}$,}