Reader/Writer Property Specifications as QREs

This page describes the reader/writer properties as Quantified Regular Expressions ( QREs ). For other property specification formalisms, click on the name of the property.

Exclusive-write property
for events { {writer_1_start_write}, {writer_1_stop_write},
             {writer_2_start_write}, {writer_2_stop_write} } 
show all executions satisfy

[-{writer_1_start_write}, {writer_2_start_write}]*; 
    ( {writer_1_start_write}; 
      [-{writer_2_start_write}, {writer_1_stop_write}]*; 
    ( {writer_2_start_write}; 
      [-{writer_1_start_write}, {writer_2_stop_write}]*; 
  [-{writer_1_start_write}, {writer_2_start_write}]* 

Write-first property

for events { {reader_1_start_read}, {any_writer_wrote} }

show no executions satisfy
[-{reader_1_start_read} , {any_writer_wrote}]*;
{reader_1_start_read} ;
[{reader_1_start_read} , {any_writer_wrote}]*

Back to Readers/Writers

Back to main