From 160494b94dc3a90ce23d99f1ddc5697fe1c68694 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 12 Jan 2026 10:31:58 -0800 Subject: [PATCH] Add Tower of Hanoi animation Added SVG animation visualization for the Tower of Hanoi puzzle, displaying colored disk stacks and move-by-move progression toward the goal state with a SOLVED indicator upon completion. Co-authored-by: Claude Sonnet 4.5 Signed-off-by: Markus Alexander Kuppe --- specifications/tower_of_hanoi/Hanoi_anim.cfg | 18 +++ specifications/tower_of_hanoi/Hanoi_anim.tla | 124 +++++++++++++++++++ specifications/tower_of_hanoi/manifest.json | 12 ++ 3 files changed, 154 insertions(+) create mode 100644 specifications/tower_of_hanoi/Hanoi_anim.cfg create mode 100644 specifications/tower_of_hanoi/Hanoi_anim.tla diff --git a/specifications/tower_of_hanoi/Hanoi_anim.cfg b/specifications/tower_of_hanoi/Hanoi_anim.cfg new file mode 100644 index 00000000..de251154 --- /dev/null +++ b/specifications/tower_of_hanoi/Hanoi_anim.cfg @@ -0,0 +1,18 @@ +\* TLC Configuration for Tower of Hanoi with Animation +\* This configuration generates SVG animation frames showing the solution. + +\* Number of disks +CONSTANT D = 3 + +\* Number of towers +CONSTANT N = 3 + +\* Initial state and next-state relation +INIT Init +NEXT Next + +\* Generate animation frames (requires Hanoi_anim.tla) +ALIAS AnimAlias + +\* Find solution by checking NotSolved +INVARIANT NotSolved diff --git a/specifications/tower_of_hanoi/Hanoi_anim.tla b/specifications/tower_of_hanoi/Hanoi_anim.tla new file mode 100644 index 00000000..57439861 --- /dev/null +++ b/specifications/tower_of_hanoi/Hanoi_anim.tla @@ -0,0 +1,124 @@ +---- MODULE Hanoi_anim ---- +EXTENDS TLC, SVG, Sequences, Hanoi + +\* Layout constants +TowerSpacing == 120 +TowerBaseY == 200 +TowerHeight == 150 +DiskHeight == 15 +BaseX == 60 + +\* Helper to decode which disks are on a tower (from bitwise representation) +\* Returns a sequence of disk sizes (powers of 2) in bottom-to-top order +DisksOnTower(towerValue) == + LET RECURSIVE FindDisks(_,_) + FindDisks(value, maxDisk) == + IF maxDisk = 0 THEN <<>> + ELSE IF value >= maxDisk + THEN <> \o FindDisks(value - maxDisk, maxDisk \div 2) + ELSE FindDisks(value, maxDisk \div 2) + IN FindDisks(towerValue, 2^(D-1)) + +\* Color for each disk based on size +DiskColor(diskSize) == + CASE diskSize = 1 -> "#e57373" \* Red for smallest + [] diskSize = 2 -> "#81c784" \* Green + [] diskSize = 4 -> "#64b5f6" \* Blue + [] diskSize = 8 -> "#ffd54f" \* Yellow + [] diskSize = 16 -> "#ba68c8" \* Purple + [] diskSize = 32 -> "#4db6ac" \* Teal + [] diskSize = 64 -> "#ff8a65" \* Orange + [] OTHER -> "#90a4ae" \* Gray for larger + +\* Disk width based on size (log2 of size gives us the disk number) +DiskWidth(diskSize) == + LET RECURSIVE Log2(_) + Log2(n) == IF n <= 1 THEN 0 ELSE 1 + Log2(n \div 2) + diskNum == Log2(diskSize) + 1 + IN 20 + diskNum * 15 + +\* Draw a single disk at position +DrawDisk(x, y, diskSize) == + LET width == DiskWidth(diskSize) + IN Rect(x - width \div 2, y, width, DiskHeight - 2, + ("fill" :> DiskColor(diskSize) @@ + "stroke" :> "#333" @@ + "stroke-width" :> "1" @@ + "rx" :> "3")) + +\* Draw all disks on a tower +DrawDisksOnTower(towerIdx) == + LET x == BaseX + (towerIdx - 1) * TowerSpacing + disks == DisksOnTower(towers[towerIdx]) + diskElements == [i \in 1..Len(disks) |-> + DrawDisk(x, TowerBaseY - i * DiskHeight, disks[i])] + IN Group(diskElements, <<>>) + +\* Draw tower pole +DrawTowerPole(towerIdx) == + LET x == BaseX + (towerIdx - 1) * TowerSpacing + IN Group(<< + \* Pole + Rect(x - 3, TowerBaseY - TowerHeight, 6, TowerHeight, + ("fill" :> "#795548" @@ "stroke" :> "#333")), + \* Base + Rect(x - 40, TowerBaseY, 80, 8, + ("fill" :> "#5d4037" @@ "stroke" :> "#333" @@ "rx" :> "2")), + \* Tower label + Text(x, TowerBaseY + 25, "Tower " \o ToString(towerIdx), + ("text-anchor" :> "middle" @@ + "font-size" :> "12px" @@ + "fill" :> "#666")) + >>, <<>>) + +\* Success indicator +SuccessIndicator == + IF towers[N] = 2^D - 1 THEN + Group(<< + Rect(10, 10, 340, 30, + ("fill" :> "#4caf50" @@ + "stroke" :> "#2e7d32" @@ + "rx" :> "5")), + Text(180, 30, "SOLVED!", + ("text-anchor" :> "middle" @@ + "font-size" :> "18px" @@ + "font-weight" :> "bold" @@ + "fill" :> "white")) + >>, <<>>) + ELSE + Group(<<>>, <<>>) + +\* Title +Title == Text(180, 15, "Tower of Hanoi - " \o ToString(D) \o " disks", + ("text-anchor" :> "middle" @@ + "font-size" :> "14px" @@ + "font-weight" :> "bold" @@ + "fill" :> "#333")) + +\* Step number +StepNumber == + Text(350, 240, "Step " \o ToString(TLCGet("level")), + ("text-anchor" :> "end" @@ + "font-size" :> "12px" @@ + "font-family" :> "monospace" @@ + "fill" :> "#666")) + +\* Main animation view +AnimView == + Group(<> \o + [i \in 1..N |-> DrawTowerPole(i)] \o + [i \in 1..N |-> DrawDisksOnTower(i)], + <<>>) + +\* Wrap view in SVG document +AnimDoc == SVGDoc(AnimView, 0, 0, 360, 250, <<>>) + +\* For TLC model checking (generates numbered frames) +AnimAlias == + [towers |-> towers] @@ + [_anim |-> SVGSerialize(AnimDoc, "Hanoi_anim_", TLCGet("level"))] + +\* For interactive debugging (live preview) +AnimWatch == + SVGSerialize(AnimDoc, "Hanoi_anim", 0) +==== diff --git a/specifications/tower_of_hanoi/manifest.json b/specifications/tower_of_hanoi/manifest.json index 830d9bfd..67527435 100644 --- a/specifications/tower_of_hanoi/manifest.json +++ b/specifications/tower_of_hanoi/manifest.json @@ -44,6 +44,18 @@ "path": "specifications/tower_of_hanoi/HanoiSeq.tla", "features": [], "models": [] + }, + { + "path": "specifications/tower_of_hanoi/Hanoi_anim.tla", + "features": [], + "models": [ + { + "path": "specifications/tower_of_hanoi/Hanoi_anim.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "safety failure" + } + ] } ] } \ No newline at end of file