Specifications for all Generic Multicast algorithms proposed by Antunes. Once available, the article will be added for reference.
The project follows a fixed structure, where we do what Lamport tells us not to do. We share TLA+ components between specifications, each is in its folder, and each folder must have only a single TLA file. We use Make to execute TLC. If a folder contains multiple configuration files, TLC will run with all of them.
At a higher level are the communication primitives, functionalities shared by the algorithms, and the algorithms per se. The algorithms have specifications written for each of the properties. The properties are verified individually using different conflict relations. By default, each property uses the following conflict relations:
- Always Conflict: deliver messages in a total order;
- Never Conflict: deliver messages in any order;
- Id Conflict: deliver messages in a partial order;