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

[tlaplus] TLA+ Specification for Einsteins Riddle

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 <bch@xxxxxxxxx>

-- 
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/87czwg7zx5.fsf%40x230a3.onfire.org.