(second attempt at this post - failed the captcha the first time (?))
Fellow beginners may find this example useful. I took what I learned from the "DieHard" example and wrote a TLA+ spec to solve the "Missionaries and Cannibals" puzzle.
Config file Cannibal.cfg
SPECIFICATION Spec
INVARIANTS TypeOK NotSolvedSpec file Cannibal.tla
------------------------------ MODULE Cannibal -----------------------------
(***************************************************************************)
(* The Missionaries and Cannibals Problem solved using TLA+ *)
(* Everybody starts on the lhs of the river *)
(* The goal is to get everybody safely across the river *)
(* The boat can only carry 1 or 2 (never none) *)
(* If the cannibals ever outnumber the missionaries, they will eat them! *)
(* NOTE-there CAN legally be more cannibals than missionaries on the same *)
(* side of the river when the number of missionaries = 0 *)
(* Worked on this 12/07/2010-12/08/2010 *)
(***************************************************************************)
EXTENDS Naturals
VARIABLES cl, \* The number of cannibals on the lhs of the river.
ml, \* The number of missionaries on the lhs of the river.
cr, \* The number of cannibals on the rhs of the river.
mr, \* The number of missionaries on the rhs of the river.
boat \* 0 when boat is on the lhs, 1 when the boat is on the rhs
TypeOK == /\ cl \in 0..3
/\ ml \in 0..3
/\ cr \in 0..3
/\ mr \in 0..3
/\ boat \in 0..1
Init == /\ cl = 3
/\ ml = 3
/\ cr = 0
/\ mr = 0
/\ boat = 0
(***************************************************************************)
(* Now we define the actions that can happen. There are ten. *)
(* Because the boat changes sides each time a crossing is made, only 5 are *)
(* possible at any given time. *)
(***************************************************************************)
BoatLR1C == /\ boat = 0
/\ cl >= 1
/\ \/ mr = 0
\/ mr >= cr+1
/\ boat' = 1
/\ cl' = cl-1
/\ UNCHANGED <<ml>>
/\ cr' = cr+1
/\ UNCHANGED <<mr>>
BoatLR2C == /\ boat = 0
/\ cl >= 2
/\ \/ mr = 0
\/ mr >= cr+2
/\ boat' = 1
/\ cl' = cl-2
/\ UNCHANGED <<ml>>
/\ cr' = cr+2
/\ UNCHANGED <<mr>>
BoatLR1M == /\ boat = 0
/\ ml >= 1
/\ \/ ml-1 = 0
\/ ml-1 >= cl
/\ mr+1 >= cr
/\ boat' = 1
/\ ml' = ml-1
/\ UNCHANGED <<cl>>
/\ mr' = mr+1
/\ UNCHANGED <<cr>>
BoatLR2M == /\ boat = 0
/\ ml >= 2
/\ \/ ml-2 = 0
\/ ml-2 >= cl
/\ mr+2 >= cr
/\ boat' = 1
/\ ml' = ml-2
/\ UNCHANGED <<cl>>
/\ mr' = mr+2
/\ UNCHANGED <<cr>>
BoatLR1C1M == /\ boat = 0
/\ cl >= 1
/\ ml >= 1
/\ \/ ml-1 = 0
\/ ml-1 >= cl-1
/\ mr+1 >= cr+1
/\ boat' = 1
/\ cl' = cl-1
/\ ml' = ml-1
/\ cr' = cr+1
/\ mr' = mr+1
BoatRL1C == /\ boat = 1
/\ cr >= 1
/\ \/ ml = 0
\/ ml >= cl+1
/\ boat' = 0
/\ cr' = cr-1
/\ UNCHANGED <<mr>>
/\ cl' = cl+1
/\ UNCHANGED <<ml>>
BoatRL2C == /\ boat = 1
/\ cr >= 2
/\ \/ ml = 0
\/ ml >= cl+2
/\ boat' = 0
/\ cr' = cr-2
/\ UNCHANGED <<mr>>
/\ cl' = cl+2
/\ UNCHANGED <<ml>>
BoatRL1M == /\ boat = 1
/\ mr >= 1
/\ \/ mr-1 = 0
\/ mr-1 >= cr
/\ ml+1 >= cl
/\ boat' = 0
/\ mr' = mr-1
/\ UNCHANGED <<cr>>
/\ ml' = ml+1
/\ UNCHANGED <<cl>>
BoatRL2M == /\ boat = 1
/\ mr >= 2
/\ \/ mr-2 = 0
\/ mr-2 >= cr
/\ ml+2 >= cl
/\ boat' = 0
/\ mr' = mr-2
/\ UNCHANGED <<cr>>
/\ ml' = ml+2
/\ UNCHANGED <<cl>>
BoatRL1C1M == /\ boat = 1
/\ cr >= 1
/\ mr >= 1
/\ \/ mr-1 = 0
\/ mr-1 >= cr-1
/\ ml+1 >= cl+1
/\ boat' = 0
/\ cr' = cr-1
/\ mr' = mr-1
/\ cl' = cl+1
/\ ml' = ml+1
Next == \/ BoatLR1C
\/ BoatLR2C
\/ BoatLR1M
\/ BoatLR2M
\/ BoatLR1C1M
\/ BoatRL1C
\/ BoatRL2C
\/ BoatRL1M
\/ BoatRL2M
\/ BoatRL1C1M
Spec == Init /\ [][Next]_<<cl, ml, cr, mr, boat>>
-----------------------------------------------------------------------------
(***************************************************************************)
(* The puzzle is solved when all parties are safely across the river, *)
(***************************************************************************)
Solved == /\ cl = 0
/\ ml = 0
/\ cr = 3
/\ mr = 3
/\ boat = 1
NotSolved == ~Solved
(*NotSolved == \/ cl # 0
\/ ml # 0
\/ cr # 3
\/ mr # 3
\/ boat # 1*)
=============================================================================