tlaplus
Overhaul Tower of Hanoi specification
- Modeling towers as Naturals in Hanoi.tla is rather low-level/close to an implementation. A high-level spec is likely simpler to grasp if it models towers as sequences...
- Current Hanoi.tla refinement for high-level spec?!
- ~Add comments to Bits And operator and explain what it is doing~ Moved to CommunityModules](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla)
- Existing comments limited to TLC module overwrite
- State Hanoi problem at the beginning of Hanoi.tla in case the file is passed around without README.md
-
TypeOK not a type invariant because it omits that tower is a function
- Comment states that a tower is a number in 1..2^D, while the formula says it's a number in 0..(2^D-1)
(see personal email "RE: Github examples" dated 07/17/19 from LL)
And more explicit variant of how to specify logical and. It is broken when Len(by) # Len(bx)
LOCAL INSTANCE Sequences
LOCAL Max(n, m) == IF n < m THEN m ELSE n
RECURSIVE ToBase2(_, _)
ToBase2(d, b) == IF d > 0
THEN ToBase2(d \div 2, b) \o <<d % 2>>
ELSE b
ToBase10(b) == LET d[i \in DOMAIN b] == IF i = 1
THEN b[Len(b) + 1 - i] * (2^(i-1))
ELSE b[Len(b) + 1 - i] * (2^(i-1)) + d[i - 1]
IN d[Len(b)]
LOCAL And2(x,y) == LET bx == ToBase2(x, <<>>)
by == ToBase2(y, <<>>)
and == [ i \in DOMAIN bx \cup DOMAIN by |->
IF bx[i] = 1 /\ by[i] = 1 THEN 1 ELSE 0 ]
IN ToBase10(and)
I tried to model this as an exercise, maybe this is along the lines of what you had in mind and can be used as example?
------------------------------- MODULE hanoi -------------------------------
EXTENDS TLC, Sequences, Integers
CONSTANTS A, B, C
VARIABLES towers
ASSUME A \in [1..Len(A) -> Nat]
ASSUME B \in [1..Len(B) -> Nat]
ASSUME C \in [1..Len(C) -> Nat]
CanMove(from, to) ==
/\ from /= to
/\ towers[from] /= <<>>
/\ IF
towers[to] = <<>>
THEN
TRUE
ELSE
Head(towers[to]) > Head(towers[from])
Move(from, to) ==
towers' = [
towers EXCEPT
![from] = Tail(towers[from]),
![to] = <<Head(towers[from])>> \o towers[to]
]
Init ==
towers = <<A, B, C>>
Next ==
\E from, to \in 1..Len(towers):
/\ CanMove(from, to)
/\ Move(from, to)
-------------------------------------
Range(sequence) ==
{sequence[i]: i \in DOMAIN sequence}
TypeOK ==
/\ DOMAIN towers = 1..3
/\ \A sequence \in Range(towers):
sequence \in [1..Len(sequence) -> Nat]
NoNewElements ==
LET
originalElements ==
UNION {Range(A), Range(B), Range(C)}
towerElements ==
UNION {Range(towers[1]), Range(towers[2]), Range(towers[3])}
IN
towerElements = originalElements
TotalConstant ==
LET
originalTotal ==
Len(A) + Len(B) + Len(C)
towerTotal==
Len(towers[1]) + Len(towers[2]) + Len(towers[3])
IN
towerTotal = originalTotal
SolutionNotFound ==
~(
/\ towers[1] = <<>>
/\ towers[2] = <<>>
/\ towers[3] = [i \in 1..Len(towers[3]) |-> i]
)
=============================================================================
I think this is a nice problem to get started with TLA+. Maybe the current example could be separated and explicitly marked as example of how to do module overwrites?
Do you want to open a PR?
Btw. the existing variant of Hanoi is not just about module overrides but also shows how towers can be modeled as natural numbers. In other words, it is a space-optimized refinement of the variant with sequences.
Do you want to open a PR?
Sure, I can do that. Would it be ok to just add it as separate example and leave the current variant untouched?
I suggest creating HanoiSeq.tla in the existing towers_of_hanoi folder to leave the door open to adding a refinement mapping later. Please add comments to your spec and state the Hanoi problem in the README or before the module header in HanoiSeq.tla.