Help with Advent of Code day 01

39 views
Skip to first unread message

migu...@ciencias.unam.mx

unread,
Dec 9, 2020, 1:19:12 AM12/9/20
to tlaplus

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

unread,
Dec 9, 2020, 2:23:06 PM12/9/20
to tla...@googlegroups.com
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

unread,
Dec 9, 2020, 2:41:24 PM12/9/20
to tlaplus
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

unread,
Dec 9, 2020, 2:45:11 PM12/9/20
to tlaplus
The second repo is very useful as well, thank you Markus!

Arnaud Bos

unread,
Dec 9, 2020, 7:20:51 PM12/9/20
to tlaplus
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+.

Reply all
Reply to author
Forward
0 new messages