Off-chain spec changes

Increment and ReqSn changes are all there.
We need to tackle `combine` for the \tx_{\omega} where
we need to first check if the ReqSn contains \tx_{\omega} or
\bigcup_{\omega} first.

spec/fig_offchain_prot.tex

@@ -73,19 +73,23 @@
 								$\hatmT \gets \hatmT \cup \{\tx\}$ \;
 								% issue snapshot if we are leader
 								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-									\Multi{} $(\hpRS,\red{\hatv,}\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}})$ \;
+                  \Multi{} $(\hpRS,\red{\hatv,}\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}, \bigcup_{\omega}})$ \;
 								}
 							}
 						}
 
 						\vspace{12pt}
 
 						%%% REQ SN
-						\On{$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_{\omega}})$ from $\party_j$}{
+            \On{$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_{\omega}, \bigcup_{\omega}})$ from $\party_j$}{
 							\Req{$\red{v = \hatv ~ \land} ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \;
 							\Wait{$\hats = \bar{\mc S}.s$}{
-							    \red{\Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$}} \;
+                \If{\red{\Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$}} \;}{
 							    \red{$U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega}$} \;
+                }
+                \If{\red{\Req{$\bigcup_{\omega} \not= \bot$}} \;}{
+							    \red{$U_{\mathsf{active}} \gets \bar{\mc S}.U \cup \bigcup_{\omega}$} \;
+                }
 								\Req{$\red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \;
 								$U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$ \;
 								% XXX: why +1? ̂s ← s would be clearer here
@@ -123,7 +127,7 @@
 							  $\tx_\omega \gets \tx$ \;
 							  % issue snapshot if we are leader
 							  \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-								\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega})$ \;
+								\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega}, \bot)$ \;
 							  }
 							}
 						}
@@ -138,14 +142,35 @@
 								$\hatv \gets v$ \;
 								% TODO: always snapshot? not strictly needed (to clear pending decommits)?
 								\If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
-									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega})$ \;
+									\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega}, \bot)$ \;
 								}
 							}
 						}
 						}
 
 						\vspace{12pt}
 
+						%%% REC INC
+            \red{\On{$(\mathtt{reqInc},\bigcup_{\omega})$ from $\party_j$}{
+                \Wait{$\bigcup_{\omega} = \bot$}{
+							  % issue snapshot if we are leader
+							  \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{
+								\Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \bot , \bigcup_{\omega})$ \;
+							  }
+							}
+						}
+						}
+
+						\vspace{12pt}
+
+						%%% INCREMENT
+						\red{\On{$(\mathtt{incrementTx}, U_{\omega}, v)$ from chain}{
+								$\bigcup_{\omega} \gets \bot$ \;
+							}
+						}
+
+						\vspace{12pt}
+
 						%%% ACK SN
 						\On{$(\hpAS,s,\msSig_j)$ from $\party_j$}{
 							\Req{} $s \in \{\hats,\hats+1\}$ \;
@@ -174,7 +199,7 @@
 									}}
 									% issue snapshot if we are leader
 									\If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{
-										\Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}})$ \;
+                    \Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}, \bigcup_{\omega}})$ \;
 									}
 								}
 							}

spec/macros.tex

@@ -418,6 +418,7 @@
 
 \newcommand{\hpNS}{\mathtt{newSn}}
 \newcommand{\hpRS}{\mathtt{reqSn}}
+\newcommand{\hpRI}{\mathtt{reqInc}}
 \newcommand{\hpRD}{\mathtt{reqDec}}
 \newcommand{\hpAS}{\mathtt{ackSn}}
 \newcommand{\hpCS}{\mathtt{confSn}}