Re: Using TLA+ to solve a logic puzzle

[Dominik Hansen <do.han...@xxxxxxxxxxxxxx>]

Hello,

there are some typo errors in your specification ("green" # "Green"):

 

Colors == { "white", "yellow", "blue", "red", "green" }

    (painted[h] = "Green" /\ livesin[p] = h) => drinks[p] = "coffee"

You should use model values instead of strings.

 

I modified your specification at some points and then run the model checker & constraint solver ProB on it.

Note: I assign values to some of the constants in the config file (only model values) and ProB finds values for the rest.

ProB finds a single constant setup satisfying the ASSUME clause. Hence the solution is unique:

livesin = (Brit:>3 @@ Swede:>5 @@ Dane:>2 @@ Norwegian:>1 @@ German:>4)

painted = (1:>yellow @@ 2:>blue @@ 3:>red @@ 4:>green @@ 5:>white)

keeps = (Brit:>birds @@ Swede:>dogs @@ Dane:>horses @@ Norwegian:>cats @@ German:>fish)

drinks = (Brit:>milk @@ Swede:>beer @@ Dane:>tea @@ Norwegian:>water @@ German:>coffee)

smokes = (Brit:>Pall_Mall @@ Swede:>Winfield @@ Dane:>Marlboro @@ Norwegian:>Dunhill @@ German:>Rothmans)

keepsTheFish = German

( :> and @@ are operators of the standard module TLC. In the screenshot is an error displaying functions. << >> should be replaced by ( )  )  

Best regards,

Dominik

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

EXTENDS Integers

CONSTANTS

Brit, Swede, Dane, Norwegian, German,

white, yellow, blue, red, green,

birds, cats, dogs, horses, fish, 

tea, coffee, milk, beer, water, 

Pall_Mall, Dunhill, Marlboro, Winfield, Rothmans,

livesin, painted, keeps, drinks, smokes, keepsTheFish

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 p1,p2 \in People : p1 # p2 => livesin[p1] # livesin[p2]) 

           /\ (\A p1,p2 \in People : p1 # p2 => keeps[p1] # keeps[p2])

           /\ (\A p1,p2 \in People : p1 # p2 => drinks[p1] # drinks[p2])

           /\ (\A p1,p2 \in People : p1 # p2 => smokes[p1] # smokes[p2])

           /\ (\A c1,c2 \in Houses : c1 # c2 => painted[c1] # painted[c2]) 

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

ASSUME Constraints /\ keeps[keepsTheFish] =  fish

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

\* CONSTANT declarations
CONSTANT German = German
\* CONSTANT declarations
CONSTANT coffee = coffee
\* CONSTANT declarations
CONSTANT water = water
\* CONSTANT declarations
CONSTANT white = white
\* CONSTANT declarations
CONSTANT yellow = yellow
\* CONSTANT declarations
CONSTANT green = green
\* CONSTANT declarations
CONSTANT Rothmans = Rothmans
\* CONSTANT declarations
CONSTANT Winfield = Winfield
\* CONSTANT declarations
CONSTANT birds = birds
\* CONSTANT declarations
CONSTANT Dunhill = Dunhill
\* CONSTANT declarations
CONSTANT Swede = Swede
\* CONSTANT declarations
CONSTANT red = red
\* CONSTANT declarations
CONSTANT dogs = dogs
\* CONSTANT declarations
CONSTANT blue = blue
\* CONSTANT declarations
CONSTANT tea = tea
\* CONSTANT declarations
CONSTANT Brit = Brit
\* CONSTANT declarations
CONSTANT cats = cats
\* CONSTANT declarations
CONSTANT beer = beer
\* CONSTANT declarations
CONSTANT Dane = Dane
\* CONSTANT declarations
CONSTANT horses = horses
\* CONSTANT declarations
CONSTANT milk = milk
\* CONSTANT declarations
CONSTANT Pall_Mall = Pall_Mall
\* CONSTANT declarations
CONSTANT Norwegian = Norwegian
\* CONSTANT declarations
CONSTANT Marlboro = Marlboro
\* CONSTANT declarations
CONSTANT fish = fish

\* Generated on Sun Jun 01 20:11:38 CEST 2014

Attachment: fish.tla
Description: Binary data