From fa26ee4b3834962c545fc5ee1d7f660822579e10 Mon Sep 17 00:00:00 2001 From: Sasha Bogicevic Date: Wed, 7 Aug 2024 16:58:06 +0200 Subject: [PATCH] Update the spec with decommit offchain changes Signed-off-by: Sasha Bogicevic --- .../Protocol/Figures/fig_offchain_prot.tex | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex b/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex index 93366fb..2f80ea3 100644 --- a/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex +++ b/hydra-protocol/Hydra/Protocol/Figures/fig_offchain_prot.tex @@ -82,10 +82,19 @@ %%% REQ SN \On{$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$ from $\party_j$}{ - \Req{$v = \hatv ~ \land ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; - \Wait{$\hats = \bar{\mc S}.s$}{ - \Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$} \; - $U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega} \setminus \mathsf{outputs(\tx_{\omega})}$ \; + \Req{$s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; + \Wait{$ v = \hatv ~ \land ~ \hats = \bar{\mc S}.s$}{ + % TODO: waiting for version observed is way longer than for no snapshot in flight! + \If{$v = \bar{\mc S}.v ~ \land ~ \bar{\mc S}.\tx_{\omega} \neq \bot$ }{ + \Req{$\bar{\mc S}.\tx_{\omega} = \tx_{\omega}$} \; + $U_{\mathsf{active}} \gets \bar{\mc S}.U$ \; + $U_{\omega} \gets \bar{\mc S}.U_{\omega}$ + } + \Else{ + \Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$} \; + $U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega} \setminus \mathsf{outputs(\tx_{\omega})}$ \; + $U_{\omega} \gets \mathsf{outputs}(\tx_{\omega})$ + } \Req{$U_{\mathsf{active}} \applytx \mT_{\mathsf{req}} \not= \bot$} \; $U \gets U_{\mathsf{active}} \applytx \mT_{\mathsf{req}}$ \; $\hats \gets s$ \;