const int T;
// Minimum probability that a leader has been elected by deadline T
Pmin=? [ F<=T "done" ]