This page describes the dining philosopher with dictionary 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"))))))
Not Eating While Holding Dictionary property
(defquery "no_p2d" "nofair"
(omega-star-less
(sequence
(interval :initial t
:open t
:ends-with '((rend "phil_1;phil_2.dictionary")))
(interval :ends-with '((rend "phil_2;phil_3.dictionary"))))))
or
(defquery "no_p2d_con" "nofair"
(omega-star-less
(sequence
(interval :initial t
:open t
:ends-with '((rend "phil_2;fork_2.up"))
:constraints '((<=(- "call(phil_2;phil_3.dictionary)"
"call(phil_1;phil_2.dictionary)")-1))))))
Back to Dining Philosophers with Dictionary
Back to main