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

Re: [tlaplus] TLA+ Specification for Einsteins Riddle



Hi Christian,

I'm assuming you're interested in writing the brute-force solver as your spec, instead of trying to solve the problem with set operations on a function set.

When models get large, it's worth doing a back-of-envelope calculation to get an estimate for roughly how large it should be. Let's assume we make the "removing none" optimization, so all values are always assigned. There are five properties per house and 5! possibilities for each property, so we'd expect the state space to be at least 5!⁵ 24 billion states. If we allow one value to also be null, we now have (5! + (5 choose 4)*4!)⁵ ≈ 800 billion states.

(I'm being a bit sloppy with the math, but the point here is the magnitudes: you're working with a much bigger state space than you expected.)

The best way to optimize this is to fold the problem structure into your spec. For example, we have

9 the Norwegian lives in the first house      

So there's no reason to explore any state where that's false: it can't be a solution, and it's not a necessary state on the "path" to the real solution. If you don't want to change the spec, you can add owner[h1] = Norweigan to the "State Constraints" in the TLA+ Toolbox. You won't be able to do this with all of the rules, but you should be able to do this with enough of them to make the problem tractable.

Answering specific questions:


Q1: Is there anything I can do to improve my specification to run  
the TLC model checker on it i.e. some tricks to prevent the state
explosion problem?

A couple of other recommendations I'd make: since houses and houseOrder never change, move them to operators. Then you don't need StaticData.

Instead of storing the house order as a set of tuples, why not just write <<h1, h2, h3, h4, h5>>? You might even want to consider just making the houses 1 2 3 4 5 and not worry about special constants for them.

Also, getting rid of "none" states and instead swapping will lead to a much smaller model, as you found out already.

Q2: While running the TLC model checker, I got output like this
(line wrapped for readability):

--8<---------------cut here---------------start------------->8---
 ...
Progress(7) at 2021-02-25 15:25:21: 53,778,336 states generated
   (27,490,150 s/min),
   4,258,962 distinct states found (1,912,070 ds/min),
   3,721,176 states left on queue.
Progress(8) at 2021-02-25 15:26:21: 77,487,511 states generated
  (23,709,175 s/min),
   5,818,666 distinct states found (1,559,704 ds/min),
   5,043,790 states left on
 queue.
  ...
--8<---------------cut here---------------end--------------->8---

What does the number in curved brackets mean i.e. 7 in
Progress(7) or 8 in Progress(8)?
That's the report number. Progress(8) means it's the 8th time it's reporting statistics.
I am wondering about so many states?  Perhaps, I made an error in
my TLA+ specification or is that amount of states generated
reasonable?

Q3: Is there a specific reason why TLC can not compare a string
value or number with the empty set?
With the TLA+ REPL Shell, I get:

--8<---------------cut here---------------start------------->8---
..
Enter a constant-level TLA+ _expression_.
(tla+) 1 = {}
1 = {}
Error evaluating _expression_: '1 = {}'
--8<---------------cut here---------------end--------------->8---
TLA+ is an untyped formalism: we don't know whether or not 1 = {}. In practice, this is usually a sign someone made a mistake in the model, so TLC treats it as an error.
Q4: I also tried to remove constrains in the `Solution' action.
It seems that with one constraint, TLC is able to find a
counterexample very fast and reports it.  But when I am adding an
additional constraint, the TLC model checker generates a lot/too
many states.  Can anyone elaborate on this how the TLC model
checker operates with a formula like `Solution' and why it
generates so many states?  Is this due to many \E and
alternations?

By removing a constraint from Solution, you significantly increased the number of states that count as a solution, so TLC found a solution much quicker.

H

Thanks for your help,
  Christian B.



TLA+ Specification:

