This page describes the dining philosopher properties as INCA queries. For other property specification formalisms, click on the name of the property.
Adjacent Philosophers Not Eating property
(defquery "no_p1p2" "nofair"
(omega-star-less
(sequence
(interval :initial t :open t
:ends-with '((rend "phil_1;fork_1.up")
(rend "phil_2;fork_2.up"))))))
Back to Dining Philosophers
Back to main