// Minimum probability that the protocol terminates successfully
<<>>Pmin=? [ F "terminated_successfully" ]
<<p1>>Pmin=? [ F "terminated_successfully" ]
<<p2>>Pmin=? [ F "terminated_successfully" ]
<<p1,p2>>Pmin=? [ F "terminated_successfully" ]

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