[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ Specification for Einsteins Riddle
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.