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.