Yet another bridge puzzle in TLA+

bridge.tla

---------------------------- MODULE bridgePuzzle ----------------------------
(*
  Use TLC from TLA Toolbox to solve this puzzle:
    http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html

  A family of four people (the father, the mother, the baby, and the grandmother)
  have to cross a bridge at night having only one flashlight.
  At most two people can cross the bridge at a time holding
  the flashlight in their hands. It takes each member of the family the
  following time to cross the bridge in either direction: father needs 1 minute,
  mother needs 2 minutes, baby needs 5 minutes, and grandmother needs 10 minutes.
  
  Can all of them cross the bridge as fast as in 17 minutes?
 *)

EXTENDS Integers, FiniteSets

CONSTANTS speed
  (* time it takes each person to cross the bridge (in fact, it is inverted speed) *)
  (* e.g., [x \in Persons |-> IF x = "father" THEN 1 ELSE IF x = "mother" THEN 2 ELSE IF x = "baby" THEN 5 ELSE 10] *)

VARIABLES
    pos,    (* the positions of the persons and of the flashlight *)
    clock,  (* the global clock *)
    turn    (* whose turn is to move *)

Persons == {"baby", "father", "mother", "grandma"}
Objects == Persons \cup {"flashlight"}

(* only the following turns are allowed *)
AllowedTurn(t, p) ==
  \E S \in SUBSET Persons:
    (* at most two persons are crossing the bridge *)
    /\ t = S /\ (Cardinality(S) = 1 \/ Cardinality(S) = 2)
    (* the flashlight is on the same side of the bridge *)
    /\ \A x \in S: p["flashlight"] = p[x]

(* the initial states *)
Init ==
    /\ pos = [x \in Objects |-> "LEFT"]
    /\ clock = 0
    /\ AllowedTurn(turn, pos)
    
(* move a person or the flashlight *)    
Update(x) ==
    IF x # "flashlight" /\ x \notin turn
    THEN pos[x] (* not moving *)
    ELSE IF pos[x] = "LEFT" THEN "RIGHT" ELSE "LEFT" (* flipping sides *)    

Next ==
  /\ pos' = [x \in Objects |-> Update(x)]     (* update the positions *)
  /\ AllowedTurn(turn', pos')                 (* pick the next turn   *)
  /\ \E slowest \in turn: (* the slowest person in the moving set *)
    slowest \in turn /\ clock' = clock + speed[slowest] (* update the clock *)
      /\ \A x \in turn: speed[slowest] >= speed[x] 

Spec == Init /\ [Next]_<<pos, clock, turn>>

(*
 We want to disprove the following invariant candidate.

 NOTE: use the following state constraint to restrict the model checker's search space:
   clock <= 17
 *)
Inv ==
  \/ clock > 17                         (* too slow *)
  \/ \E x \in Objects: pos[x] = "LEFT"  (* somebody has not crossed the bridge *)

(*
  This constraint is not required to find a solution, but it is a good idea to
  specify a type invariant.
 *)
TypeOK ==
    /\ speed \in [ Persons -> Nat ]
    /\ pos \in [ Objects -> {"LEFT", "RIGHT"}]
    /\ \A x \in Objects: pos[x] \in {"LEFT", "RIGHT"}
    /\ clock \in Int
    /\ AllowedTurn(turn, pos)
    
=============================================================================
\* Modification History
\* Last modified Mon Jun 06 19:50:54 CEST 2016 by igor
\* Created Mon Jun 06 18:27:42 CEST 2016 by igor