--8<---------------cut here---------------start------------->8---
------------------- MODULE einstein ------------------------
(* Literature/Source:                                               *)
(* [1] https://udel.edu/~os/riddle.html                             *)
(* **************************************************************** *)
(* Situation                                                        *)
(* **************************************************************** *)
(* - There are 5 houses in five different colors.                   *)
(* - In each house lives a person with a different nationality.     *)
(* - These five owners drink a certain type of beverage, smoke a    *)
(*   certain brand of cigar and keep a certain pet.                 *)
(* - No owners have the same pet, smoke the same brand of cigar or  *)
(*   drink the same beverage.                                       *)
(* **************************************************************** *)
(* Rules                                                            *)
(* **************************************************************** *)
(*  1 the Brit lives in the red house                               *)
(*  2 the Swede keeps dogs as pets                                  *)
(*  3 the Dane drinks tea                                           *)
(*  4 the green house is on the left of the white house             *)
(*  5 the green house's owner drinks coffee                         *)
(*  6 the person who smokes Pall Mall rears birds                   *)
(*  7 the owner of the yellow house smokes Dunhill                  *)
(*  8 the man living in the center house drinks milk                *)
(*  9 the Norwegian lives in the first house                        *)
(* 10 the man who smokes blends lives next to the one who keeps cats*)
(* 11 the man who keeps horses lives next to man who smokes Dunhill *)
(* 12 the owner who smokes BlueMaster drinks beer                   *)
(* 13 the German smokes Prince                                      *)
(* 14 the Norwegian lives next to the blue house                    *)
(* 15 the man who smokes blend has a neighbor who drinks water      *)
(* **************************************************************** *)

EXTENDS Naturals, FiniteSets
CONSTANTS
  univ_colors,
  univ_pets,
  univ_cigars,
  univ_drinks,
  univ_nations

VARIABLE
  owner,
  colors,       \* {red, white, blue, gree, yellow}
  pets,         \* {bird, cat, dog, fish, horse}
  cigars,       \* {blend, bluemaster, dunhill, pallmall, prince
  drinks,       \* {beer, coffee, milk, tea, water}
  houses,       \* {h1, h2, h3, h4, h5}
  houseOrder,   \* {<<h1, h2>>, <<h2, h3>>, <<h3, h4>>, <<h4, h5>>
  nations       \* {brit, swede, dane, norwegian, german}

TypeOK ==
  /\ colors \subseteq univ_colors
  /\ pets \subseteq univ_pets
  /\ cigars \subseteq univ_cigars
  /\ drinks \subseteq univ_drinks
  /\ houses \subseteq {"h1", "h2", "h3", "h4", "h5" }
  /\ houseOrder \subseteq (houses \X houses)
  /\ nations \subseteq univ_nations
  /\ owner \in [ houses ->
      [ color: univ_colors,
        pet: univ_pets,
        cigar: univ_cigars,
        nation: univ_nations,
        drink: univ_drinks ]]

StaticData == UNCHANGED <<houseOrder, houses>>
------------------------------------------------------------

AssignColor(h, c) ==
  /\ owner[h].color = "none"
  /\ owner' = [ owner EXCEPT ![h] = [ @ EXCEPT !.color = c ]]
  /\ colors' = colors \ {c}
  /\ UNCHANGED <<pets, cigars, drinks, nations>>
  /\ StaticData

AssignPet(h, p) == 
  /\ owner[h].pet = "none"
  /\ owner' = [ owner EXCEPT ![h] = [ @ EXCEPT !.pet = p ]]
  /\ pets' = pets \ {p}
  /\ UNCHANGED <<colors, cigars, drinks, nations>>
  /\ StaticData
  
AssignCigar(h, c) == 
  /\ owner[h].cigar = "none"
  /\ owner' = [ owner EXCEPT ![h] = [ @ EXCEPT !.cigar = c ]]
  /\ cigars' = cigars \ {c}
  /\ UNCHANGED <<colors, pets, drinks, nations>>
  /\ StaticData

AssignDrink(h, b) ==
  /\ owner[h].drink = "none"
  /\ owner' = [ owner EXCEPT ![h] = [ @ EXCEPT !.drink = b ]]
  /\ drinks' = drinks \ {b}
  /\ UNCHANGED <<colors, pets, cigars, nations>>
  /\ StaticData

AssignNation(h, n) ==
  /\ owner[h].nation = "none"
  /\ owner' = [ owner EXCEPT ![h] = [ @ EXCEPT !.nation = n ]]
  /\ nations' = nations \ {n}
  /\ UNCHANGED <<colors, pets, drinks, cigars>>
  /\ StaticData

RejectColor(h, c) ==
  /\ owner[h].color = c
  /\ owner' = [ owner EXCEPT ![h] = [ @EXCEPT !.color = "none" ]]
  /\ colors' = colors \cup {c}
  /\ UNCHANGED <<pets, drinks, cigars, nations>>
  /\ StaticData

RejectPet(h, p) ==
  /\ owner[h].pet = p
  /\ owner' = [ owner EXCEPT ![h] = [ @EXCEPT !.pet = "none" ]]
  /\ pets' = pets \cup {p}
  /\ UNCHANGED <<colors, drinks, cigars, nations>>
  /\ StaticData

RejectCigar(h, c) ==
  /\ owner[h].cigar = c
  /\ owner' = [ owner EXCEPT ![h] = [ @EXCEPT !.cigar = "none" ]]
  /\ cigars' = cigars \cup {c}
  /\ UNCHANGED <<colors, drinks, pets, nations>>
  /\ StaticData

RejectDrink(h, b) ==
  /\ owner[h].drink = b
  /\ owner' = [ owner EXCEPT ![h] = [ @EXCEPT !.drink = "none" ]]
  /\ drinks' = drinks \cup {b}
  /\ UNCHANGED <<colors, cigars, pets, nations>>
  /\ StaticData

RejectNation(h, n) ==
  /\ owner[h].nation = n
  /\ owner' = [ owner EXCEPT ![h] = [ @EXCEPT !.nation = "none" ]]
  /\ nations' = nations \cup {n}
  /\ UNCHANGED <<colors, cigars, pets, drinks>>
  /\ StaticData

Init ==
  /\ colors = univ_colors
  /\ pets = univ_pets
  /\ cigars = univ_cigars
  /\ drinks = univ_drinks
  /\ houses = {"h1", "h2", "h3", "h4", "h5"}
  /\ houseOrder = {<<"h1", "h2">>, <<"h2", "h3">>,
                   <<"h3", "h4">>, <<"h4", "h5">> }
  /\ nations = univ_nations
  /\ owner = [o \in houses |->
                [ color |-> "none",
                  pet |-> "none",
                  cigar |-> "none",
                  nation |-> "none",
                  drink |-> "none" ]]

Assign(h) ==
  \/ \E c \in colors: AssignColor(h, c)
  \/ \E c \in pets: AssignPet(h, c)
  \/ \E c \in cigars: AssignCigar(h, c)
  \/ \E c \in drinks: AssignDrink(h, c)
  \/ \E c \in nations: AssignNation(h, c)      
  
Reject(h) ==
  \/ \E c \in univ_colors: RejectColor(h, c)
  \/ \E c \in univ_pets: RejectPet(h, c)
  \/ \E c \in univ_cigars: RejectCigar(h, c)
  \/ \E c \in univ_drinks: RejectDrink(h, c)
  \/ \E c \in univ_nations: RejectNation(h, c)        

Next ==
  \/ \E h \in houses: Assign(h)
  \/ \E h \in houses: Reject(h)

IsMiddleHouse(hmiddle) ==
  \* the middle house has two neighbours on the left and right:
  \* h1 -> h2 -> hmiddle -> h3 -> h4
  \E h1, h2, h3, h4 \in houses:
     /\ <<h1, h2>> \in houseOrder /\ <<h2, hmiddle>> \in houseOrder
     /\ <<hmiddle, h3>> \in houseOrder /\ <<h3, h4>> \in houseOrder

LivesNext(h2, h1) ==
  \* h2 lives next to h1 (somewhere on the right side)
  \/ <<h1, h2>> \in houseOrder
  \/ /\ \E h3 \in houses: <<h1, h3>> \in houseOrder
     /\ <<h3, h2>> \in houseOrder
  \/ \E h3,h4 \in houses:
     /\ <<h1, h3>> \in houseOrder
     /\ <<h3, h4>> \in houseOrder
     /\ <<h4, h2>> \in houseOrder
  \/ \E h3, h4, h5 \in houses:
     /\ <<h1, h3>> \in houseOrder
     /\ <<h3, h4>> \in houseOrder
     /\ <<h4, h5>> \in houseOrder
     /\ <<h5, h2>> \in houseOrder

IsNeighbour(h1, h2) ==
  <<h1, h2>> \in houseOrder \/ <<h2, h1>> \in houseOrder
  
------------------------------------------------------------
Solution ==
\* 1. ------------------------------------------------------------------
/\ \E h \in houses: owner[h].color = "red" /\ owner[h].nation = "brit"
/\ \E h \in houses: owner[h].nation = "swede" /\ owner[h].pet = "dogs"
/\ \E h \in houses: owner[h].nation = "dane" /\ owner[h].drink = "tea"
/\ \E h1, h2 \in houses:
   /\ h1 # h2 /\ owner[h1].color = "green"
   /\ owner[h2].color = "white" /\ <<h1, h2>> \in houseOrder
\* 5. ------------------------------------------------------------------
/\ \E h \in houses: owner[h].color = "green" /\ owner[h].drink = "coffee"
/\ \E h \in houses: owner[h].cigar = "pm" /\ owner[h].pet = "birds"
/\ \E h \in houses: owner[h].color = "yellow" /\ owner[h].cigar = "dunhill"
/\ \E h \in houses: IsMiddleHouse(h) /\ owner[h].drink = "milk"
/\ \E h \in houses: h = "h1" /\ owner[h].nation = "norwegian"
\* 10. ------------------------------------------------------------------
/\ \E h1, h2 \in houses:
   /\ h1 # h2 /\ owner[h1].cigar = "blend"
   /\ owner[h2].pet = "cat" /\ LivesNext(h1, h2)
/\ \E h1, h2 \in houses:
   /\ h1 # h2 /\ owner[h1].pet = "horses"
   /\ owner[h2].cigar = "dunhill" /\ LivesNext(h1, h2)
/\ \E h \in houses: owner[h].cigar = "bm" /\ owner[h].drink = "beer"
/\ \E h \in houses: owner[h].nation = "german" /\ owner[h].cigar = "prince"
/\ \E h1, h2 \in houses:
   /\ owner[h1].nation = "norwegian" /\ owner[h2].color = "blue"
   /\ LivesNext(h1, h2)
\* 15. ------------------------------------------------------------------   
/\ \E h1, h2 \in houses:
   /\ owner[h1].cigar = "blend"
   /\ owner[h2].drink = "water"
   /\ IsNeighbour(h1, h2)

FindSolution == \neg(Solution)
------------------------------------------------------------
============================================================
--8<---------------cut here---------------end--------------->8---


einstein.cfg, executed with:
  /usr/bin/time -l \
       java -cp tla2tools.jar \
       tlc2.TLC \
       -config ./einstein.cfg einstein.tla

--8<---------------cut here---------------start------------->8---
CONSTANTS
  univ_colors = {"red", "white", "blue", "green", "yellow", "none" }
  univ_pets = {"bird", "cat", "dog", "fish", "horse", "none"}
  univ_cigars = {"blend", "bm", "dunhill", "pm", "prince", "none"}
  univ_drinks = {"beer", "coffee", "milk", "tea", "water", "none"}
  univ_nations = {"brit", "swede", "dane", "norwegian", "german", "none"}
INVARIANT TypeOK
INVARIANT FindSolution
INIT Init
NEXT Next
--8<---------------cut here---------------end--------------->8---


[1] https://udel.edu/~os/riddle.html

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f20cf55e-304f-9283-45e5-5a5bfe5323e9%40gmail.com.