Overhaul Tower of Hanoi specification

[lemmy]

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

[Alexander-N]

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?

[lemmy]

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.

[Alexander-N]

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?

[lemmy]

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.