Add SlidingPuzzles animation specification

specifications/SlidingPuzzles/SlidingPuzzles.tla

@@ -12,7 +12,13 @@ Klotski == {{<<0, 0>>, <<0, 1>>},
             {<<3, 0>>, <<3, 1>>},{<<0, 2>>, <<0, 3>>},
             {<<1, 2>>, <<2, 2>>},{<<3, 2>>, <<3, 3>>},
             {<<1, 3>>}, {<<2, 3>>}, {<<0, 4>>}, {<<3, 4>>}}
-
+
+(***************************************************************************)
+(* The optimal solution is 81 moves                                        *)
+(* (https://en.wikipedia.org/wiki/Klotski#Solving), counting each          *)
+(* multi-position slide as one move. TLC's trace will be longer since      *)
+(* each step in this spec moves a piece exactly one position.              *)
+(***************************************************************************)            
 KlotskiGoal == {<<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>} \notin board
 
 ChooseOne(S, P(_)) == CHOOSE x \in S : P(x) /\ \A y \in S : P(y) => y = x

specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg

@@ -0,0 +1,6 @@
+INIT Init
+NEXT Next
+INVARIANTS
+  TypeOK
+  KlotskiGoal
+ALIAS AnimAlias

specifications/SlidingPuzzles/SlidingPuzzles_anim.tla

@@ -0,0 +1,142 @@
+--------------------------- MODULE SlidingPuzzles_anim ---------------------------
+EXTENDS TLC, SVG, SequencesExt, SlidingPuzzles
+
+\* Layout constants
+CELL_SIZE == 60
+CELL_SPACING == 2
+BASE_X == 30
+BASE_Y == 50
+BOARD_WIDTH == W * (CELL_SIZE + CELL_SPACING)
+BOARD_HEIGHT == H * (CELL_SIZE + CELL_SPACING)
+
+\* Map piece directly to color based on size and orientation
+PieceColor(piece) ==
+    LET size == Cardinality(piece)
+        \* For 2-cell pieces: vertical means same x-coordinate, horizontal means same y-coordinate
+        isVertical == size = 2 /\ \A p1, p2 \in piece : p1[1] = p2[1]
+    IN CASE size = 0 -> "#ecf0f1"      \* Empty cells
+         [] size = 1 -> "#95a5a6"      \* Gray - single pieces
+         [] size = 2 /\ isVertical  -> "#3498db"  \* Blue - vertical 2x1
+         [] size = 2 /\ ~isVertical -> "#1abc9c"  \* Teal - horizontal 1x2
+         [] size = 4 -> "#e74c3c"      \* Red - 2x2 goal piece
+         [] OTHER -> "#cccccc"         \* Fallback
+
+\* Goal position (the 2x2 piece should reach bottom center)
+GoalPositions == {<<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>}
+
+\* Find which piece occupies a given position
+PieceAt(pos) ==
+    IF \E piece \in board : pos \in piece
+    THEN CHOOSE piece \in board : pos \in piece
+    ELSE {}  \* Empty
+
+\* Draw a single cell
+CellRect(x, y, w, h, piece) ==
+    LET fillColor == PieceColor(piece)
+        strokeColor == "#2c3e50"
+        strokeWidth == IF piece = {} THEN "1" ELSE "2"
+    IN Rect(x, y, w, h, 
+           ("fill" :> fillColor @@ 
+            "stroke" :> strokeColor @@ 
+            "stroke-width" :> strokeWidth @@ 
+            "rx" :> "3"))
+
+\* Draw the grid showing all positions
+GridCells ==
+    LET cellElems == {
+            LET pos == <<x, y>>
+                piece == PieceAt(pos)
+                cellX == BASE_X + x * (CELL_SIZE + CELL_SPACING)
+                cellY == BASE_Y + y * (CELL_SIZE + CELL_SPACING)
+            IN CellRect(cellX, cellY, CELL_SIZE, CELL_SIZE, piece)
+            : x \in 0..W-1, y \in 0..H-1
+        }
+    IN Group(SetToSeq(cellElems), <<>>)
+
+\* Draw goal position indicator (subtle border around goal area)
+GoalIndicator ==
+    LET minX == BASE_X + 1 * (CELL_SIZE + CELL_SPACING) - 4
+        minY == BASE_Y + 3 * (CELL_SIZE + CELL_SPACING) - 4
+        width == 2 * (CELL_SIZE + CELL_SPACING) + 4
+        height == 2 * (CELL_SIZE + CELL_SPACING) + 4
+    IN Rect(minX, minY, width, height,
+           ("fill" :> "none" @@ 
+            "stroke" :> "#f1c40f" @@ 
+            "stroke-width" :> "3" @@ 
+            "stroke-dasharray" :> "5,5" @@
+            "rx" :> "5"))
+
+\* Title
+Title == 
+    Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y - 25, "Klotski Puzzle", 
+         ("text-anchor" :> "middle" @@ 
+          "font-size" :> "20px" @@ 
+          "font-weight" :> "bold" @@ 
+          "fill" :> "#2c3e50"))
+
+\* Subtitle explaining goal
+Subtitle == 
+    Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y - 8, 
+         "Move red piece to dashed area", 
+         ("text-anchor" :> "middle" @@ 
+          "font-size" :> "11px" @@ 
+          "fill" :> "#7f8c8d"))
+
+\* Step counter - positioned below the board to avoid overlap
+StepCounter == 
+    Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y + BOARD_HEIGHT + 20, 
+         "Step " \o ToString(TLCGet("level")), 
+         ("text-anchor" :> "middle" @@ 
+          "font-size" :> "12px" @@ 
+          "font-family" :> "monospace" @@ 
+          "fill" :> "#95a5a6"))
+
+\* Success indicator (shows when puzzle is solved)
+SuccessIndicator ==
+    LET solved == ~KlotskiGoal  \* Puzzle is solved when KlotskiGoal invariant is violated
+        checkX == BASE_X + BOARD_WIDTH + 30
+        checkY == BASE_Y + 20
+    IN Group(<<
+        SVGElem("circle",
+               ("cx" :> ToString(checkX) @@ 
+                "cy" :> ToString(checkY) @@ 
+                "r" :> "15" @@ 
+                "fill" :> "#2ecc71" @@ 
+                "stroke" :> "#27ae60" @@ 
+                "stroke-width" :> "2"),
+               <<>>,
+               ""),
+        SVGElem("path",
+               ("d" :> "M " \o ToString(checkX - 6) \o " " \o ToString(checkY) \o 
+                       " L " \o ToString(checkX - 2) \o " " \o ToString(checkY + 5) \o 
+                       " L " \o ToString(checkX + 7) \o " " \o ToString(checkY - 5) @@
+                "stroke" :> "white" @@
+                "stroke-width" :> "3" @@
+                "fill" :> "none" @@
+                "stroke-linecap" :> "round" @@
+                "stroke-linejoin" :> "round"),
+               <<>>,
+               "")
+    >>, IF solved THEN <<>> ELSE ("opacity" :> "0"))
+
+\* Main animation view combining all elements
+AnimView == 
+    Group(<<Title, Subtitle, GoalIndicator, GridCells, 
+            StepCounter, SuccessIndicator>>, <<>>)
+
+\* Wrap view in SVG document
+AnimDoc == SVGDoc(AnimView, 0, 0, 
+                  BASE_X + BOARD_WIDTH + 60, 
+                  BASE_Y + BOARD_HEIGHT + 40, 
+                  <<>>)
+
+\* For TLC model checking (generates numbered frames for screencasts)
+AnimAlias ==
+    [board |-> board] @@
+    [_anim |-> SVGSerialize(AnimDoc, "SlidingPuzzles_anim_", TLCGet("level"))]
+
+\* For interactive debugging (live preview in debugger)
+AnimWatch ==
+    SVGSerialize(AnimDoc, "SlidingPuzzles_anim", 0)
+
+=============================================================================

specifications/SlidingPuzzles/manifest.json

@@ -16,6 +16,18 @@
           "result": "safety failure"
         }
       ]
+    },
+    {
+      "path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.tla",
+      "features": [ ],
+      "models": [
+        {
+          "path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg",
+          "runtime": "00:00:10",
+          "mode": "exhaustive search",
+          "result": "safety failure"
+        }
+      ]
     }
   ]
 }