const int K; // discrete time bound

// 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}]