Added TLC models for all viable specs

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities

Other

1.29k stars 200 forks source link

Added TLC models for all viable specs #110

Closed ahelwer closed 9 months ago

ahelwer commented 10 months ago

WIP Models added for:

TeachingConcurrency
Stones
Bakery-Boulangerie (ref #109)
LoopInvariance
bcastByz
sums_even
TwoPhase
lamport_mutex
Paxos (How to Win a Turing Award)
Chang-Roberts
Aynchronous Byzantine Consensus
Folklore Reliable Broadcast
Bosco Consensus
Consensus in 1 Communication Step
One-Step Consensus with Zero Degradation
Failure Detector
Bunch of others

Closes #107

lemmy commented 9 months ago

Doesn't the last commit make it impossible for Toolbox users to import the models? According to our community survey, about half of our users use the Toolbox.

ahelwer commented 9 months ago

What files do the toolbox users need to import a model? I had added the missing modules in the toolbox model style in a previous commit, but all the duplicated modules were messing with the lists of modules to skip proof testing on.

lemmy commented 9 months ago

The 3Values model for a Consensus spec would need the following three files:

Consensus.toolbox/.project Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs Consensus.toolbox/Consensus___3Values.launch

ahelwer commented 9 months ago

So the copied .tla files and MC.tla/.cfg files don't need to be present in the Consensus.toolbox/3Values directory?

lemmy commented 9 months ago

IIRC, the Toolbox will copy them from the spec's root folder.