diff --git a/Recherche/BFT-ARBover/3_GEO_CS/index.tex b/Recherche/BFT-ARBover/3_GEO_CS/index.tex index e14d01e..fd15553 100644 --- a/Recherche/BFT-ARBover/3_GEO_CS/index.tex +++ b/Recherche/BFT-ARBover/3_GEO_CS/index.tex @@ -34,18 +34,26 @@ DenyList as follows. \begin{algorithmic} - \Function{CANDIDATE}{$r$} - \State $\PROVE(r)$ - \EndFunction - \vspace{1em} - \Function{CLOSE}{$r$} - \State $\APPEND(r)$ - \EndFunction - \vspace{1em} - \Function{READGE}{$r$} - \State $P \gets \READ()$ - \State \Return $\{ j : (j,\PROVEtrace(r)) \in P \}$ - \EndFunction + \begin{algorithm}[H] + \caption{Group Election implementation using DenyList} + + \Function{CANDIDATE}{$r$} + \State $\PROVE(r)$ + \EndFunction + + \vspace{1em} + + \Function{CLOSE}{$r$} + \State $\APPEND(r)$ + \EndFunction + + \vspace{1em} + + \Function{READGE}{$r$} + \State $P \gets \READ()$ + \State \Return $\{ j : (j,\PROVEtrace(r)) \in P \}$ + \EndFunction + \end{algorithm} \end{algorithmic} \paragraph{Termination.} Termination follows from the Termination property of DenyList operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the DenyList. @@ -71,26 +79,29 @@ The operations are implemented as follows. - \begin{algorithmic} - \Function{APPEND}{$r$} - \State $\CLOSE(r)$ - \EndFunction - \vspace{1em} - \Function{PROVE}{$r$} - \State $\CANDIDATE(r)$ - \State $W_r \gets \READGE(r)$ - \If{$p \in W_r$} - \State \Return \texttt{True} - \Else - \State \Return \texttt{False} - \EndIf - \EndFunction - \vspace{1em} - \Function{READ}{$ $} - \State $W \gets \bigcup_{\forall r \in S}\READGE(r)$ - \State \Return $\{(p,r) \mid p \in W_r\}$ - \EndFunction - \end{algorithmic} + \begin{algorithm}[H] + \begin{algorithmic} + \caption{Group Election implementation using DenyList} + \Function{APPEND}{$r$} + \State $\CLOSE(r)$ + \EndFunction + \vspace{1em} + \Function{PROVE}{$r$} + \State $\CANDIDATE(r)$ + \State $W_r \gets \READGE(r)$ + \If{$p \in W_r$} + \State \Return \texttt{True} + \Else + \State \Return \texttt{False} + \EndIf + \EndFunction + \vspace{1em} + \Function{READ}{$ $} + \State $W \gets \bigcup_{\forall r \in S}\READGE(r)$ + \State \Return $\{(p,r) \mid p \in W_r\}$ + \EndFunction + \end{algorithmic} + \end{algorithm} \paragraph{Termination.} Termination follows from the Termination property of Group Election operations. Consider now a fixed sequential history $\mathsf{Seq}$ of the Group Election. diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf index f582a8f..935a2a8 100644 Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