% 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,line width=1.0pt}
,pstyle5/.style={color=plantucolor0001,fill=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}
,pstyle10/.style={color=plantucolor0001,fill=plantucolor0005,line width=0.5pt}
]
\draw[pstyle0] (20.5pt,75pt) rectangle (28.5pt,537.1498pt);
\draw[pstyle1] (24pt,75pt) -- (24pt,537.1498pt);
\draw[pstyle0] (105.8255pt,75pt) rectangle (113.8255pt,537.1498pt);
\draw[pstyle1] (109.3255pt,75pt) -- (109.3255pt,537.1498pt);
\draw[pstyle0] (273.8933pt,75pt) rectangle (281.8933pt,537.1498pt);
\draw[pstyle1] (277.3933pt,75pt) -- (277.3933pt,537.1498pt);
\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 (269.5983pt,65pt)[below right,color=black,inner sep=0]{Pi};
\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] (109.3255pt,99pt) -- (151.3255pt,99pt);
\draw[pstyle4] (151.3255pt,99pt) -- (151.3255pt,112pt);
\draw[pstyle4] (110.3255pt,112pt) -- (151.3255pt,112pt);
\draw[pstyle5] (120.3255pt,108pt) -- (110.3255pt,112pt) -- (120.3255pt,116pt) -- (116.3255pt,112pt) -- cycle;
\node at (116.3255pt,87pt)[below right,inner sep=0]{$ABcast(m)$};
\draw[pstyle4] (109.3255pt,133.2243pt) -- (151.3255pt,133.2243pt);
\draw[pstyle4] (151.3255pt,133.2243pt) -- (151.3255pt,146.2243pt);
\draw[pstyle4] (110.3255pt,146.2243pt) -- (151.3255pt,146.2243pt);
\draw[pstyle5] (120.3255pt,142.2243pt) -- (110.3255pt,146.2243pt) -- (120.3255pt,150.2243pt) -- (116.3255pt,146.2243pt) -- cycle;
\node at (116.3255pt,124pt)[below right,inner sep=0]{$m \in S$};
\draw[pstyle5] (35pt,166.2243pt) -- (25pt,170.2243pt) -- (35pt,174.2243pt) -- (31pt,170.2243pt) -- cycle;
\draw[pstyle4] (29pt,170.2243pt) -- (108.3255pt,170.2243pt);
\node at (41pt,158.2243pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle5] (97.3255pt,187.0576pt) -- (107.3255pt,191.0576pt) -- (97.3255pt,195.0576pt) -- (101.3255pt,191.0576pt) -- cycle;
\draw[pstyle6] (24pt,191.0576pt) -- (103.3255pt,191.0576pt);
\node at (31pt,182.2243pt)[below right,inner sep=0]{$P$};
\draw[pstyle4] (109.3255pt,215.0576pt) -- (151.3255pt,215.0576pt);
\draw[pstyle4] (151.3255pt,215.0576pt) -- (151.3255pt,228.0576pt);
\draw[pstyle4] (110.3255pt,228.0576pt) -- (151.3255pt,228.0576pt);
\draw[pstyle5] (120.3255pt,224.0576pt) -- (110.3255pt,228.0576pt) -- (120.3255pt,232.0576pt) -- (116.3255pt,228.0576pt) -- cycle;
\node at (116.3255pt,203.0576pt)[below right,inner sep=0]{$r_{max} = max\{r : (\_, prove(r)) \in P\}$};
\draw[pstyle7] (8pt,240.0576pt) -- (74.4pt,240.0576pt) -- (74.4pt,242.0576pt) -- (64.4pt,252.0576pt) -- (8pt,252.0576pt) -- (8pt,240.0576pt);
\draw[pstyle8] (8pt,240.0576pt) rectangle (293.4464pt,513.1498pt);
\node at (23pt,241.0576pt)[below right,color=black,inner sep=0]{\textbf{loop}};
\node at (89.4pt,243.3076pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (92.59pt,242.0576pt)[below right,inner sep=0]{$\textbf{foreach } r \in \{r_{max} + 1, \dots\}$};
\node at (215.4514pt,243.3076pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle5] (265.5167pt,278.762pt) -- (275.3933pt,283.0576pt) -- (265.2788pt,286.7585pt) -- (269.396pt,282.8792pt) -- cycle;
\draw[pstyle4] (109.3255pt,278.0576pt) -- (275.3933pt,283.0576pt);
\node at (116.3255pt,266.0576pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\draw[pstyle5] (35pt,303.0576pt) -- (25pt,307.0576pt) -- (35pt,311.0576pt) -- (31pt,307.0576pt) -- cycle;
\draw[pstyle4] (29pt,307.0576pt) -- (108.3255pt,307.0576pt);
\node at (41pt,295.0576pt)[below right,inner sep=0]{$PROVE(r)$};
\draw[pstyle5] (35pt,327.0576pt) -- (25pt,331.0576pt) -- (35pt,335.0576pt) -- (31pt,331.0576pt) -- cycle;
\draw[pstyle4] (29pt,331.0576pt) -- (108.3255pt,331.0576pt);
\node at (41pt,319.0576pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle5] (35pt,351.0576pt) -- (25pt,355.0576pt) -- (35pt,359.0576pt) -- (31pt,355.0576pt) -- cycle;
\draw[pstyle4] (29pt,355.0576pt) -- (108.3255pt,355.0576pt);
\node at (41pt,343.0576pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle5] (97.3255pt,371.8909pt) -- (107.3255pt,375.8909pt) -- (97.3255pt,379.8909pt) -- (101.3255pt,375.8909pt) -- cycle;
\draw[pstyle6] (24pt,375.8909pt) -- (103.3255pt,375.8909pt);
\node at (31pt,367.0576pt)[below right,inner sep=0]{$P$};
\draw[pstyle7] (65.7255pt,387.8909pt) -- (123.9755pt,387.8909pt) -- (123.9755pt,389.8909pt) -- (113.9755pt,399.8909pt) -- (65.7255pt,399.8909pt) -- (65.7255pt,387.8909pt);
\draw[pstyle8] (65.7255pt,387.8909pt) rectangle (268.4464pt,499.1498pt);
\node at (80.7255pt,388.8909pt)[below right,color=black,inner sep=0]{\textbf{alt}};
\node at (138.9755pt,391.1409pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (142.1655pt,389.8909pt)[below right,inner sep=0]{$(1, \text{prove(}r\text{)}) \in P$};
\node at (215.6282pt,391.1409pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[color=black,line width=1.0pt,dash pattern=on 2.0pt off 2.0pt] (65.7255pt,450.8909pt) -- (268.4464pt,450.8909pt);
\node at (70.7255pt,454.1498pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (73.9155pt,452.8909pt)[below right,inner sep=0]{$(\exists j, r' : (j, prove(r')) \in P \land m \in prop[r'][j])$};
\node at (263.2564pt,454.1498pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle10] (86.7255pt,414.8909pt) -- (86.7255pt,434.8909pt) -- (131.7255pt,434.8909pt) -- (131.7255pt,424.8909pt) -- (121.7255pt,414.8909pt) -- (86.7255pt,414.8909pt);
\draw[pstyle10] (121.7255pt,414.8909pt) -- (121.7255pt,424.8909pt) -- (131.7255pt,424.8909pt) -- (121.7255pt,414.8909pt);
\node at (92.7255pt,419.8909pt)[below right,color=black,inner sep=0]{break};
\draw[pstyle10] (86.7255pt,474.1498pt) -- (86.7255pt,494.1498pt) -- (131.7255pt,494.1498pt) -- (131.7255pt,484.1498pt) -- (121.7255pt,474.1498pt) -- (86.7255pt,474.1498pt);
\draw[pstyle10] (121.7255pt,474.1498pt) -- (121.7255pt,484.1498pt) -- (131.7255pt,484.1498pt) -- (121.7255pt,474.1498pt);
\node at (92.7255pt,479.1498pt)[below right,color=black,inner sep=0]{break};
\end{tikzpicture}