Description:
The Not Eating While Holding Dictionary property says that a philosopher cannot start eatting while holding the dictionary.
Philosopher 1 holds the dictionary at the start of the program. Philosophers 2 through N where N is the size of the program start out not holding the dictionary. Using a symmetry argument for philosophers 2 through N, this property can be checked for a single philosopher. The results can then be generalized to the rest of the philosophers. This property is specified in terms of philosopher 2. This allows the same property specification to be used when the problem is scaled.
This property should be valid when analyzed by any of the finite state verification tools.
Specification:
Back to Dining Philosophers with Dictionary
Back to main