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

Re: [tlaplus] TLA+ Specification for Einsteins Riddle



Thanks, Michael and Markus!


Best,

Isaac DeFrain


On Thu, Mar 11, 2021 at 8:47 AM Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
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.

--
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/CAM3xQxFs3aVCBHpCQwLShhKWKfn5itQj48gDEx5Ot5gvmhPsVQ%40mail.gmail.com.