Re: Using TLA+ to solve a logic puzzle

Hello,

TLC is not the right tool to solve this kind of problem: it is an explicit-state model checker, not a constraint solver. From the first conjunct in your set of constraints, TLC will try to compute all type-correct states. Now, all of your sets have 5 elements, hence each set of functions of the form [ People -> Houses ] etc. contains 5^5 possible functions. Given that you have 5 variables, each of which can take that many values, you have a potential state space of (5^5)^5 assignments, which makes about 3E17 possible states. TLC tries to generate each of these assignments one by one, then filter out those that are impossible due to the other constraints.

I suggest you use a constraint solver. You could try ProB, available from http://www.stups.uni-duesseldorf.de/ProB/index.php5/The_ProB_Animator_and_Model_Checker, which can handle TLA+ specifications.

In fact, your encoding of the puzzle as a TLA+ specification with a stuttering next-state action is somewhat artificial: it would be more natural to declare livesin, painted, ..., smokes as CONSTANTs and check if the conjunction of the predicates given in Constraints and the formula \E p \in People : keeps[p] = "fish" (or the equivalent finite disjunction for the elements of People) is satisfiable, then extract a model. If you want to know if the solution is unique, you could add the negation of the solution (say, it's the Swede, then add ... /\ keeps[Swede] # fish) and check that now the problem becomes unsatisfiable.

TLA+ is meant for analyzing transition systems that usually start from a small set of initial states and evolve according to transition rules.

Hope this helps,

Stephan

On Sunday, June 1, 2014 4:56:58 PM UTC+2, Lorin Hochstein wrote:

To start learning how to use TLA+, I'm trying to use the toolbox to solve a logic puzzle.

I specified an invariant that should be false in order to get the model checker to return an error and provide a counter-example that solves the puzzle ("who owns the fish"?)

However, when I run the model checker on my module, it doesn't terminate after executing for at least 100 minutes, so I suspect I'm doing something wrong.

I'm running the model checker with the following parameters:

Behavior spec:
Init: Init
Next: Next

What to check?
Invariants: NobodyHasTheFish

(all other options are default)

Here's my module, fish.tla:

-------------------------------- MODULE fish --------------------------------

EXTENDS Integers

VARIABLES livesin, painted, keeps, drinks, smokes

People == { "Brit", "Swede", "Dane", "Norwegian", "German" }

Colors == { "white", "yellow", "blue", "red", "green" }
Pets == { "birds", "cats", "dogs", "horses", "fish" }

Beverages == { "tea", "coffee", "milk", "beer", "water" }
Cigarettes == { "Pall Mall", "Dunhill", "Marlboro", "Winfield", "Rothmans" }

Houses == 1..5

TypeOK == /\ livesin \in [ People -> Houses ]

/\ keeps \in [ People -> Pets ]
/\ drinks \in [ People -> Beverages ]
/\ smokes \in [ People -> Cigarettes ]

/\ painted \in [ Houses -> Colors ]

FuncsAreOnto == /\ \A h \in Houses : \E p \in People : livesin[p] = h

/\ \A c \in Colors : \E h \in Houses : painted[h] = c
/\ \A t \in Pets : \E p \in People : keeps[p] = t

/\ \A b \in Beverages : \E p \in People : drinks[p] = b
/\ \A c \in Cigarettes : \E p \in People : smokes[p] = c

Neighbor(p1, p2) == livesin[p2] \in { livesin[p1] - 1, livesin[p1] + 1 }

TheBritLivesInTheRedHouse == \A h \in Houses : painted[h] = "red" => livesin["Brit"] = h
TheSwedeKeepsDogsAsPets == keeps["Swede"] = "dogs"

TheDaneDrinksTea == drinks["Dane"] = "tea"
TheGreenHouseIsOnTheLeftOfTheWhiteHouse == \A h1, h2 \in Houses :

(painted[h1] = "green" /\ painted[h2] = "white") => h1 = h2 - 1
TheGreenHousesOwnerDrinksCoffee == \A p \in People, h \in Houses :

(painted[h] = "Green" /\ livesin[p] = h) => drinks[p] = "coffee"
ThePersonWhoSmokesPallMallRearsBirds == \A p \in People :

(smokes[p] = "Pall Mall") => keeps[p] = "birds"
TheYellowHouseOwnerSmokesDunhill == \A p \in People, h \in Houses:

(smokes[p] = "Dunhill" /\ painted[h] = "yellow") => livesin[p] = h
TheManLivingInTheCenterHouseDrinksMilk == \A p \in People :

(livesin[p] = 3) => (drinks[p] = "milk")
TheNorwegianLivesInTheFirstHouse == livesin["Norwegian"] = 1

ThePersonWhoSmokesMarlboroLiveNextToTheOneWhoKeepsCats == \A p1,p2 \in People :
(smokes[p1] = "Marlboro" /\ keeps[p2] = "cats") => Neighbor(p1, p2)

ThePersonWhoKeepsHorsesLivesNextToThePersonWhoSmokesDunhill == \A p1,p2 \in People :
(keeps[p1] = "horses" /\ smokes[p2] = "Dunhill") => Neighbor(p1, p2)

ThePersonWhoSmokesWinfieldDrinksBeer == \A p \in People:
(smokes[p] = "Winfield") => (drinks[p] = "Beer")

TheGermanSmokesRothmans == smokes["German"] = "Rothmans"
TheNorwegianLivesNextToTheBlueHouse == \A p \in People :

painted[livesin[p]] = "blue" => Neighbor("Norwegian", p)
ThePersonWhoSmokesMarlboroHasNeighborWhoDrinksWater == \A p1,p2 \in People :

(smokes[p1] = "Marlboro" /\ drinks[p2] = "water") => Neighbor(p1, p2)

Constraints == /\ TypeOK
/\ FuncsAreOnto
/\ TheBritLivesInTheRedHouse

/\ TheSwedeKeepsDogsAsPets
/\ TheDaneDrinksTea
/\ TheGreenHouseIsOnTheLeftOfTheWhiteHouse

/\ TheGreenHousesOwnerDrinksCoffee
/\ ThePersonWhoSmokesPallMallRearsBirds
/\ TheYellowHouseOwnerSmokesDunhill

/\ TheManLivingInTheCenterHouseDrinksMilk
/\ TheNorwegianLivesInTheFirstHouse
/\ ThePersonWhoSmokesMarlboroLiveNextToTheOneWhoKeepsCats

/\ ThePersonWhoKeepsHorsesLivesNextToThePersonWhoSmokesDunhill
/\ ThePersonWhoSmokesWinfieldDrinksBeer

/\ TheGermanSmokesRothmans
/\ TheNorwegianLivesNextToTheBlueHouse
/\ ThePersonWhoSmokesMarlboroHasNeighborWhoDrinksWater

NobodyHasTheFish == ~ \E p \in People: keeps[p] = "fish"

Init == Constraints
Next == UNCHANGED << livesin, painted, keeps, drinks >>

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