diff --git a/specifications/ewd998/EWD998_anim.tla b/specifications/ewd998/EWD998_anim.tla index c09ba20a..df57d5ff 100644 --- a/specifications/ewd998/EWD998_anim.tla +++ b/specifications/ewd998/EWD998_anim.tla @@ -1,189 +1,526 @@ -------------------------------- CONFIG EWD998_anim ------------------------------- -CONSTANTS - Node = {"a", "b", "c", "d", "e", "f"} - RingOfNodes <- SomeRingOfNodes - -SPECIFICATION - Spec - -ALIAS - Alias - -\* HowTo Graphical Debugging (https://youtu.be/IO9ik850i0M): -\* - Uncomment ACTION_CONSTRAINT ToSVG and comment INVARIANT AnimInv instead -\* - Remove prime from plsN in Messages (no double-priming allowed in TLA+) -\* - Remove ", Solid: Arrival in next" from Labels (makes no sense in this mode) -\* - Run TLC with "-config EWD998_anim.tla EWD998_anim -simulate -note -debugger" -\* - Attach the VSCode debugger to the running TLC process -\* ACTION_CONSTRAINT -\* ToSVG - -INVARIANT - AnimInv -================================================================================== - ------------------------------- MODULE EWD998_anim ------------------------------- -EXTENDS EWD998ChanID, SVG, TLC, IOUtils - -SomeRingOfNodes == - SimpleCycle(Node) - +(*************************************************************************** + * EWD998 Termination Detection Animation + * + * This animation file visualizes Dijkstra's EWD998 distributed termination + * detection algorithm. It shows a ring of nodes passing a token, where each + * node can be active/inactive and white/black (tainted). The animation + * displays: + * - Node states (active=circle, inactive=square; white/black coloring) + * - Message counters tracking sent/received messages + * - Token position and state (color + queue count) + * - Messages in flight between nodes + * - System status (RUNNING/TERMINATED/DETECTED) + * + * How Animation Works (Conceptual): + * Animation in TLA+ is an action-level formula. This means the animation + * operators have access to BOTH the current state (unprimed variables + * like `inbox`) AND the next state (primed variables like `inbox'`). + * The animation translates this state transition into an SVG frame that + * visualizes the system at that moment. + * + * Key insight: Because we have both states, we can show: + * - What's happening NOW (current state values) + * - What's about to happen NEXT (by comparing current vs. next state) + * + * Architecture: + * - Extends EWD998ChanID (the base specification with channels) + * - Uses SVG module for visual elements and file serialization + * - Uses TLC for state inspection (TLCGet("level")) + * + * Best Practices Applied: + * - Deterministic ordering using SimpleCycle for consistent rendering + * - Consistent viewBox (760×420) across all frames + * - Step number displayed in bottom-right corner + * - Modular visual components (Legend, Status, Nodes, Token, Messages) + * - Clear visual language with legend explaining all symbols + ***************************************************************************) +EXTENDS EWD998ChanID, SVG, TLC + +\* Deterministic node ordering: ensures nodes appear in consistent positions +\* across all animation frames (Best Practice from Animation Guide) +SomeRingOfNodes == SimpleCycle(Node) + +\* Aliased state variables from the EWD998Chan specification for convenience token == EWD998Chan!token tpos == EWD998Chan!tpos +--------------------------------------------------------------------------- +\* VISUAL CONSTANTS AND POSITIONING +\* +\* This section defines the layout structure for the animation, including +\* font styles, positioning coordinates, and spacing. All positions are +\* calculated to fit within the 760×420 viewBox. +--------------------------------------------------------------------------- + +\* Font style definitions for consistent typography throughout the animation +Arial == [font |-> "Arial, sans-serif", font_size |-> "12"] +ArialSmall == [font |-> "Arial, sans-serif", font_size |-> "11", font_weight |-> "bold"] +ArialXSmall == [font |-> "Arial, sans-serif", font_size |-> "10", font_weight |-> "bold"] +ArialBold == [font |-> "Arial, sans-serif", font_size |-> "14", font_weight |-> "bold"] +ArialTitle == [font |-> "Arial, sans-serif", font_size |-> "18", font_weight |-> "bold"] + +\* Top-left position for legend and title (20px from left, 30px from top) +LegendBasePos == [ x |-> 20, y |-> 30 ] + +\* Ring network layout: centered horizontally in viewBox +\* w: x-coordinate of ring center (380 = 760/2, horizontally centered) +\* h: y-coordinate of ring center (55px from top) +\* r: radius of the ring in pixels +RingBasePos == [w |-> 380, h |-> 55, r |-> 85] + +\* Token path layout: concentric with node ring but with larger radius +\* The offset (15px in x/y, 30px additional radius) creates visual separation +\* so the token doesn't overlap with nodes. This makes the token path clearly +\* distinguishable from the node ring. +TokenBasePos == [ w |-> RingBasePos.w + 15, + h |-> RingBasePos.h + 15, + r |-> RingBasePos.r + 30 ] --------------------------------------------------------------------------- +\* COLOR SCHEME +\* +\* Defines the visual language of the animation. Colors are chosen for: +\* - Clarity: distinct colors for different states +\* - Semantics: intuitive mapping (green=success, red=running, etc.) +\* - Accessibility: sufficient contrast for readability +--------------------------------------------------------------------------- -Arial == [font |-> "Arial"] +Colors == [ + nodeWhite |-> "#f8f9fa", \* Light gray: untainted (white) node background + nodeBlack |-> "#343a40", \* Dark gray: tainted (black) node background + tokenWhite |-> "#ffc107", \* Amber/yellow: white token (no tainted nodes encountered) + tokenBlack |-> "#6f42c1", \* Purple: black token (encountered a tainted node) + message |-> "#ff6b6b", \* Bright red: message arriving now + messageInFlight |-> "#ff9a9a", \* Light red: message in-flight (arriving next state) + statusRunning |-> "#dc3545", \* Red: system is running + statusTerminated |-> "#ffc107", \* Yellow/amber: system has terminated but not detected + statusDetected |-> "#28a745", \* Green: termination successfully detected + text |-> "#212529", \* Dark text for labels + counter |-> "#0066cc" \* Blue: message counter display +] -LegendBasePos == [ x |-> -5, y |-> 25 ] +--------------------------------------------------------------------------- +\* TITLE AND LEGEND +\* +\* The legend provides a visual key to help viewers understand the animation. +\* It explains the meaning of shapes, colors, and symbols used throughout. +\* This is a best practice for making animations self-documenting. +--------------------------------------------------------------------------- + +Title == + Text(LegendBasePos.x, LegendBasePos.y, + "EWD998 Termination Detection", + ArialTitle @@ [fill |-> Colors.text]) + +Legend == + Group(<< + Title, + \* Left column: Node state explanations + Text(LegendBasePos.x, LegendBasePos.y + 25, + "● Round node = Active ■ Square node = Inactive", + Arial @@ [fill |-> Colors.text]), + Text(LegendBasePos.x, LegendBasePos.y + 42, + "White/Light = Untainted Black/Dark = Tainted", + Arial @@ [fill |-> Colors.text]), + Text(LegendBasePos.x, LegendBasePos.y + 59, + "Counter (C:n) tracks sent/received messages", + Arial @@ [fill |-> Colors.counter]), + \* Right column: Token and message explanations + Text(LegendBasePos.x + 350, LegendBasePos.y + 25, + "Token: ◯ = white ● = black", + Arial @@ [fill |-> Colors.text]), + Text(LegendBasePos.x + 350, LegendBasePos.y + 42, + "Lines = Messages Dashed = In-flight", + Arial @@ [fill |-> Colors.text]) + >>, <<>>) -RingBasePos == [w |-> 55, h |-> 55, r |-> 75] +--------------------------------------------------------------------------- +\* STATUS DISPLAY +\* +\* Shows the current state of the termination detection algorithm. +\* Three possible states are displayed with distinct colors: +\* - RUNNING (red): System is active, nodes may still be processing +\* - TERMINATED (yellow): All nodes are inactive, but not yet detected +\* - TERM. DETECTED (green): Termination successfully detected by algorithm +\* +\* This provides immediate feedback about whether the algorithm has completed +\* its goal of detecting termination. +--------------------------------------------------------------------------- -\* 12pts (x/y) offset to be concentric with RingNetwork. -TokenBasePos == [ w |-> RingBasePos.w + 12, - h |-> RingBasePos.h + 12, - r |-> RingBasePos.r + 25 ] +StatusInfo == + LET \* Query the underlying specification for termination state + isTerminated == EWD998Chan!EWD998!Termination + isDetected == EWD998Chan!EWD998!terminationDetected + \* Determine status text based on current state + statusText == IF isDetected THEN "TERM. DETECTED" + ELSE IF isTerminated THEN "TERMINATED" + ELSE "RUNNING" + \* Color-code the status for quick visual recognition + statusColor == IF isDetected THEN Colors.statusDetected + ELSE IF isTerminated THEN Colors.statusTerminated + ELSE Colors.statusRunning + IN Group(<< + \* Status box: rounded rectangle background + Rect(LegendBasePos.x + 550, LegendBasePos.y - 10, 160, 35, + [fill |-> statusColor, + stroke |-> Colors.text, + stroke_width |-> "2", + rx |-> "8", \* Rounded corners + opacity |-> "0.9"]), + \* Status text: white text centered in the box + Text(LegendBasePos.x + 630, LegendBasePos.y + 13, statusText, + ArialBold @@ [fill |-> "#ffffff", text_anchor |-> "middle"]) + >>, <<>>) --------------------------------------------------------------------------- -\* Labels +\* STEP NUMBER DISPLAY +\* +\* Best Practice (from Animation Guide): Every animation frame MUST include +\* a step number to track progression through the state space. The step +\* number should appear in a consistent location across all frames, similar +\* to page numbers in documents. +\* +\* TLCGet("level") returns the current depth in the state graph exploration. +--------------------------------------------------------------------------- -Labels == Group(<>, - <<>>) +StepNumber == + Text(730, 405, "Step " \o ToString(TLCGet("level")), + ("text-anchor" :> "end" @@ \* Right-aligned + "font-size" :> "12px" @@ + "font-family" :> "monospace" @@\* Monospace for consistent digit width + "fill" :> "#666")) \* Subtle gray color --------------------------------------------------------------------------- -NodeDimension == 26 +\* NODE RENDERING +\* +\* Nodes are the core elements of the algorithm. Each node has multiple +\* visual properties that encode its state: +\* - Shape: Circle if active, Square if inactive +\* - Color: Light (white) if untainted, Dark (black) if tainted +\* - Label: Node ID number centered in the shape +\* - Counter: "C:n" display below showing message balance +\* +\* The node ring is positioned using NodeOfRingNetwork, which calculates +\* polar coordinates for evenly-spaced nodes around a circle. +\* +\* Compatibility Note: NodeOfRingNetwork is not implemented in Spectacle, +\* making this animation incompatible with Spectacle's animation viewer. +--------------------------------------------------------------------------- + +NodeDimension == 30 \* Width/height of square nodes +NodeRadius == 15 \* Radius of circular nodes (also half of NodeDimension) -\* Centers the line/circle at the center of a node instead of -\* a node's left upper corner (which are its 0:0 coordinates). -ArrowPosOffset == NodeDimension \div 2 +\* ArrowPosOffset: Centers message line endpoints at node centers. +\* SVG Rect coordinates specify the top-left corner, but Circle coordinates +\* specify the center, so we add NodeRadius to align message arrows properly. +ArrowPosOffset == NodeRadius -\* Ring Network +\* Ring Network: Creates visual representation of all nodes in the ring RingNetwork == - LET RN[ n \in Node ] == - LET coord == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, node2nat[n], N) - id == Text(coord.x + ArrowPosOffset + 2, coord.y + ArrowPosOffset + 7, ToString(counter[n]), - Arial @@ [fill |-> CHOOSE c \in Color : c # color[n]]) - node == Rect(coord.x, coord.y, NodeDimension, NodeDimension, - \* round (rx=15) if node is active. - [rx |-> IF ~active[n] THEN "0" ELSE "15", - stroke |-> "black", - fill |-> color[n]]) - IN Group(<>, ("transform" :> "translate(0 125)")) + LET \* Function that creates a visual element for each node + RN[ n \in Node ] == + LET \* Calculate (x,y) position for this node on the ring + coord == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, node2nat[n], N) + + \* Map node color state to visual colors + \* "white" nodes are untainted (have not sent messages while black) + \* "black" nodes are tainted (have sent messages while black) + nodeColor == IF color[n] = "white" + THEN Colors.nodeWhite + ELSE Colors.nodeBlack + \* Text color contrasts with node color for readability + textColor == IF color[n] = "white" + THEN Colors.nodeBlack + ELSE Colors.nodeWhite + + \* Node shape encodes activity status: + \* Active nodes = Circle (nodes that can still send/receive messages) + \* Inactive nodes = Square/Rectangle (idle nodes) + node == IF active[n] + THEN Circle(coord.x + NodeRadius, coord.y + NodeRadius, NodeRadius, + [fill |-> nodeColor, + stroke |-> Colors.text, + stroke_width |-> "2.5", + opacity |-> "0.95"]) + ELSE Rect(coord.x, coord.y, NodeDimension, NodeDimension, + [fill |-> nodeColor, + stroke |-> Colors.text, + stroke_width |-> "2.5", + rx |-> "3", \* Slightly rounded corners + opacity |-> "0.95"]) + + \* Node ID label: displays the node number inside the shape + id == Text(coord.x + NodeRadius, coord.y + NodeRadius + 5, + ToString(node2nat[n]), + Arial @@ [fill |-> textColor, + text_anchor |-> "middle", + font_weight |-> "bold"]) + + \* Counter display: tracks message balance (sent minus received) + \* Positive = sent more messages than received + \* Zero = balanced, meaning no messages in transit from this node + \* All counters must be zero for valid termination detection + cnt == Text(coord.x + NodeRadius, coord.y + NodeDimension + 18, + "C:" \o ToString(counter[n]), + ArialSmall @@ [fill |-> Colors.counter, + text_anchor |-> "middle"]) + IN Group(<>, ("transform" :> "translate(0 180)")) \* Vertical offset IN Group(RN, <<>>) --------------------------------------------------------------------------- -\* Token ring (with larger radius than ring above and only visible at the node that currently holds the token). +\* TOKEN VISUALIZATION +\* +\* The token is a key element of EWD998. It circulates around the ring to +\* detect termination. The token carries two pieces of information: +\* 1. color: "white" or "black" (tracks if any node was black when passed) +\* 2. q: queue count accumulator (sum of counters from nodes that passed it) +\* +\* Visual representation: +\* - Position: Moves around a larger concentric circle (TokenBasePos) +\* - Color: Amber/yellow for white, Purple for black +\* - Content: Displays the queue count (q value) inside the circle +\* - Label: "Token" text above the circle +\* +\* The token path radius is larger than the node ring to prevent overlap +\* and make the token's movement clearly visible. +--------------------------------------------------------------------------- + TokenNetwork == - LET coord == NodeOfRingNetwork(TokenBasePos.w, TokenBasePos.h, TokenBasePos.r, tpos, N) - circ == Circle(coord.x-2, coord.y, 8, [stroke |-> "black", fill |-> token.color]) - id == Text(coord.x - 5, coord.y + 3, ToString(token.q), [font |-> "Arial", fill |-> CHOOSE c \in Color : c # token.color ]) - \* Group always expects a sequence! - IN Group(<>, ("transform" :> "translate(0 125)")) + LET \* Calculate token position on its dedicated ring (concentric, larger radius) + coord == NodeOfRingNetwork(TokenBasePos.w, TokenBasePos.h, TokenBasePos.r, tpos, N) + + \* Token color encoding: + \* White token (yellow/amber) = has not encountered any black nodes + \* Black token (purple) = has encountered at least one black node + tokenColor == IF token.color = "white" + THEN Colors.tokenWhite + ELSE Colors.tokenBlack + \* Text color for queue value inside token + textColor == IF token.color = "white" + THEN Colors.nodeBlack + ELSE "#ffffff" + + \* Token circle: larger and more prominent than node circles + circ == Circle(coord.x + 10, coord.y + 10, 12, + [fill |-> tokenColor, + stroke |-> Colors.text, + stroke_width |-> "2.5", + opacity |-> "1.0"]) + + \* Queue count display: shows accumulated counter sum (q value) + \* As the token circulates, each node adds its counter to q + \* When token completes a round with q=0 and color=white, termination is detected + qVal == Text(coord.x + 10, coord.y + 15, ToString(token.q), + ArialSmall @@ [fill |-> textColor, + text_anchor |-> "middle"]) + + \* "Token" label above the circle for identification + label == Text(coord.x + 10, coord.y - 5, "Token", + ArialXSmall @@ [fill |-> Colors.text, + text_anchor |-> "middle"]) + IN Group(<>, ("transform" :> "translate(0 180)")) \* Vertical offset --------------------------------------------------------------------------- -\* Messages send from one node to another. A proper arrow would be more intuitive with regards to the direction -\* of message flow but SVG doesn't natively has arrows. This is why we use a lollipop instead where the ball -\* replaces the arrowhead. +\* MESSAGE VISUALIZATION +\* +\* Messages represent work being transferred between nodes. The animation +\* distinguishes between two types of message states: +\* 1. Arriving messages (solid lines): Messages being delivered in current step +\* 2. In-flight messages (dashed lines): Messages still in transit +\* +\* This distinction helps viewers understand the asynchronous nature of the +\* algorithm. A message sent in one step doesn't arrive until a later step. +\* +\* Visual encoding: +\* - Solid red line + dark arrow = message arriving now +\* - Dashed light red line + light arrow = message in-flight (will arrive later) +\* - Direction: arrow points from sender to receiver +\* - Arrow markers match their line colors for visual consistency +\* +\* Implementation notes: +\* - We compare inbox and inbox' (primed) to determine which messages are +\* arriving vs. remaining in-flight +\* - Two arrow markers (arrowSolid, arrowDashed) defined in DefsElement provide +\* direction indicators that match the line style +--------------------------------------------------------------------------- Messages == - LET M[ n \in Node ] == - LET pls == Range(SelectSeq(inbox[n], LAMBDA msg: msg.type = "pl")) + LET \* For each destination node, create message visualizations + M[ n \in Node ] == + LET \* Extract payload messages ("pl" type) from this node's inbox + pls == Range(SelectSeq(inbox[n], LAMBDA msg: msg.type = "pl")) + \* Extract payload messages in the NEXT state (primed) plsN == Range(SelectSeq(inbox'[n], LAMBDA msg: msg.type = "pl")) + \* For each message in the current inbox, create a visual line I[ pl \in pls ] == - LET from == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, node2nat[pl.src], N) + LET \* Get coordinates of sender and receiver nodes + from == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, node2nat[pl.src], N) to == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, node2nat[n], N) + \* Check if message persists in next state (in-flight) or is being delivered + isInFlight == pl \in plsN + \* Color and style based on message state + msgColor == IF isInFlight THEN Colors.messageInFlight ELSE Colors.message + dashArray == IF isInFlight THEN "6,4" ELSE "0" \* SVG dash pattern + \* Arrow marker selection: use lighter arrow for dashed lines + arrowMarker == IF isInFlight THEN "url(#arrowDashed)" ELSE "url(#arrowSolid)" + \* Message line with directional arrow (points from sender to receiver) line == Line(from.x + ArrowPosOffset, from.y + ArrowPosOffset, - to.x + ArrowPosOffset, to.y + ArrowPosOffset, - [stroke |-> "orange", stroke_dasharray |-> IF pl \in plsN THEN "5" ELSE "0", - marker_end |-> "url(#arrow)"]) \* See Defs below for the definition of arrow. - IN Group(<>, ("transform" :> "translate(0 125)")) + to.x + ArrowPosOffset, to.y + ArrowPosOffset, + [stroke |-> msgColor, + stroke_width |-> "2.5", + stroke_dasharray |-> dashArray, + opacity |-> IF isInFlight THEN "0.6" ELSE "0.9", + marker_end |-> arrowMarker]) \* Arrow shows message direction + IN Group(<>, ("transform" :> "translate(0 180)")) \* Vertical offset IN Group(I, <<>>) IN Group(M, <<>>) ---------------------------------------------------------------------------- -Animation == SVGElemToString(Group(<>, <<>>)) - -\* This is just the arrow head that's used by the Message definition above as an attribute. -Defs == - "" - -ToSVG == - IOExecTemplate( - <<"bash", "-c", "echo \"%1$s\" > EWD998_anim.svg">>, - <<"" - \o Defs - \o Animation' \* Note the prime here! - >>).exitValue = 0 - -Alias == [ - toolbox |-> Defs \o Animation, - eyeofgnome |-> "" \o Defs \o Animation \o "", - toSVG |-> - IOExecTemplate( - \* %%03d to escape %03d in Java format strings. - <<"bash", "-c", "echo \"%1$s\" > EWD998_anim_$(printf %%03d %2$s).svg">>, - <<"" - \o Defs - \o Animation - \o "", ToString(TLCGet("level"))>>) - ] - ---------------------------------------------------------------------------- - -AnimSpec == - \* AnimSpec constraints the set of initial states to a set of states, - \* s.t. all nodes are inactive but have sent or received a message. - \* The sum of all counters is zero. The token is at the Initiator. - \* The next-state relation does not permit environment (sub-) actions. - \* Replacing Spec with AnimSpec above, TLC can generate traces for large - \* numbers of nodes. - /\ active = [ n \in Node |-> FALSE ] - /\ color = [ n \in Node |-> "black" ] - /\ counter = [n \in Node |-> IF Cardinality(Node) % 2 = 0 - THEN IF node2nat[n] % 2 = 0 - THEN 1 - ELSE -1 - ELSE IF n # Initiator - THEN IF node2nat[n] % 2 = 0 - THEN 1 - ELSE -1 - ELSE 0 ] - /\ inbox = [n \in Node |-> IF n = Initiator \* RingOfNodes[Initiator] - THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> - ELSE <<>>] \* with empty channels. - /\ Init!5 - /\ [][\E n \in Node: System(n)]_vars - -\* Property that leads to interesting traces when animated. - -AnimInv == EWD998Chan!EWD998!terminationDetected => TLCGet("level") < 20 - -============================================================================= - -## Assuming the most recent Toolbox nightly build (https://nightly.tlapl.us/dist) -## installed to /opt/toolbox. On macOS, install gawk with `brew install gawk` -## (default nawk does not like the match). -/opt/toolbox/tla2tools.jar -simulate -noGenerateSpecTE -config EWD998_anim.tla EWD998_anim | gawk 'match($0,//) { n += 1; print substr($0,RSTART,RLENGTH) > sprintf("%03d", n) ".svg" }' && eog . +--------------------------------------------------------------------------- +\* ANIMATION COMPOSITION +\* +\* This section assembles all visual components into the final animation frame. +\* Components are layered in a specific order (z-order) to ensure proper +\* visual hierarchy. +--------------------------------------------------------------------------- +\* Background: White rectangle covering the entire viewBox +\* This ensures a clean, consistent background across all frames +Background == + Rect(-20, 0, 760, 420, + [fill |-> "#ffffff", stroke |-> "none"]) + +\* SVG Definitions Element: Creates SVG with reusable arrow markers +\* This must be included in the SVG document for message arrows to render. +\* Two arrow markers are defined, matching their respective line styles: +\* - arrowSolid: Dark red arrow for arriving messages +\* - arrowDashed: Light red arrow for in-flight messages +DefsElement == + SVGElem("defs", <<>>, << + \* Arrow marker for solid message lines (arriving now) + SVGElem("marker", + ("id" :> "arrowSolid" @@ + "markerWidth" :> "6" @@ \* Compact size for subtle direction indication + "markerHeight" :> "6" @@ + "refX" :> "5" @@ \* Reference point for line attachment + "refY" :> "2" @@ + "orient" :> "auto" @@ \* Auto-rotate to match line angle + "markerUnits" :> "strokeWidth" @@ + "viewBox" :> "0 0 10 10"), + < "M0,0 L0,6 L9,3 z" @@ "fill" :> Colors.message), <<>>, "")>>, + ""), + \* Arrow marker for dashed message lines (in-flight) + SVGElem("marker", + ("id" :> "arrowDashed" @@ + "markerWidth" :> "6" @@ \* Compact size for subtle direction indication + "markerHeight" :> "6" @@ + "refX" :> "5" @@ \* Reference point for line attachment + "refY" :> "2" @@ + "orient" :> "auto" @@ \* Auto-rotate to match line angle + "markerUnits" :> "strokeWidth" @@ + "viewBox" :> "0 0 10 10"), + < "M0,0 L0,6 L9,3 z" @@ "fill" :> Colors.messageInFlight), <<>>, "")>>, + "") + >>, "") + +\* AnimView: Main visual composition operator +\* +\* Best Practice (from Animation Guide): Create a single operator that composes +\* all visual elements. This provides a clean entry point for the animation. +\* +\* Layer ordering (bottom to top): +\* 0. DefsElement - SVG definitions (arrow markers, must be first) +\* 1. Background - white canvas +\* 2. Legend - title and key (always visible, explains symbols) +\* 3. StatusInfo - current algorithm state (running/terminated/detected) +\* 4. RingNetwork - the nodes in their ring formation +\* 5. TokenNetwork - the token (overlays the ring) +\* 6. Messages - message lines with arrows (drawn on top) +\* 7. StepNumber - step counter (topmost, bottom-right corner) +\* +\* This ordering ensures proper visual hierarchy and prevents elements from +\* obscuring each other inappropriately. +AnimView == + Group(<< + DefsElement, \* Layer 0: SVG definitions (arrow markers) + Background, \* Layer 1: White background + Legend, \* Layer 2: Title and legend + StatusInfo, \* Layer 3: Status indicator box + RingNetwork, \* Layer 4: Node ring + TokenNetwork, \* Layer 5: Token (on top of ring) + Messages, \* Layer 6: Message arrows (most prominent) + StepNumber \* Layer 7: Step counter (always visible) + >>, <<>>) -## The best viewer for a stack of SVGs is Gnome's Eye Of Gnome (eog) that -## is available for Win, macOS, and Linux. In its preferences, one can replace -## the transparent background with a custom color. One can also run a slideshow -## with a custom frame rate. +--------------------------------------------------------------------------- +\* ANIMATION WATCH EXPRESSION (for TLA+ Debugger) +\* +\* AnimWatch is designed for use as a Watch expression in the TLA+ Debugger. +\* When used with a live SVG viewer (e.g., https://open-vsx.org/extension/jock/svg), +\* the animation dynamically updates as you step through the debugger. +\* +\* Usage in Debugger: +\* When debugging EWD998ChanID.tla, use this watch expression: +\* +\* LET A == INSTANCE EWD998_anim IN A!AnimWatch +\* +\* (You must instantiate EWD998_anim in your watch expression, because +\* EWD998ChanID does not extend or instantiate EWD998_anim.) +\* +\* Frame parameter = 0: +\* - Each new frame REPLACES the previous SVG file on disk +\* - The SVG viewer automatically refreshes to show the current state +\* - Perfect for interactive debugging: see live updates as you step through +\* - Only one SVG file exists at a time (e.g., "EWD998_anim_watch_00.svg") +--------------------------------------------------------------------------- ----- +AnimWatch == + \* SVGSerialize writes one SVG file that updates with each state transition + SVGSerialize( + SVGDoc(AnimView, -20, 0, 760, 420, <<>>), \* Complete SVG document + "EWD998_anim_watch_", \* Filename prefix + 0) \* Frame 0 (overwrites each time) + +--------------------------------------------------------------------------- +\* ANIMATION ALIAS FOR TLC (for Screencast Generation) +\* +\* Best Practice (from Animation Guide): The AnimAlias operator is a TLC alias +\* that combines state variable inspection with animation generation. When you +\* add "ALIAS AnimAlias" to your .cfg file, TLC will automatically call this +\* operator at each state during exploration. +\* +\* Structure: +\* - Returns a record with state variables (active, color, counter, etc.) +\* merged with the special _anim field +\* - The _anim field contains the SVGSerialize call for animation generation +\* - This allows both visual animation AND state value inspection in TLC output +\* +\* How the animation works: +\* 1. AnimView is evaluated to create SVG elements based on current state +\* 2. SVGDoc wraps the elements in a complete SVG document structure +\* 3. SVGSerialize (from SVG module) writes the SVG to disk +\* 4. Files are named "EWD998_anim_.svg" where N is the state level +\* +\* Frame parameter = TLCGet("level"): +\* - Each state generates a UNIQUE SVG file on disk +\* - Creates a complete sequence: EWD998_anim_0.svg, EWD998_anim_1.svg, etc. +\* - Perfect for creating screencasts: combine frames into GIF, MOV, MP4, etc. +\* - All frames are preserved for post-processing and review +\* +\* ViewBox: -20, 0, 760, 420 +\* - Starts slightly left (-20) to accommodate background padding +\* - 760×420 dimensions fit all elements with appropriate margins +\* - Consistent viewBox across all frames (required for animation playback) +--------------------------------------------------------------------------- -## Unfortunately, the MacPorts package cannot be installed -## because of a broken dependency (https://trac.macports.org/ticket/61713). Instead, -## one can use the browser-based TLA+ trace Animator at https://animator.tlapl.us. -## In this case, a slightly different awk matching is needed. Optionally, pipe -## output of awk directly to xclip to send it to the clipboard ("| xclip"). +AnimAlias == + \* Record merge: state variables for debugging + _anim field for visualization + [active |-> active, color |-> color, counter |-> counter, + inbox |-> inbox, clock |-> clock, passes |-> passes] @@ + [_anim |-> SVGSerialize( + SVGDoc(AnimView, -20, 0, 760, 420, <<>>), \* Complete SVG document + "EWD998_anim_", \* Filename prefix + TLCGet("level"))] \* Unique frame number per state -/opt/toolbox/tla2tools.jar -simulate -noGenerateSpecTE -config EWD998_anim.tla EWD998_anim | gawk 'match($0,/toolbox = .*/) { print "[\ntb |->" substr($0, RSTART+9, RLENGTH) "\n]," }' +=============================================================================