// player 1 can ensure that within 3 steps // a state in which the variable c equals 2 is reached // no matter the behaviour of the other players <<1>> P>=0.84 [ F<=3 c=2 ] // what is the minimum probability player 1 can ensure that // within 3 steps a state in which the variable c equals 2 is reached // no matter the behaviour of the other players <<1>> Pmin=? [ F<=3 c=2 ] // what is the maximum probability player 1 can ensure that // eventually a state in which the variable h equals 2 and variable c equals 0 is reached // no matter the behaviour of the other players <<1>> Pmax=? [ F (h=2 & c=0) ]