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 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