Last active
May 31, 2022 23:46
-
-
Save ocadaruma/ced8c0ff1b89b70964ad510e8637419e to your computer and use it in GitHub Desktop.
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
| INIT Init | |
| NEXT Next | |
| INVARIANT NotSolved |
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
| ---- MODULE hanoi ---- | |
| EXTENDS Integers, Sequences | |
| VARIABLES rods | |
| Last(seq) == | |
| seq[Len(seq)] | |
| Init == | |
| rods = << | |
| <<3,2,1>>, <<>>, <<>> | |
| >> | |
| MoveDisk(from, to) == | |
| /\ Len(rods[from]) > 0 | |
| /\ Len(rods[to]) > 0 => Last(rods[from]) < Last(rods[to]) | |
| /\ rods' = [rods EXCEPT![from] = SubSeq(@, 1, Len(@) - 1), | |
| ![to] = Append(@, Last(rods[from]))] | |
| Next == | |
| \E i, j \in DOMAIN rods: i /= j /\ MoveDisk(i, j) | |
| NotSolved == | |
| rods /= << | |
| <<>>, <<>>, <<3, 2, 1>> | |
| >> | |
| ==== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment