TLA+ Specification for Einsteins Riddle

[Christian Barthel]

Hello,

I am currently studying TLA+ and try to do a lot of different
exercises to get comfortable with the language and tools.
Recently, I tried to solve Einsteins Riddle [1] with TLA+ and
created a specification and a TLC configuration (Spec and config
below).

The problem with this is that I can't model check it with TLC because
it generates a lot of states (executed on an ordinary notebook,
roughly 10 years old).
I tried some variations with it like removing the "none" value
and directly assigning values initially (INIT) and switching two
arbitrarily chosen values in the Next action.
The goal was to reduce the state space (at least a bit), but it
was not possible to solve the puzzle so far.

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?

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

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?

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
--
Christian Barthel <b...@online.de>

[Hillel Wayne]

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

[Markus Kuppe]

On 03.03.21 13:56, Hillel Wayne wrote:
>> 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.

TLC reports statistics, i.e., Progress every minute. At the beginning of
model-checking, the number N in "Progress(N)" indeed correlates with
TLC's reporting. However, N actually is what the Toolbox reports as
"diameter", which is the length of the longest behavior found so far
(remember, breadth-first search). Usually, after a while, the diameter
stagnates for extended periods before TLC starts to generate the next
longer behavior.

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

Try to reduce the size of these sets to keep the state-space explosion
at bay, assuming that the small model/scope hypothesis applies to this
riddle as well. In other words, you will likely be able to learn
everything useful about your spec and its properties even without those
beer-drinking Germans. ;-)

M.

[Christian Barthel]

Hillel,
Markus,

thanks for your answers and giving me some advice (and good tips)
where to look next. I am going to try this now and improve my
specification.

Markus Kuppe <tlaplus-go...@lemmster.de> writes:

> On 03.03.21 13:56, Hillel Wayne wrote:

[..]

>> That's the report number. Progress(8) means it's the 8th time it's
>> reporting statistics.
>
>
> TLC reports statistics, i.e., Progress every minute. At the beginning
> of model-checking, the number N in "Progress(N)" indeed correlates
> with TLC's reporting. However, N actually is what the Toolbox reports
> as "diameter", which is the length of the longest behavior found so
> far (remember, breadth-first search). Usually, after a while, the
> diameter stagnates for extended periods before TLC starts to generate
> the next longer behavior.

OK thanks for the insights! I guess, that also explains why the
number doesn't start with "1".

>> 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"}
>
>
> Try to reduce the size of these sets to keep the state-space explosion
> at bay, assuming that the small model/scope hypothesis applies to this
> riddle as well. In other words, you will likely be able to learn
> everything useful about your spec and its properties even without
> those beer-drinking Germans. ;-)

I guess that Hillel pointed me in the same direction with using
CONSTRAINT in the model configuration. This will be interesting
how this works out (I read about that option and forgot about it
because I was doing fine with INVARIANT and CONSTANTS options in
the TLC model configurations so far).

--
Christian Barthel <b...@online.de>

[Christian Barthel]

Hillel Wayne <hwa...@gmail.com> writes:

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

This sounds like you have another approach in mind than the
brute-force one? Can you elaborate a bit on how the problem
might be solved with "set operations on a function set"?

I was able to complete the TLC model checking part (by applying
the tips I got from you and Markus Kuppe, thanks).

What I did change:

* use natural numbers to represent the houses,
* use default natural number ordering,
* write/update a swap action to reassign values,
* remove the "none" value and reduce possible state space,
* I spotted and fixed some errors in my initial spec
(like "birds" vs "bird")
* I wrote a few CONSTRAINTS to further limit the state space
(I actually wanted to write even more constraints but TLC
found a solution before I had the chance to do so). The
number of states explored is still, quite big.

The final spec, the TLC configuration file and the TLC output is
attached below if anyone is interested in how that all looks
like. Not sure if it is interesting enough for the
tlaplus/examples repository.


------------------- MODULE einstein4 -----------------------

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

VARIABLE
owner,

houses \* 1 -> 2 -> 3 -> 4 -> 5

TypeOK ==
/\ houses \in {1..5}

/\ owner \in [ houses ->
[ color: univ_colors,
pet: univ_pets,
cigar: univ_cigars,
nation: univ_nations,
drink: univ_drinks ]]

------------------------------------------------------------
(* Start with an almost randomly chosen default assignment:*)
Init ==
/\ houses = {1,2,3,4,5}
/\ owner = [ x \in {1,2,3,4,5} |->
IF x = 1 THEN
[ color |-> "red",
pet |-> "bird",
cigar |-> "blend",
nation |-> "norwegian",
drink |-> "beer" ]
ELSE IF x = 2 THEN
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "bm",
nation |-> "swede",
drink |-> "coffee" ]
ELSE IF x = 3 THEN
[ color |-> "blue",
pet |-> "dog",
cigar |-> "dunhill",
nation |-> "dane",
drink |-> "milk" ]
ELSE IF x = 4 THEN
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ]
ELSE
[ color |-> "white",
pet |-> "horse",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ]
]

(* constraints to limit state space *)
Constraint ==
/\ owner[1].nation = "norwegian" \* 9
/\ owner[3].drink = "milk" \* 8

