const int L;
// A leader is eventually elected with probability 1
P=? [ F "elected" ]
// Probability that a leader is eventually elected
P=? [ F "elected" ]
// Probability that a leader is elected within L steps
P=? [ F<=L "elected" ]
// Probability that a leader is elected within L rounds
P=? [ F<=(L*(N+1)) "elected" ]
// Expected time (num. rounds) to elect a leader
R{"num_rounds"}=? [ F "elected" ]