[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Help with Advent of Code day 01
Hello,
As Markus said, Thomas' repo and mine are written in TLA+, but if you have specific questions we'd be happy to answer.
We had a quick Zoom meeting the other day and it was fun to talk and compare our solutions.
About your module:
First, I'd advise you reconsider the x \in Input bit. As Input is a sequence and not a set, it can't work.
Second, using a while ... end while; around your with blocks will translate into a much more readable TLA+, which you
can inspect to get more insight on what it is you are actually writing.
Third, here you are trying to find the pair of integers x and y such that x + y = Sum, but your assertion is written in a way
which will halt TLC for any other pair. It will fail on the first state it explores right after the initial state. Unless it stumbles
upon that pair on the first attempt, it's never going to get to the solution.
In Advent Of Code, you're playing TLC as a problem solver rather than a checker: try to write invariants opposite of what
you'd want in a real specification.
Lastly, I'd avoid assert, because if you actually find the solution, you will not see which x and y make the solution, just
an assertion failure message.
I got bored when I saw the problem statements of days 4 and 5 and all the parsing involved. The recursive operators I
originally wrote for parsing day 2 and 3 inputs didn't satisfy me at all.
So I got sidetracked and implemented custom modules for parsing which I've just got working [1] (caution, it's Clojure code).With that it's possible that I'll find motivation for the other exercises.
Thomas went further if you're interested in solutions for days 4+.
[1] https://github.com/arnaudbos/aoc2020-tla-plus/tree/master/aoc2020-tla-plus
On Wednesday, December 9, 2020 at 8:45:11 PM UTC+1 migu...@xxxxxxxxxxxxxxxx wrote:
The second repo is very useful as well, thank you Markus!
Thanks!
I actually took most of the code from the first repo, ran it locally and was pleased, then tried implementing the PlusCal version.
On Wednesday, 9 December 2020 at 13:23:06 UTC-6 Markus Alexander Kuppe wrote:
On 08.12.20 22:19, migu...@xxxxxxxxxxxxxxxx wrote:
>
> Hello all!
> This is my first attempt at seriuosly using PlusCal, and I'm trying to
> solve some small problems to warm up. I tried solving the first Advent
> of Code problem, but my PlusCal is quite rough.
> Any help ?
> The problem is, given a list, find 2 numbers that sum to 2020.
>
>
> ---- MODULE pcal ----
> EXTENDS TLC, Integers, FiniteSets, Sequences
>
> (*--algorithm pcal
> variables
> Sum = 2020,
> Input = <<
> 1511,
> 1112,
> 1958,
> 1778,
> 1769,
> 1946,
> 1800,
> 1911,
> 1821,
> 1886,
> 285,
> 1649,
> 1952,
> 1428,
> 1779,
> 1822,
> 1735
>>>;
>
> begin
> with x \in Input do
> with y \in Input \ {x} do
> assert x + y = Sum;
> end with;
> end with; end algorithm; *)
Hi,
although TLA+ and not PlusCal, it perhaps helps to study the solutions
of Arnaud Bos [1] and Thomas Bracher [2].
Markus
[1] https://github.com/arnaudbos/aoc2020-tla-plus/tree/master/day1
[2] https://github.com/sadraskol/advent-2020/blob/main/Advent1.tla
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/db703010-c5a1-44c7-9c14-2ee5090af1a3n%40googlegroups.com.