[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:
I had a quick look at the example on
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.)
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.