Dining Philosopher with Dictionary Property Specifications as Never Claims

This page describes the dining philosopher with dictionary properties as Never Claims. For other property specification formalisms, click on the name of the property.

Adjacent Philosophers Not Eating property

never {
  do
    :: phil__1[phil_1_pid]@state_3 & 
       phil__2[phil_2_pid]@state_3 -> goto accept
    :: else -> skip 
  od;
  accept:
    do
      :: skip
    od
}
	

Not Eating While Holding Dictionary property

never {
  do
    ::phil__2[phil_2_pid]@state_4 &
      (holding_dictionary==true) -> goto accept
    ::else -> skip
  od;
  accept:
    do
      ::skip
    od
}
    

Back to Dining Philosophers with Dictionary

Back to main