--------------------------- MODULE CycleDetection ---------------------------
EXTENDS TLC, Naturals, FiniteSets, Sequences
CONSTANT N, NIL
\* Put the constraint on N
ASSUME NIsPositive == N \in (Nat \ {0})
\* Put the constraint on NIL
ASSUME NilIsNotInN == NIL \notin 1..N
\* Represents the set of nodes
Nodes == 1..N
\*Init position of hare and tortoise
InitPos == 1
VARIABLES linkedList, tortoise, hare, cycleDetected, pc
vars == << linkedList, tortoise, hare, cycleDetected, pc >>
\* Check if the linkedList is a valid singly linked linkedList (may have cycle)
IsValidLinkedList(l) == \A n \in Nodes :
\/ /\ n = N
/\ l[n] \in ((Nodes \union {NIL}) \ {n})
\/ l[n] = n + 1
ValidlinkedListsSet == {l \in [Nodes -> Nodes \union {NIL}] : IsValidLinkedList(l) }
Init == /\ linkedList \in ValidlinkedListsSet
/\ tortoise = InitPos
/\ hare = InitPos
/\ cycleDetected = FALSE
/\ pc = "MoveTortoise"
MoveTortoise ==
/\ pc = "MoveTortoise"
/\ tortoise' = IF tortoise # NIL THEN linkedList[tortoise] ELSE NIL
/\ pc' = "MoveHare"
/\ UNCHANGED << linkedList, hare, cycleDetected >>
MoveHare ==
/\ pc = "MoveHare"
/\ hare' = IF (hare = NIL \/ linkedList[hare] = NIL) THEN NIL ELSE linkedList[linkedList[hare]]
/\ pc' = "Check"
/\ UNCHANGED << linkedList, tortoise, cycleDetected >>
Check ==
/\ pc = "Check"
/\ cycleDetected' = (tortoise = hare)
/\ pc' = IF (tortoise = NIL \/ hare = NIL \/ (tortoise = hare)) THEN "Done" ELSE "MoveTortoise"
/\ UNCHANGED << linkedList, tortoise, hare >>
Next == MoveTortoise \/ MoveHare \/ Check \/ (pc = "Done" /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
TypeInvariant ==
/\ pc \in {"MoveTortoise", "MoveHare", "Done", "Check"}
/\ cycleDetected \in BOOLEAN
/\ tortoise \in (Nodes \union {NIL})
/\ hare \in (Nodes \union {NIL})
Termination == <> (pc = "Done")
=============================================================================