Tla-tortoise-hare Specification's authors: Lorin Hochstein Original paper: Floyd's Cycle Detection Algorithm (The Tortoise and the Hare) Extended modules: Nat Computation models: no faults Some properties checked with TLC: termination, partial correctness TLA+ files