Towers of Hanoi and a question about Invariants

(3 posts) (2 voices)

Tags

No tags yet.

  1. kbanks
    Member

    Created an example for the "Towers of Hanoi" logic puzzle, but ran out of time before I could add any error checking using invariants.

    Anybody got a good suggestion for what I should have verified in

    (*
TypeInvariant == /\ peg1 ???
                 /\ peg2 ???
                 /\ peg3 ???
*)

    Hanoi.tla

    ------------------------------ MODULE Hanoi ---------------------------------
(***************************************************************************)
(* "Towers of Hanoi" puzzle solved using TLA+ 12/12/2010-12/13/2010        *)
(* Transfer a stack of disks from one peg to another, with the constraint  *)
(* that a larger disk can never be placed on a smaller disk. A third peg   *)
(* makes the puzzle possible.                                              *)
(***************************************************************************)

(***************************************************************************)
(* Since we care about the SIZE of the disks we represent them as integers *)
(* We will represent each peg as a sequence of those disks, with the Head  *)
(* of each Sequence representing the TOP of that stack of disks.           *)
(***************************************************************************)
EXTENDS Integers, Sequences
CONSTANTS NumberOfDisks
VARIABLE peg1, peg2, peg3

-----------------------------------------------------------------------------

\* I never did find a way to specify the initial tuple in the .cfg file...
Disks == [i \in 1..NumberOfDisks |-> i]

Init == /\ peg1 = Disks
        /\ peg2 = <<>>
        /\ peg3 = <<>>

(*
TypeInvariant == /\ peg1 ???
                 /\ peg2 ???
                 /\ peg3 ???
*)

(***************************************************************************)
(* Helper function, needed because the destination peg might be empty      *)
(* (You cannot take the Head() of an empty Sequence!)                      *)
(* What we do in the "empty peg" case is return a number bigger than ANY   *)
(* disk.                                                                   *)
(***************************************************************************)
Top(peg) == IF peg = <<>> THEN NumberOfDisks+1 ELSE Head(peg)

(***************************************************************************)
(* A legal move in Hanoi, genericized in terms of src peg, dest peg, and   *)
(* the spare peg                                                           *)
(***************************************************************************)
MoveDisk(src, dest, spare) == /\ src # <<>>
                              /\ Head(src) < Top(dest)
                              /\ src' = Tail(src)
                              /\ dest' = SubSeq(src,1,1) \o dest
                              /\ UNCHANGED <<spare>>

(***************************************************************************)
(* The legal moves in Hanoi, specified in terms of MoveDisk.               *)
(***************************************************************************)

MoveTopDiskFromPeg1ToPeg2 == MoveDisk(peg1, peg2, peg3)

MoveTopDiskFromPeg1ToPeg3 == MoveDisk(peg1, peg3, peg2)

MoveTopDiskFromPeg2ToPeg1 == MoveDisk(peg2, peg1, peg3)

MoveTopDiskFromPeg2ToPeg3 == MoveDisk(peg2, peg3, peg1)

MoveTopDiskFromPeg3ToPeg1 == MoveDisk(peg3, peg1, peg2)

MoveTopDiskFromPeg3ToPeg2 == MoveDisk(peg3, peg2, peg1)

Next == \/ MoveTopDiskFromPeg1ToPeg2
        \/ MoveTopDiskFromPeg1ToPeg3
        \/ MoveTopDiskFromPeg2ToPeg1
        \/ MoveTopDiskFromPeg2ToPeg3
        \/ MoveTopDiskFromPeg3ToPeg1
        \/ MoveTopDiskFromPeg3ToPeg2

Spec == Init /\ [][Next]_<<peg1, peg2, peg3>>
-----------------------------------------------------------------------------

Solved == /\ peg1 = <<>>
          /\ peg2 = <<>>
          /\ peg3 = Disks

NotSolved == ~Solved
=============================================================================

    Hanoi.cfg

    CONSTANTS
  NumberOfDisks = 3

SPECIFICATION Spec
\*INVARIANTS TypeInvariant NotSolved
INVARIANTS NotSolved
    Posted 1 year ago #

  2. merz
    Member

    A suitable type invariant is

    /\ peq1 \in Seq(1 .. NumberOfDisks)
    /\ peg2 \in Seq(1 .. NumberOfDisks)
    /\ peg3 \in Seq(1 .. NumberOfDisks)

    Also, I tried running your example from the TLA+ toolbox, and TLC found a solution (for NumberOfDisks = 3) in no time. Also, it verifies the type invariant very quickly (the state space quite obviously consists of 27 distinct states).

    Here's a variant of your specification using arrays, which leads to a more concise model.


    ------------------------------ MODULE Hanoi ---------------------------------
    (***************************************************************************)
    (* "Towers of Hanoi" puzzle solved using TLA+ 12/12/2010-12/13/2010 *)
    (* Transfer a stack of disks from one peg to another, with the constraint *)
    (* that a larger disk can never be placed on a smaller disk. A third peg *)
    (* makes the puzzle possible. *)
    (***************************************************************************)

    (***************************************************************************)
    (* Since we care about the SIZE of the disks we represent them as integers *)
    (* We will represent each peg as a sequence of those disks, with the Head *)
    (* of each Sequence representing the TOP of that stack of disks. *)
    (***************************************************************************)
    EXTENDS Integers, Sequences, TLC
    CONSTANTS NumberOfDisks
    VARIABLE pegs

    -----------------------------------------------------------------------------

    Pegs == 1 .. 3
    Disks == 1 .. NumberOfDisks
    AllDisks == [i \in Disks |-> i]

    Init == pegs = (1 :> AllDisks) @@ (2 :> <<>>) @@ (3 :> <<>>)

    TypeInvariant == pegs \in [ Pegs -> Seq(Disks) ]

    (***************************************************************************)
    (* Helper function, needed because the destination peg might be empty *)
    (* (You cannot take the Head() of an empty Sequence!) *)
    (* What we do in the "empty peg" case is return a number bigger than ANY *)
    (* disk. *)
    (***************************************************************************)
    Top(peg) == IF peg = <<>> THEN NumberOfDisks+1 ELSE Head(peg)

    (***************************************************************************)
    (* Move the top disk from peg src to peg dst. *)
    (***************************************************************************)
    MoveDisk(src, dst) == /\ pegs[src] # <<>>
    /\ Top(pegs[src]) < Top(pegs[dst])
    /\ pegs' = [pegs EXCEPT ![src] = Tail(@),
    ![dst] = <<Top(pegs[src])>> \o @]

    (***************************************************************************)
    (* The legal moves in Hanoi, specified in terms of MoveDisk. *)
    (***************************************************************************)

    Next == \E src,dst \in Pegs : src # dst /\ MoveDisk(src,dst)

    Spec == Init /\ [][Next]_pegs
    -----------------------------------------------------------------------------

    Solved == pegs = (1 :> <<>>) @@ (2 :> <<>>) @@ (3 :> AllDisks)

    NotSolved == ~Solved

    =============================================================================

    Posted 1 year ago #

  3. kbanks
    Member

    Thanks for the example!

    Posted 11 months ago #

RSS feed for this topic

Reply

You must log in to post.