PlusCal spec review request

[Yegor Roganov]

Hi,

I’m learning TLA+ and PlusCal by writing a specification for an algorithm that will be used in a production service at my job.

I’m now at a point where I have a working specification that is checked with TLC. The "problem" is that I’m not 100% confident in my specification and the way I wrote it because I didn’t have someone to learn from, only videos and books (which were tremendously helpful).

I would be extremely thankful if someone reviews my PlusCal spec and maybe point out some things that could be written better. My spec looks somewhat too low-level, but I couldn't come up with anything without sacrificing precision.

Also, as the algorithm is concurrent (more below), model checking with high concurrency takes a lot of time.

Is there something I can do to speed up the checking? I know that fewer labels mean fewer total states, but again, I don't think I can remove labels without sacrificing precision.

The algorithm itself is a concurrent modification of Union Find / Disjoint Sets with "backlinks". Underlying key-value storage must support atomic Compare-and-Set operations.

- Input is several "events", each event is associated with one or more nodes.

- Events that are (transitively) connected belong to the same set

- Each set must have a root (representative) node

- Stale roots (nodes that used to be roots) must be remembered and retrievable given a root node

- Events must be retrievable given a root node

I should say that TLA+/PlusCal have been extremely helpful in designing this algorithm, I don't think I'd manage to succeed

without the help of these tools. Also, I don't expect people to spend a lot of time reviewing this, but even a little feedback is greatly appreciated.

The spec can be seen on GitHub. 

Thank you!