amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

reformatage

Browse Source
This commit is contained in:
Amaury JOLY
2026-01-20 10:53:00 +01:00
parent d5a865dd0a
commit 3e8aec36a2
2 changed files with 43 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

75
Recherche/BFT-ARBover/3_GEO_CS/index.tex
View File

@@ -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.