Add SlidingPuzzles animation specification #195
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Member
lemmy
commented
Jan 13, 2026
lemmy
commented
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 <github.com@lemmster.de>
lemmy
force-pushed
the
mku-anims
branch
3 times, most recently
from
d1b395e to
518fb56
Compare
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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.