54 lines
1.3 KiB
Plaintext
54 lines
1.3 KiB
Plaintext
@startuml
|
|
!pragma teoz true
|
|
|
|
database DL
|
|
actor P1
|
|
actor P2
|
|
P1 -> DL : <latex>READ()</latex>
|
|
DL --> P1 : <latex>P</latex>
|
|
P1 -> P1 : <latex>r_{max} = max\{r : (\_, prove(r)) \in P\}</latex>
|
|
|
|
loop <latex>\textbf{foreach } r \in \{r_{max} + 1, \dots\}</latex>
|
|
|
|
' P1 ->(05) P2 : <latex>RBcast(prop, S, r, 1)</latex>
|
|
|
|
P1 -> DL : <latex>PROVE(r)</latex>
|
|
P1 -> DL : <latex>APPEND(r)</latex>
|
|
|
|
P1 -> DL : <latex>READ()</latex>
|
|
DL --> P1 : <latex>P</latex>
|
|
|
|
alt <latex>(1, \text{prove(}r\text{)}) \in P</latex>
|
|
note over P1 : break
|
|
end
|
|
end
|
|
|
|
P2 -> P2 : <latex>ABdeliver()</latex>
|
|
P2 -> DL : <latex>READ()</latex>
|
|
DL --> P2 : <latex>P</latex>
|
|
note over P2
|
|
line(C4)
|
|
process P2 check locally if
|
|
<latex>\forall j : (j, prove(r)) \not\in P</latex>
|
|
which is false since P1 correctly
|
|
PROVE(r) and APPEND(r)
|
|
|
|
<latex>\text{P1 is next include in } W_r</latex>
|
|
end note
|
|
|
|
P2 -> DL : <latex>APPEND(r)</latex>
|
|
P2 -> DL : <latex>READ()</latex>
|
|
DL --> P2 : <latex>P</latex>
|
|
|
|
note over P2
|
|
line(C9)
|
|
process P2 check locally if
|
|
<latex>\forall j \in W_r : prop[r][j] = \bot</latex>
|
|
which can't be false since P1 didn't
|
|
execute <latex>RBcast(prop, S, r, 1)</latex>
|
|
|
|
P2 will never progress and
|
|
deliver any futur messages
|
|
end note
|
|
hide footbox
|
|
@enduml |