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

Re: [tlaplus] TLA+ Specification for Einsteins Riddle



On 10.03.21 23:31, Michael Leuschel wrote:
Hi Isaac,

I had a quick look at the example on https://github.com/Isaac-DeFrain/TLAplusFun/tree/main/EinsteinRiddle <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


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

M.

--
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/049e2380-ce00-3864-1135-e8bf1a1cd40b%40lemmster.de.