Dining philosophers problem. Chandy/Misra solution. TLA+
Don't forget to configure your model:
SPECIFICATION Spec
CONSTANT N = 5
PROPERTY
The following properties are provided to check states' sanity :
TypeInvariant
MutualExclusion
IndividualVivacity
GlobalVivacity