Refine EWD998 animation formatting and the modules documentation.

Changed EWD998ChanID's Init predicate to allow nodes to initially
be active and inactive, which is required for the animation to be
interesting.

Co-authored-by: Claude Sonnet 4.5 <[email protected]>
Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

specifications/ewd998/EWD998ChanID.tla

@@ -96,7 +96,7 @@ Init ==
                               THEN << [type |-> "tok", q |-> 0, color |-> "black", vc |-> clock[n] ] >> 
                               ELSE <<>>] \* with empty channels.
   (* EWD840 *) 
-  /\ active \in [Node -> {FALSE}]
+  /\ active \in [Node -> BOOLEAN]
   /\ color \in [Node -> {"black"}]
   /\ passes = IF terminated THEN 0 ELSE -1