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
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/08AA8B55-2928-4A00-9E4C-B6ECBC602D04%40gmail.com.