Skip to content

Commit c7dc34e

Browse files
lemmyClaude Sonnet 4.5
lemmy
and
Claude Sonnet 4.5
committed
Add SlidingPuzzles animation specification
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 <sonnet@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 30efe07 commit c7dc34e

File tree

3 files changed

+160
-0
lines changed

3 files changed

+160
-0
lines changed

‎specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
INIT Init
2+
NEXT Next
3+
INVARIANTS
4+
TypeOK
5+
KlotskiGoal
6+
ALIAS AnimAlias

‎specifications/SlidingPuzzles/SlidingPuzzles_anim.tla‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
--------------------------- MODULE SlidingPuzzles_anim ---------------------------
2+
EXTENDS TLC, SVG, SequencesExt, SlidingPuzzles
3+
4+
\* Layout constants
5+
CELL_SIZE == 60
6+
CELL_SPACING == 2
7+
BASE_X == 30
8+
BASE_Y == 50
9+
BOARD_WIDTH == W * (CELL_SIZE + CELL_SPACING)
10+
BOARD_HEIGHT == H * (CELL_SIZE + CELL_SPACING)
11+
12+
\* Map piece directly to color based on size and orientation
13+
PieceColor(piece) ==
14+
LET size == Cardinality(piece)
15+
\* For 2-cell pieces: vertical means same x-coordinate, horizontal means same y-coordinate
16+
isVertical == size = 2 /\ \A p1, p2 \in piece : p1[1] = p2[1]
17+
IN CASE size = 0 -> "#ecf0f1" \* Empty cells
18+
[] size = 1 -> "#95a5a6" \* Gray - single pieces
19+
[] size = 2 /\ isVertical -> "#3498db" \* Blue - vertical 2x1
20+
[] size = 2 /\ ~isVertical -> "#1abc9c" \* Teal - horizontal 1x2
21+
[] size = 4 -> "#e74c3c" \* Red - 2x2 goal piece
22+
[] OTHER -> "#cccccc" \* Fallback
23+
24+
\* Goal position (the 2x2 piece should reach bottom center)
25+
GoalPositions == {<<1, 3>>, <<1, 4>>, <<2, 3>>, <<2, 4>>}
26+
27+
\* Find which piece occupies a given position
28+
PieceAt(pos) ==
29+
IF \E piece \in board : pos \in piece
30+
THEN CHOOSE piece \in board : pos \in piece
31+
ELSE {} \* Empty
32+
33+
\* Draw a single cell
34+
CellRect(x, y, w, h, piece) ==
35+
LET fillColor == PieceColor(piece)
36+
strokeColor == "#2c3e50"
37+
strokeWidth == IF piece = {} THEN "1" ELSE "2"
38+
IN Rect(x, y, w, h,
39+
("fill" :> fillColor @@
40+
"stroke" :> strokeColor @@
41+
"stroke-width" :> strokeWidth @@
42+
"rx" :> "3"))
43+
44+
\* Draw the grid showing all positions
45+
GridCells ==
46+
LET cellElems == {
47+
LET pos == <<x, y>>
48+
piece == PieceAt(pos)
49+
cellX == BASE_X + x * (CELL_SIZE + CELL_SPACING)
50+
cellY == BASE_Y + y * (CELL_SIZE + CELL_SPACING)
51+
IN CellRect(cellX, cellY, CELL_SIZE, CELL_SIZE, piece)
52+
: x \in 0..W-1, y \in 0..H-1
53+
}
54+
IN Group(SetToSeq(cellElems), <<>>)
55+
56+
\* Draw goal position indicator (subtle border around goal area)
57+
GoalIndicator ==
58+
LET minX == BASE_X + 1 * (CELL_SIZE + CELL_SPACING) - 4
59+
minY == BASE_Y + 3 * (CELL_SIZE + CELL_SPACING) - 4
60+
width == 2 * (CELL_SIZE + CELL_SPACING) + 4
61+
height == 2 * (CELL_SIZE + CELL_SPACING) + 4
62+
IN Rect(minX, minY, width, height,
63+
("fill" :> "none" @@
64+
"stroke" :> "#f1c40f" @@
65+
"stroke-width" :> "3" @@
66+
"stroke-dasharray" :> "5,5" @@
67+
"rx" :> "5"))
68+
69+
\* Title
70+
Title ==
71+
Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y - 25, "Klotski Puzzle",
72+
("text-anchor" :> "middle" @@
73+
"font-size" :> "20px" @@
74+
"font-weight" :> "bold" @@
75+
"fill" :> "#2c3e50"))
76+
77+
\* Subtitle explaining goal
78+
Subtitle ==
79+
Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y - 8,
80+
"Move red piece to dashed area",
81+
("text-anchor" :> "middle" @@
82+
"font-size" :> "11px" @@
83+
"fill" :> "#7f8c8d"))
84+
85+
\* Step counter - positioned below the board to avoid overlap
86+
StepCounter ==
87+
Text(BASE_X + BOARD_WIDTH \div 2, BASE_Y + BOARD_HEIGHT + 20,
88+
"Step " \o ToString(TLCGet("level")),
89+
("text-anchor" :> "middle" @@
90+
"font-size" :> "12px" @@
91+
"font-family" :> "monospace" @@
92+
"fill" :> "#95a5a6"))
93+
94+
\* Success indicator (shows when puzzle is solved)
95+
SuccessIndicator ==
96+
LET solved == ~KlotskiGoal \* Puzzle is solved when KlotskiGoal invariant is violated
97+
checkX == BASE_X + BOARD_WIDTH + 30
98+
checkY == BASE_Y + 20
99+
IN Group(<<
100+
SVGElem("circle",
101+
("cx" :> ToString(checkX) @@
102+
"cy" :> ToString(checkY) @@
103+
"r" :> "15" @@
104+
"fill" :> "#2ecc71" @@
105+
"stroke" :> "#27ae60" @@
106+
"stroke-width" :> "2"),
107+
<<>>,
108+
""),
109+
SVGElem("path",
110+
("d" :> "M " \o ToString(checkX - 6) \o " " \o ToString(checkY) \o
111+
" L " \o ToString(checkX - 2) \o " " \o ToString(checkY + 5) \o
112+
" L " \o ToString(checkX + 7) \o " " \o ToString(checkY - 5) @@
113+
"stroke" :> "white" @@
114+
"stroke-width" :> "3" @@
115+
"fill" :> "none" @@
116+
"stroke-linecap" :> "round" @@
117+
"stroke-linejoin" :> "round"),
118+
<<>>,
119+
"")
120+
>>, IF solved THEN <<>> ELSE ("opacity" :> "0"))
121+
122+
\* Main animation view combining all elements
123+
AnimView ==
124+
Group(<<Title, Subtitle, GoalIndicator, GridCells,
125+
StepCounter, SuccessIndicator>>, <<>>)
126+
127+
\* Wrap view in SVG document
128+
AnimDoc == SVGDoc(AnimView, 0, 0,
129+
BASE_X + BOARD_WIDTH + 60,
130+
BASE_Y + BOARD_HEIGHT + 40,
131+
<<>>)
132+
133+
\* For TLC model checking (generates numbered frames for screencasts)
134+
AnimAlias ==
135+
[board |-> board] @@
136+
[_anim |-> SVGSerialize(AnimDoc, "SlidingPuzzles_anim_", TLCGet("level"))]
137+
138+
\* For interactive debugging (live preview in debugger)
139+
AnimWatch ==
140+
SVGSerialize(AnimDoc, "SlidingPuzzles_anim", 0)
141+
142+
=============================================================================

‎specifications/SlidingPuzzles/manifest.json‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,18 @@
1616
"result": "safety failure"
1717
}
1818
]
19+
},
20+
{
21+
"path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.tla",
22+
"features": [ ],
23+
"models": [
24+
{
25+
"path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg",
26+
"runtime": "00:00:10",
27+
"mode": "exhaustive search",
28+
"result": "safety failure"
29+
}
30+
]
1931
}
2032
]
2133
}

0 commit comments

Comments
 (0)