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" ]