% generated by Plantuml 1.2025.10      
\definecolor{plantucolor0000}{RGB}{255,255,255}
\definecolor{plantucolor0001}{RGB}{24,24,24}
\definecolor{plantucolor0002}{RGB}{0,0,0}
\definecolor{plantucolor0003}{RGB}{226,226,240}
\definecolor{plantucolor0004}{RGB}{238,238,238}
\definecolor{plantucolor0005}{RGB}{254,255,221}
\begin{tikzpicture}[yscale=-1
,pstyle0/.style={color=plantucolor0000,line width=0.0pt}
,pstyle1/.style={color=plantucolor0001,line width=0.5pt,dash pattern=on 5.0pt off 5.0pt}
,pstyle2/.style={color=plantucolor0001,fill=plantucolor0003,line width=0.5pt}
,pstyle3/.style={color=plantucolor0001,line width=0.5pt}
,pstyle4/.style={color=plantucolor0001,fill=plantucolor0001,line width=1.0pt}
,pstyle5/.style={color=plantucolor0001,line width=1.0pt}
,pstyle6/.style={color=plantucolor0001,line width=1.0pt,dash pattern=on 2.0pt off 2.0pt}
,pstyle7/.style={color=black,fill=plantucolor0004,line width=1.5pt}
,pstyle8/.style={color=black,line width=1.5pt}
,pstyle9/.style={color=plantucolor0001,fill=plantucolor0005,line width=0.5pt}
]
\draw[pstyle0] (20.5pt,75pt) rectangle (28.5pt,722.6982pt);
\draw[pstyle1] (24pt,75pt) -- (24pt,722.6982pt);
\draw[pstyle0] (105.8255pt,75pt) rectangle (113.8255pt,722.6982pt);
\draw[pstyle1] (109.3255pt,75pt) -- (109.3255pt,722.6982pt);
\draw[pstyle0] (273.8933pt,75pt) rectangle (281.8933pt,722.6982pt);
\draw[pstyle1] (277.3933pt,75pt) -- (277.3933pt,722.6982pt);
\node at (14.055pt,65pt)[below right,color=black,inner sep=0]{DL};
\draw[pstyle2] (6pt,29pt) ..controls (6pt,19pt) and (24pt,19pt) .. (24pt,19pt) ..controls (24pt,19pt) and (42pt,19pt) .. (42pt,29pt) -- (42pt,55pt) ..controls (42pt,65pt) and (24pt,65pt) .. (24pt,65pt) ..controls (24pt,65pt) and (6pt,65pt) .. (6pt,55pt) -- (6pt,29pt);
\draw[pstyle3] (6pt,29pt) ..controls (6pt,39pt) and (24pt,39pt) .. (24pt,39pt) ..controls (24pt,39pt) and (42pt,39pt) .. (42pt,29pt);
\node at (100.4205pt,65pt)[below right,color=black,inner sep=0]{P1};
\draw[pstyle2] (109.3255pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (109.3255pt,21.5pt) -- (109.3255pt,48.5pt)(96.3255pt,29.5pt) -- (122.3255pt,29.5pt)(109.3255pt,48.5pt) -- (96.3255pt,63.5pt)(109.3255pt,48.5pt) -- (122.3255pt,63.5pt);
\node at (268.4883pt,65pt)[below right,color=black,inner sep=0]{P2};
\draw[pstyle2] (277.3933pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (277.3933pt,21.5pt) -- (277.3933pt,48.5pt)(264.3933pt,29.5pt) -- (290.3933pt,29.5pt)(277.3933pt,48.5pt) -- (264.3933pt,63.5pt)(277.3933pt,48.5pt) -- (290.3933pt,63.5pt);
\draw[pstyle4] (35pt,95pt) -- (25pt,99pt) -- (35pt,103pt) -- (31pt,99pt) -- cycle;
\draw[pstyle5] (29pt,99pt) -- (108.3255pt,99pt);
\node at (41pt,87pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (97.3255pt,115.8333pt) -- (107.3255pt,119.8333pt) -- (97.3255pt,123.8333pt) -- (101.3255pt,119.8333pt) -- cycle;
\draw[pstyle6] (24pt,119.8333pt) -- (103.3255pt,119.8333pt);
\node at (31pt,111pt)[below right,inner sep=0]{$P$};
\draw[pstyle5] (109.3255pt,143.8333pt) -- (151.3255pt,143.8333pt);
\draw[pstyle5] (151.3255pt,143.8333pt) -- (151.3255pt,156.8333pt);
\draw[pstyle5] (110.3255pt,156.8333pt) -- (151.3255pt,156.8333pt);
\draw[pstyle4] (120.3255pt,152.8333pt) -- (110.3255pt,156.8333pt) -- (120.3255pt,160.8333pt) -- (116.3255pt,156.8333pt) -- cycle;
\node at (116.3255pt,131.8333pt)[below right,inner sep=0]{$r_{max} = max\{r : (\_, prove(r)) \in P\}$};
\draw[pstyle7] (8pt,168.8333pt) -- (74.4pt,168.8333pt) -- (74.4pt,170.8333pt) -- (64.4pt,180.8333pt) -- (8pt,180.8333pt) -- (8pt,168.8333pt);
\draw[pstyle8] (8pt,168.8333pt) rectangle (259.8182pt,353.6666pt);
\node at (23pt,169.8333pt)[below right,color=black,inner sep=0]{\textbf{loop}};
\node at (89.4pt,172.0833pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (92.59pt,170.8333pt)[below right,inner sep=0]{$\textbf{foreach } r \in \{r_{max} + 1, \dots\}$};
\node at (215.4514pt,172.0833pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle4] (35pt,202.8333pt) -- (25pt,206.8333pt) -- (35pt,210.8333pt) -- (31pt,206.8333pt) -- cycle;
\draw[pstyle5] (29pt,206.8333pt) -- (108.3255pt,206.8333pt);
\node at (41pt,194.8333pt)[below right,inner sep=0]{$PROVE(r)$};
\draw[pstyle4] (35pt,226.8333pt) -- (25pt,230.8333pt) -- (35pt,234.8333pt) -- (31pt,230.8333pt) -- cycle;
\draw[pstyle5] (29pt,230.8333pt) -- (108.3255pt,230.8333pt);
\node at (41pt,218.8333pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle4] (35pt,250.8333pt) -- (25pt,254.8333pt) -- (35pt,258.8333pt) -- (31pt,254.8333pt) -- cycle;
\draw[pstyle5] (29pt,254.8333pt) -- (108.3255pt,254.8333pt);
\node at (41pt,242.8333pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (97.3255pt,271.6666pt) -- (107.3255pt,275.6666pt) -- (97.3255pt,279.6666pt) -- (101.3255pt,275.6666pt) -- cycle;
\draw[pstyle6] (24pt,275.6666pt) -- (103.3255pt,275.6666pt);
\node at (31pt,266.8333pt)[below right,inner sep=0]{$P$};
\draw[pstyle7] (65.7255pt,287.6666pt) -- (123.9755pt,287.6666pt) -- (123.9755pt,289.6666pt) -- (113.9755pt,299.6666pt) -- (65.7255pt,299.6666pt) -- (65.7255pt,287.6666pt);
\draw[pstyle8] (65.7255pt,287.6666pt) rectangle (234.8182pt,339.6666pt);
\node at (80.7255pt,288.6666pt)[below right,color=black,inner sep=0]{\textbf{alt}};
\node at (138.9755pt,290.9166pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (142.1655pt,289.6666pt)[below right,inner sep=0]{$(1, \text{prove(}r\text{)}) \in P$};
\node at (215.6282pt,290.9166pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle9] (86.7255pt,314.6666pt) -- (86.7255pt,334.6666pt) -- (131.7255pt,334.6666pt) -- (131.7255pt,324.6666pt) -- (121.7255pt,314.6666pt) -- (86.7255pt,314.6666pt);
\draw[pstyle9] (121.7255pt,314.6666pt) -- (121.7255pt,324.6666pt) -- (131.7255pt,324.6666pt) -- (121.7255pt,314.6666pt);
\node at (92.7255pt,319.6666pt)[below right,color=black,inner sep=0]{break};
\draw[pstyle5] (277.3933pt,383.6666pt) -- (319.3933pt,383.6666pt);
\draw[pstyle5] (319.3933pt,383.6666pt) -- (319.3933pt,396.6666pt);
\draw[pstyle5] (278.3933pt,396.6666pt) -- (319.3933pt,396.6666pt);
\draw[pstyle4] (288.3933pt,392.6666pt) -- (278.3933pt,396.6666pt) -- (288.3933pt,400.6666pt) -- (284.3933pt,396.6666pt) -- cycle;
\node at (284.3933pt,371.6666pt)[below right,inner sep=0]{$ABdeliver()$};
\draw[pstyle4] (35pt,416.6666pt) -- (25pt,420.6666pt) -- (35pt,424.6666pt) -- (31pt,420.6666pt) -- cycle;
\draw[pstyle5] (29pt,420.6666pt) -- (276.3933pt,420.6666pt);
\node at (41pt,408.6666pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (265.3933pt,437.4999pt) -- (275.3933pt,441.4999pt) -- (265.3933pt,445.4999pt) -- (269.3933pt,441.4999pt) -- cycle;
\draw[pstyle6] (24pt,441.4999pt) -- (271.3933pt,441.4999pt);
\node at (31pt,432.6666pt)[below right,inner sep=0]{$P$};
\draw[pstyle9] (195.7533pt,454.4999pt) -- (195.7533pt,534.4999pt) -- (358.7533pt,534.4999pt) -- (358.7533pt,464.4999pt) -- (348.7533pt,454.4999pt) -- (195.7533pt,454.4999pt);
\draw[pstyle9] (348.7533pt,454.4999pt) -- (348.7533pt,464.4999pt) -- (358.7533pt,464.4999pt) -- (348.7533pt,454.4999pt);
\node at (201.7533pt,459.4999pt)[below right,color=black,inner sep=0]{line(C4)};
\node at (201.7533pt,470.4999pt)[below right,color=black,inner sep=0]{process P2 check locally if~};
\node at (201.7533pt,480.4999pt)[below right,inner sep=0]{$\forall j : (j, prove(r)) \not\in P$};
\node at (201.7533pt,491.4999pt)[below right,color=black,inner sep=0]{which is false since P1 correctly~};
\node at (201.7533pt,501.4999pt)[below right,color=black,inner sep=0]{PROVE(r) and APPEND(r)};
\node at (201.7533pt,511.4999pt)[below right,color=black,inner sep=0]{~};
\node at (201.7533pt,521.4999pt)[below right,inner sep=0]{$\text{P1 is next include in } W_r$};
\draw[pstyle4] (35pt,551.9399pt) -- (25pt,555.9399pt) -- (35pt,559.9399pt) -- (31pt,555.9399pt) -- cycle;
\draw[pstyle5] (29pt,555.9399pt) -- (276.3933pt,555.9399pt);
\node at (41pt,543.9399pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle4] (35pt,575.9399pt) -- (25pt,579.9399pt) -- (35pt,583.9399pt) -- (31pt,579.9399pt) -- cycle;
\draw[pstyle5] (29pt,579.9399pt) -- (276.3933pt,579.9399pt);
\node at (41pt,567.9399pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (265.3933pt,596.7732pt) -- (275.3933pt,600.7732pt) -- (265.3933pt,604.7732pt) -- (269.3933pt,600.7732pt) -- cycle;
\draw[pstyle6] (24pt,600.7732pt) -- (271.3933pt,600.7732pt);
\node at (31pt,591.9399pt)[below right,inner sep=0]{$P$};
\draw[pstyle9] (189.1283pt,613.7732pt) -- (189.1283pt,706.7732pt) -- (365.1283pt,706.7732pt) -- (365.1283pt,623.7732pt) -- (355.1283pt,613.7732pt) -- (189.1283pt,613.7732pt);
\draw[pstyle9] (355.1283pt,613.7732pt) -- (355.1283pt,623.7732pt) -- (365.1283pt,623.7732pt) -- (355.1283pt,613.7732pt);
\node at (195.1283pt,618.7732pt)[below right,color=black,inner sep=0]{line(C9)};
\node at (195.1283pt,629.7732pt)[below right,color=black,inner sep=0]{process P2 check locally if};
\node at (195.1283pt,639.7732pt)[below right,inner sep=0]{$\forall j \in W_r : prop[r][j] = \bot$};
\node at (195.1283pt,650.7732pt)[below right,color=black,inner sep=0]{which can't be false since P1 didn't};
\node at (195.1283pt,662.6982pt)[below right,color=black,inner sep=0]{execute~};
\node at (230.9483pt,660.7732pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\node at (195.1283pt,672.6982pt)[below right,color=black,inner sep=0]{~};
\node at (195.1283pt,682.6982pt)[below right,color=black,inner sep=0]{P2 will never progress and};
\node at (195.1283pt,692.6982pt)[below right,color=black,inner sep=0]{deliver any futur messages};
\end{tikzpicture}