Byzantská dohoda: Program
Program Byzantská dohoda
always
? ? y: y ? g :: d0[y] = false ? (B1)
? ? ? y, x:: obs0[y, x] = false ? (B2)
? ? ? r, y: 1 ? r ? t + 1 :: (E1)
dr[y] = dr?1[y] ? (conr[y, ?] ? r ? conr[y, g]) ?
{ „conr[y, ?]” je skratka za „? + z: conr[y, z] :: 1 ?” }
? ? ? y:: byz[y] = dt+1[y] ? (E2)
? ? ? r, y, x: 0 ? r ? t + 1 ::
obsr+1[y, x] = (obsr[y, x] ? sumr[y, x] > t
? valr[y, x]) (E3)
? valr[y, x] = dr[x] (E4)
? conr[y, x] = sumr[y, x] > 2.t ? (E5)
? ? ? r, y, z, x: 0 ? r ? t + 1 :: robsr[y, z, x] = obsr[z, x] ? (E6)
? ? ? r, y, z, x: 0 ? r ? t + 1 ::
sumr[y, x] = ? +z: robsr[y, z, x]:: 1 ? ? (E7)
Rovnice mozno usporiadat v správnom poradí (splnenie poziadavky pre always-sekciu):
(B1), (B2), (E6), (E7), (E4), (E3), (E5), (E1), (E2)