From fc162eddc91a47371df21ab0428a0330abf03399 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 13 Jan 2026 07:19:20 -0800 Subject: [PATCH 1/2] Add optimal solution commentary for Klotski puzzle Included a detailed comment in the SlidingPuzzles.tla file outlining the optimal solution of 81 moves for the Klotski puzzle, referencing the multi-position slide counting method and noting that TLC's trace will be longer due to individual piece movements. Signed-off-by: Markus Alexander Kuppe --- specifications/SlidingPuzzles/SlidingPuzzles.tla | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/specifications/SlidingPuzzles/SlidingPuzzles.tla b/specifications/SlidingPuzzles/SlidingPuzzles.tla index 82b89599..a141d27c 100644 --- a/specifications/SlidingPuzzles/SlidingPuzzles.tla +++ b/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 From 08122251ad3f1674e651fc32c7b254dc157f2e20 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 13 Jan 2026 09:56:36 -0800 Subject: [PATCH 2/2] Add SlidingPuzzles animation specification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduced new configuration and TLA+ files for the SlidingPuzzles animation, defining layout constants, piece color mapping, goal positions, and rendering logic for the puzzle grid and indicators. This addition enhances the visual representation of the Klotski puzzle and supports interactive debugging. Note: The AI required substantial guidance because the specification is too high-level to assign a stable, unique identity to each board piece. As a result, coloring individual pieces is unreliable: pieces may appear to change or swap colors during the animation. Unless the original specification is extended to preserve a unique identity for each piece, the only viable way to establish identity is by tracking each piece through its sequence of moves. In TLA+, this would necessarily require introducing a history variable. After switching to a color scheme based on piece type (1×1, 2×1, 1×2, 2×2), the AI still failed to identify the straightforward mapping—based on cardinality and orientation—needed to distinguish these types. Co-authored-by: Claude Sonnet 4.5 Signed-off-by: Markus Alexander Kuppe --- .../SlidingPuzzles/SlidingPuzzles_anim.cfg | 6 + .../SlidingPuzzles/SlidingPuzzles_anim.tla | 142 ++++++++++++++++++ specifications/SlidingPuzzles/manifest.json | 12 ++ 3 files changed, 160 insertions(+) create mode 100644 specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg create mode 100644 specifications/SlidingPuzzles/SlidingPuzzles_anim.tla diff --git a/specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg b/specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg new file mode 100644 index 00000000..b19c8301 --- /dev/null +++ b/specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg @@ -0,0 +1,6 @@ +INIT Init +NEXT Next +INVARIANTS + TypeOK + KlotskiGoal +ALIAS AnimAlias diff --git a/specifications/SlidingPuzzles/SlidingPuzzles_anim.tla b/specifications/SlidingPuzzles/SlidingPuzzles_anim.tla new file mode 100644 index 00000000..11da8647 --- /dev/null +++ b/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 == <> + 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(<>, <<>>) + +\* 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) + +============================================================================= diff --git a/specifications/SlidingPuzzles/manifest.json b/specifications/SlidingPuzzles/manifest.json index 9455769e..13c7d3ef 100644 --- a/specifications/SlidingPuzzles/manifest.json +++ b/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" + } + ] } ] } \ No newline at end of file