/\ \E h1, h2 \in houses:
/\ h1 # h2
/\ owner[h1].color = "green"
/\ owner[h2].color = "white"

/\ h1 < h2

Swap ==
/\ \E h1, h2 \in {1,2,3,4,5}:
/\ h1 # h2
/\ \/ owner' = [ owner EXCEPT ![h1] = [ @ EXCEPT !.color = owner[h2].color],
![h2] = [ @ EXCEPT !.color = owner[h1].color]]
\/ owner' = [ owner EXCEPT ![h1] = [ @ EXCEPT !.pet = owner[h2].pet],
![h2] = [ @ EXCEPT !.pet = owner[h1].pet]]
\/ owner' = [ owner EXCEPT ![h1] = [ @ EXCEPT !.cigar = owner[h2].cigar],
![h2] = [ @ EXCEPT !.cigar = owner[h1].cigar]]
\/ owner' = [ owner EXCEPT ![h1] = [ @ EXCEPT !.nation = owner[h2].nation],
![h2] = [ @ EXCEPT !.nation = owner[h1].nation]]
\/ owner' = [ owner EXCEPT ![h1] = [ @ EXCEPT !.drink = owner[h2].drink],
![h2] = [ @ EXCEPT !.drink = owner[h1].drink]]
/\ UNCHANGED houses

Next == Swap
IsNeighbour(h1, h2) == h1 + 1 = h2 \/ h1 - 1 = h2

------------------------------------------------------------
Solution ==

/\ \E h \in houses: owner[h].color = "red" /\ owner[h].nation = "brit"
/\ \E h \in houses: owner[h].nation = "swede" /\ owner[h].pet = "dog"

/\ \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" /\ h2 - 1 = h1

/\ \E h \in houses: owner[h].color = "green" /\ owner[h].drink = "coffee"
/\ \E h \in houses: owner[h].cigar = "pm" /\ owner[h].pet = "bird"

/\ \E h \in houses: owner[h].color = "yellow" /\ owner[h].cigar = "dunhill"

/\ \E h1, h2 \in houses:
/\ h1 # h2
/\ owner[h1].cigar = "blend"

/\ owner[h2].pet = "cat" /\ IsNeighbour(h2, h1)

/\ \E h1, h2 \in houses:
/\ h1 # h2
/\ owner[h1].pet = "horse"

/\ owner[h2].cigar = "dunhill"

/\ IsNeighbour(h2, h1)

/\ \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"

/\ IsNeighbour(h2, h1)

/\ \E h1, h2 \in houses:

owner[h1].cigar = "blend" /\ owner[h2].drink = "water" /\ IsNeighbour(h1, h2)

FindSolution == \neg(Solution)
------------------------------------------------------------
============================================================



--8<---------------cut here---------------start------------->8---
CONSTANTS
univ_colors = {"red" , "white" , "blue" , "green" , "yellow" }

univ_pets = {"bird" , "cat" , "dog" , "fish" , "horse" }

univ_cigars = {"blend", "bm" , "dunhill", "pm" , "prince" }

univ_drinks = {"beer" , "coffee", "milk" , "tea" , "water" }

univ_nations = {"brit" , "swede" , "dane" , "norwegian", "german" }

INVARIANT TypeOK
INVARIANT FindSolution
CONSTRAINT Constraint

INIT Init
NEXT Next
--8<---------------cut here---------------end--------------->8---



TLC trace of the solution:

--8<---------------cut here---------------start------------->8---
Error: Invariant FindSolution is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "bird",
cigar |-> "blend",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "bm",
nation |-> "swede",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "dunhill",
nation |-> "dane",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "horse",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 2: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "bird",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "blend",
nation |-> "swede",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "dunhill",
nation |-> "dane",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "horse",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 3: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "blend",
nation |-> "swede",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "dunhill",
nation |-> "dane",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 4: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "swede",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "dane",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 5: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "dane",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 6: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "brit",
drink |-> "coffee" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "dane",
drink |-> "tea" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 7: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "pm",
nation |-> "dane",
drink |-> "coffee" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "prince",
nation |-> "german",
drink |-> "water" ] >>

State 8: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "brit",
drink |-> "tea" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "prince",
nation |-> "dane",
drink |-> "coffee" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "pm",
nation |-> "german",
drink |-> "water" ] >>

State 9: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "brit",
drink |-> "water" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "prince",
nation |-> "dane",
drink |-> "coffee" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "pm",
nation |-> "german",
drink |-> "tea" ] >>

State 10: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "norwegian",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "brit",
drink |-> "water" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "prince",
nation |-> "german",
drink |-> "coffee" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "pm",
nation |-> "dane",
drink |-> "tea" ] >>

