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