ewd998: move RECURSIVE SimpleCycle from Utils.tla to EWD998_anim.tla

TLAPS does not currently support RECURSIVE *operators*, so any
module that EXTENDS Utils.tla (EWD998Chan, EWD998ChanID, EWD998PCal)
fails to load.  Inline the operator into its sole caller
EWD998_anim.tla so Utils.tla loads under TLAPS again.  Existing
EWD998 / ATD proofs unchanged.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/ewd998/EWD998Chan.tla

@@ -5,7 +5,7 @@
 (* Shmuel Safra's version of termination detection.                        *)
 (* Contrary to EWD998, this variant models message channels as sequences.  *)
 (***************************************************************************)
-EXTENDS Integers, Sequences, FiniteSets, Utils
+EXTENDS Integers, Sequences, SequencesExt, FiniteSets, Utils
 
 CONSTANT N
 ASSUME NAssumption == N \in Nat \ {0} \* At least one node.

specifications/ewd998/EWD998_anim.tla

@@ -37,6 +37,21 @@
  ***************************************************************************)
 EXTENDS EWD998ChanID, SVG, TLC
 
+(***************************************************************************)
+(* SimpleCycle is a recursive variant of the predicate IsSimpleCycle from  *)
+(* Utils.tla.  It does not work with PlusPy or TLAPS but is orders of      *)
+(* magnitude faster when evaluated by TLC, which is why it lives here     *)
+(* inline in the animation module rather than in Utils.tla.              *)
+(***************************************************************************)
+SimpleCycle(S) ==
+    LET sts == LET SE == INSTANCE SequencesExt IN SE!SetToSeq(S)
+        RECURSIVE SimpleCycleRec(_,_,_)
+        SimpleCycleRec(seq, prefix, i) ==
+            IF i = Len(seq)
+            THEN prefix @@ (seq[i] :> seq[1])
+            ELSE SimpleCycleRec(seq, prefix @@ (seq[i] :> seq[i+1]), i+1)
+    IN SimpleCycleRec(sts, sts[1] :> sts[2], 2)
+
 \* Deterministic node ordering: ensures nodes appear in consistent positions
 \* across all animation frames (Best Practice from Animation Guide)
 SomeRingOfNodes == SimpleCycle(Node)

specifications/ewd998/Utils.tla

@@ -1,5 +1,5 @@
 ------------------------------- MODULE Utils -------------------------------
-EXTENDS Integers, Sequences, FiniteSets, TLC, Functions, SequencesExt
+EXTENDS Integers, Sequences, FiniteSets, Functions
 
 \* No support for RECURSIVE in PlusPy.
 IsSimpleCycle(S, r) ==
@@ -13,16 +13,4 @@ IsSimpleCycle(S, r) ==
               IN << r[head] >> \o F[i-1]
   IN Range(F[Cardinality(S)]) = S
 
-\* SimpleCycle is a recursive variant of the predicate IsSimpleCycle above. It
-\* does not work with PlusPy, but is orders of magnitude faster when evaluated
-\* by TLC.
-SimpleCycle(S) ==
-    LET sts == LET SE == INSTANCE SequencesExt IN SE!SetToSeq(S)
-        RECURSIVE SimpleCycle(_,_,_)
-        SimpleCycle(seq, prefix, i) ==
-            IF i = Len(seq)
-            THEN prefix @@ (seq[i] :> seq[1])
-            ELSE SimpleCycle(seq, prefix @@ (seq[i] :> seq[i+1]), i+1)
-    IN SimpleCycle(sts, sts[1] :> sts[2], 2)
-
 =============================================================================

specifications/ewd998/manifest.json

@@ -201,4 +201,4 @@
       "models": []
     }
   ]
-}
+}