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.
That's the report number. Progress(8) means it's the 8th time it's reporting statistics.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)?
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
--