# Alloy Authors - Practical Alloy - Protocol design (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article4.6bc1851654a0.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/51392058) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Alloy Authors]] **Full Title**:: Practical Alloy - Protocol design **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [practicalalloy.github.io](https://practicalalloy.github.io/chapters/protocol-design/index.html) **Host**:: [[practicalalloy.github.io]] **Highlighted**:: [[2025-05-14]] **Created**:: [[2025-05-14]] ## Highlights - Using sets for the mailboxes is an abstraction that allows us to verify that the protocol is correct even if messages are transmitted out of order. ([View Highlight](https://read.readwise.io/read/01jv6b3jvkkvvf9bepmnqsgbs6)) ^889297750 - Note that, on purpose, we did not impose a multiplicity `lone` in this declaration, because that constraint, that at most one node is elected leader, is one of the key assertions we will want to verify to be a consequence of the protocol dynamics, and thus should not be imposed as an assumption upfront. ([View Highlight](https://read.readwise.io/read/01jv6b58cerzxtfzc2csqzgsf4)) ^889297856 - `C implies A else B` is the same as `(C and A) or (not C and B)` ([View Highlight](https://read.readwise.io/read/01jv6ccskca38h8736a3as5f3k)) ^889301472 - `always eventually P` holds in a system if in every state of every trace `P` is later valid, which means that `P` is true infinitely often. ([View Highlight](https://read.readwise.io/read/01jv6cn77y9p5sv5c166axaqht)) ^889301726 Attention the differences with `eventually P` - However, imposing a total order with `util/ordering` will make the scope on `Node` exact, which means that for a given scope we would only verify all configurations with that exact number of nodes. ([View Highlight](https://read.readwise.io/read/01jv6e9bdm8kyg3fyqdmryx8h0)) ^889307147 #caveat - One possible solution to circumvent these issues if we have explicit messages is to enforce a so-called *generator axiom*. These are constraints that force every possible combination of field values of a signature to exist *in every instance*. ([View Highlight](https://read.readwise.io/read/01jv6ehwjbfg8d4kpjnmtggm88)) ^889309420