[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sun, 1 Jun 2014 08:31:20 -0700 (PDT)*References*: <CACkJihO4vd5BjFGyfX_0DFV4DB3XLwzS2qV_v3+bDM0YJRoNFA@mail.gmail.com>

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: InitNext: NextWhat to check?Invariants: NobodyHasTheFish(all other options are default)Here's my module, fish.tla:-------------------------------- MODULE fish ------------------------------ --

EXTENDS IntegersVARIABLES livesin, painted, keeps, drinks, smokesPeople == { "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..5TypeOK == /\ 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] = cNeighbor(p1, p2) == livesin[p2] \in { livesin[p1] - 1, livesin[p1] + 1 }

TheBritLivesInTheRedHouse == \A h \in Houses : painted[h] = "red" => livesin["Brit"] = hTheSwedeKeepsDogsAsPets == keeps["Swede"] = "dogs"TheDaneDrinksTea == drinks["Dane"] = "tea"TheGreenHouseIsOnTheLeftOfTheWhiteHouse == \A h1, h2 \in Houses : (painted[h1] = "green" /\ painted[h2] = "white") => h1 = h2 - 1TheGreenHousesOwnerDrinksCoffee == \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] = hTheManLivingInTheCenterHouseDrinksMilk == \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 == ConstraintsNext == UNCHANGED << livesin, painted, keeps, drinks >>

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

**References**:**Using TLA+ to solve a logic puzzle***From:*Lorin Hochstein

- Prev by Date:
**Re: Using TLA+ to solve a logic puzzle** - Next by Date:
**Re: Using TLA+ to solve a logic puzzle** - Previous by thread:
**Re: Using TLA+ to solve a logic puzzle** - Next by thread:
**Re: Using TLA+ to solve a logic puzzle** - Index(es):