// deadlock freeness
filter(forall, "hungry" => P>=1 [ F "eat"])

// no resource starvation
filter(forall, "hungry1" => P>=1 [ F "eat1"])
filter(forall, "hungry2" => P>=1 [ F "eat2"])
filter(forall, "hungry3" => P>=1 [ F "eat3"])