const int K; // discrete time bound

label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8));
label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9);

// liveness (if a philosopher is hungry then eventually some philosopher eats)
"hungry" => P>=1 [ true U "eat"]

// bounded waiting (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps)
Pmin=?[true U<=K "eat" {"hungry"}{min}]

// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats)
Rmax=?[F "eat" {"hungry"}{max}]