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