[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] PlusCal spec review request
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!
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/79dff532-9d73-446d-a0ea-5865dda922d0n%40googlegroups.com.