Re: [tlaplus] TLA+ Specification for Einsteins Riddle

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.