Formalization, by specification refinement, of token-based mutual exclusion algorithms
- oneToken.mlw: abstract spec of single-token systems
- selfstab-ring.mlw: Dijkstra's unidirectional ring system (stable phase, closure property)
- selfstab-biarray-2states.mlw: Dijkstra's bidirectional array system (stable phase, closure property)