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

Re: [tlaplus] TLA+ Specification for Einsteins Riddle



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


On Sat, Mar 6, 2021 at 12:56 AM Christian Barthel <bch@xxxxxxxxx> wrote:
Hillel Wayne <hwayne@xxxxxxxxx> 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

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

--
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/CAM3xQxH0xATFyk6Rg%2Bkdxr9J6%3D1e3Sf_NVXyv4hjdpzqLjxTOA%40mail.gmail.com.