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

*From*: Arnaud Bos <mail@xxxxxxxxxxxxx>*Date*: Wed, 9 Dec 2020 16:20:50 -0800 (PST)*References*: <fa41ccee-b829-4bca-8b48-23a71d863bc2n@googlegroups.com> <5c8c328b-6e44-fc55-4d56-c0afe5cd5f0f@lemmster.de> <401c19db-f162-4683-9baa-52754055eb5en@googlegroups.com> <d25239ae-52cb-4bdd-be17-2802b2d8d71fn@googlegroups.com>

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.

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!On Wednesday, 9 December 2020 at 13:41:24 UTC-6 migu...@xxxxxxxxxxxxxxxx wrote: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.

**References**:**[tlaplus] Help with Advent of Code day 01***From:*migu...@xxxxxxxxxxxxxxxx

**Re: [tlaplus] Help with Advent of Code day 01***From:*Markus Kuppe

**Re: [tlaplus] Help with Advent of Code day 01***From:*migu...@xxxxxxxxxxxxxxxx

**Re: [tlaplus] Help with Advent of Code day 01***From:*migu...@xxxxxxxxxxxxxxxx

- Prev by Date:
**[tlaplus] Approaching repeated assignment in PlusCal** - Next by Date:
**Re: [tlaplus] Does WF and SF statements applicable in distributed Mode?** - Previous by thread:
**Re: [tlaplus] Help with Advent of Code day 01** - Next by thread:
**[tlaplus] Does WF and SF statements applicable in distributed Mode?** - Index(es):