Description:
The Adjacent Philosophers Not Eating property says that no two philosophers may be eating at the same time.
The philosophers all behave in a symmetric way with regard to their forks. Due to this, it is sufficient to check this property for only two philosophers. If these two philosophers use their forks in a mutually exclusive fashion, then all pairs of philosophers will. This property is specified in terms of philosopher 1 and 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
Back to main