const int K;

// Minimum probability that the protocol terminates successfully
//<<>>Pmax=? [ F "terminated_successfully" ]
//<<o>>Pmax=? [ F "terminated_successfully" ]
//<<r>>Pmax=? [ F "terminated_successfully" ]
//<<o,r>>Pmax=? [ F "terminated_successfully" ]

// Maximum probability that the protocol terminates successfully within time K
//<<>>Pmax=? [ F<=K "terminated_successfully" ]
<<o>>Pmax=? [ F<=K "terminated_successfully" ]
<<r>>Pmax=? [ F<=K "terminated_successfully" ]
//<<o,r>>Pmax=? [ F<=K "terminated_successfully" ]

// Minimum expected time for the protocol to terminate successfully
//<<>>Rmin=? [ F "terminated_successfully" ]
//<<o>>Rmin=? [ F "terminated_successfully" ]
//<<r>>Rmin=? [ F "terminated_successfully" ]
//<<o,r>>Rmin=? [ F "terminated_successfully" ]