State 11: <Swap line 134, col 3 to line 146, col 21 of module einstein4>
/\ houses = {1, 2, 3, 4, 5}
/\ owner = << [ color |-> "red",
pet |-> "horse",
cigar |-> "bm",
nation |-> "brit",
drink |-> "beer" ],
[ color |-> "yellow",
pet |-> "cat",
cigar |-> "dunhill",
nation |-> "norwegian",
drink |-> "water" ],
[ color |-> "blue",
pet |-> "dog",
cigar |-> "blend",
nation |-> "swede",
drink |-> "milk" ],
[ color |-> "green",
pet |-> "fish",
cigar |-> "prince",
nation |-> "german",
drink |-> "coffee" ],
[ color |-> "white",
pet |-> "bird",
cigar |-> "pm",
nation |-> "dane",
drink |-> "tea" ] >>
4465456701 states generated, 100524188 distinct states found, 55869621 states left on queue.
The depth of the complete state graph search is 11.
The average outdegree of the complete state graph is 2 (minimum is 0, the maximum 31 and the 95th percentile is 7).
Checkpointing of run states/21-03-05-10-40-23
Checkpointing completed at (2021-03-05 17:39:20)
Finished in 06h 58min at (2021-03-05 17:39:20)
--8<---------------cut here---------------end--------------->8---


Christian

[Isaac DeFrain]

Hey Christian,

The nice thing about the brute force approach is that you don't even have to define any actions (I used Next == FALSE to disable Next actions, there is probably a better way). The most natural way for me to think about the problem was to simply define the FindSolution predicate, enumerate all possible (initial) states, and wait for TLC to give the expected counterexample.

I made all simplifications I could think of, including making each of the variables a 5-tuple and treating the first entry of each tuple as the attributes of the first house, second entries for the second house, etc. TLC ultimately enumerated 134217728 initial states (maybe you can do better, but this pretty good IMO) and took 53min 34s on a server using 4096 workers on 64 cores with 27305MB heap and 64MB offheap memory (Linux 5.3.0-26-generic amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet, DiskStateQueue). (I'm not sure what MSBDiskFPSet and DiskStateQueue mean, maybe someone can say a few words about these?)

I have my solution posted on my GitHub https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle (if you want to take a peek, but I don't want to discourage you from trying your own ideas) and I'll be making a pull request to add it to the TLA+ Examples https://github.com/tlaplus/Examples in the next few days.

I hope this helps a little!

Best,

Isaac DeFrain

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87pn0c7mbc.fsf%40x230a3.onfire.org.

[Christian Barthel]

Hi Isaac,

thanks for sharing your solution as well.

Isaac DeFrain <isaacd...@gmail.com> writes:

> Hey Christian,
>
> The nice thing about the brute force approach is that you don't even have

> to define any actions (I used *Next == FALSE* to disable Next actions,

> there is probably a better way). The most natural way for me to think about

> the problem was to simply define the *FindSolution *predicate, enumerate

> all possible (initial) states, and wait for TLC to give the expected
> counterexample.

Yes, that looks like a very reasonable choice as well. I think I
already was in the mindset where I thought "I need actions".
Anyway, I think it is good to see different approaches and how to
describe them with TLA+.

> I made all simplifications I could think of, including making each of the
> variables a 5-tuple and treating the first entry of each tuple as the
> attributes of the first house, second entries for the second house, etc.
> TLC ultimately enumerated 134217728 initial states (maybe you can do
> better, but this pretty good IMO) and took 53min 34s on a server using 4096
> workers on 64 cores with 27305MB heap and 64MB offheap memory (Linux
> 5.3.0-26-generic amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet,
> DiskStateQueue). (I'm not sure what MSBDiskFPSet and DiskStateQueue mean,
> maybe someone can say a few words about these?)

I'd be interested in those numbers as well.
Mine took almost 7 hours (as can be seen by the log/trace) on a 2
Core, 4 GB RAM machine virtual machine (Linux/Ubuntu).

[..]

>> 4465456701 states generated, 100524188 distinct states found, 55869621

I guess that the inital states are all distinct states. The
ballpark figure seems to be roughly the same as your number on
initial states (134217728).

--
Christian Barthel <b...@online.de>

[Michael Leuschel]

Hi Isaac,

I had a quick look at the example on https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle  and tried to add the Solution predicate to Init and the Invariant (to see if ProB could initialise the spec and solve it at the same time).

It did not find a solution.

I think this

GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i] = “white"

 has to  be:

GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i+1] = “white"

After that, I was able to load and solve the Puzzle pretty quickly (< 5 ms to find solution). I haven’t check the solution though.

(I realized that ProB does not like [][FALSE]_ in your spec; I will try and fix this.)

Greetings,

Michael

[Markus Kuppe]

FWIW: https://github.com/tlaplus/Examples/pull/31

M.

[Isaac DeFrain]

Thanks, Michael and Markus!

Best,

Isaac DeFrain

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/049e2380-ce00-3864-1135-e8bf1a1cd40b%40lemmster.de.

[Michael Leuschel]

Hi Markus,

> On 11 Mar 2021, at 16:47, Markus Kuppe <tlaplus-go...@lemmster.de> wrote:
>
>
> FWIW: https://github.com/tlaplus/Examples/pull/31

Thanks for the link.

For illustration purposes I have created a very small visualisation and some instructions on how to run the symbolic invariant check here:
https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples/-/tree/master/Einstein

Maybe somebody finds it useful.
There is also an Alloy version.

Greetings,
Michael