Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
EWD840.tla
EWD840_proof.tla
README.md
TLAPS.tla

README.md

Termination detection in a ring

A specification of Dijkstra's algorithm for termination detection in a ring. The algorithm was published as Edsger W. Dijkstra: Derivation of a termination detection algorithm for distributed computations. Inf. Proc. Letters 16:217-219 (1983). It appears as EWD 840.

The module EWD840 contains the specification of the algorithm in TLA+, as well as its correctness properties (and some non-properties) that can be model checked using TLC. You'll need to instantiate the parameter N by a concrete value, say, 4.

The module EWD840_proofs contains hierarchical proofs of type correctness and of the main safety property. These proofs can be checked using TLAPS.