This page describes the reader/writer properties as INCA queries. For other property specification formalisms, click on the name of the property.
(defquery "no_w1w2" "nofair"
(omega-star-less
(sequence
(interval :initial t
:open t
:ends-with '("call(writer_1;control.start_write)"
"call(writer_2;control.start_write)")))))
Write-first property
(defquery "no_r1w" "nofair"
(omega-star-less
(sequence
(interval :initial t
:ends-with '((rend "reader_1;control.start_read"))
:forbid '((rend "writer_1;control.start_write")
(rend "writer_2;control.start_write"))))))
Back to Readers/Writers
Back to main