Dining Philosopher with Dictionary Property Specifications as QREs

This page describes the dining philosopher with dictionary properties as Quantified Regular Expressions (QREs). For other property specification formalisms, click on the name of the property.

Adjacent Philosophers Not Eating property

for events { {phil_1_eating}, {phil_1_not_eating},
             {phil_2_eating}, {phil_2_not_eating} } 
    
show all executions satisfy

[-{phil_1_eating}, {phil_2_eating}]*; 
(
  (
    ( {phil_1_eating}; 
      [-{phil_2_eating}, {phil_1_not_eating}]*; 
      {phil_1_not_eating}
    ) 
    |
    ( {phil_2_eating}; 
      [-{phil_1_eating}, {phil_2_not_eating}]*; 
      {phil_2_not_eating}
    )
  ); 
  [-{phil_1_eating}, {phil_2_eating}]* 
)*
	

Not Eating While Holding Dictionary property

for events { {dpd_phil_2_dictionary}, {dpd_phil_3_dictionary}, {phil_2_eating} }

show all executions satisfy

[-{dpd_phil_2_dictionary}]*;
( {dpd_phil_2_dictionary};
  [-{phil_2_eating}, {dpd_phil_3_dictionary}]*;
  {dpd_phil_3_dictionary};
  [-{dpd_phil_2_dictionary}]*
)*
    

Back to Dining Philosophers with Dictionary

Back to main