Help with Advent of Code day 01

[migu...@ciencias.unam.mx]

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; *)

[Markus Kuppe]

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

[migu...@ciencias.unam.mx]

Thanks!

I actually took most of the code from the first repo, ran it locally and was pleased, then tried implementing the PlusCal version.

[migu...@ciencias.unam.mx]

The second repo is very useful as well, thank you Markus!

[Arnaud Bos]

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