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

Using TLA+ to solve a logic puzzle



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 >>

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