tempest/examples/mdp/consensus/coin.pctl

// C1 (with probability 1, all N processes finish the protocol)
// Pmin=? [ F finished ]

// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
// Results are same for v=1 and v=2 by symmetry
// Analytic bound is (K-1)/(2*K)
//Pmin=? [ F finished & all_coins_equal_0 ]
//Pmin=? [ F finished & all_coins_equal_1 ]

// Max probability of finishing protocol with coins not all equal
Pmax=? [ F finished & !agree ]

// Min/max probability of finishing within k steps
// Pmin=? [ F<=50 finished ]
// Pmax=? [ F<=50 finished ]

// Min/max expected steps to finish
// Rmin=? [ F finished ]
// Rmax=? [ F finished ]