const int T;

// Minimum probability that protocol terminates successfully by the deadline
Pmin=? [ F<=T "terminated_successfully" ]
// Minimum probability that protocol terminates successfully by the deadline
Pmax=? [ F<=T "terminated_successfully" ]