DirtyForksTLA

Dining philosophers problem. Chandy/Misra solution. TLA+

Model configuration

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

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
README.md		README.md
philosophes0.cfg		philosophes0.cfg
philosophes0.tla		philosophes0.tla