Last active
June 6, 2016 17:51
-
-
Save konnov/17a182a4e223d4173c8a2db3fc6879f6 to your computer and use it in GitHub Desktop.
Yet another bridge puzzle in TLA+
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
---------------------------- 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment