Overhaul Tower of Hanoi specification about examples

[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.

[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?