Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added TLC models for all viable specs #110

Merged
merged 26 commits into from
Jan 26, 2024
Merged

Added TLC models for all viable specs #110

merged 26 commits into from
Jan 26, 2024

Conversation

ahelwer
Copy link
Collaborator

@ahelwer ahelwer commented Jan 18, 2024 •
edited
Loading

WIP
Models added for:

Closes #107

@lemmy
Copy link
Member

lemmy commented Jan 22, 2024

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
Copy link
Collaborator Author

ahelwer commented Jan 22, 2024

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
Copy link
Member

lemmy commented Jan 23, 2024

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
Copy link
Collaborator Author

ahelwer commented Jan 23, 2024 •
edited
Loading

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

@lemmy
Copy link
Member

lemmy commented Jan 23, 2024

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

@ahelwer
Added model for Folklore Reliable Broadcast
153ebcd 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Re-added Paxos (Turing Award) toolbox setting files
7b8e9b4 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for Bosco consensus
545a1a1 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for c1cs
dd1d486 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for cf1s_folklore
e46331b 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for detector_chan96
2b4386c 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added models for Async Commit specs
41d96ac 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for spanning
30e196e 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added model for disk paxos
197ef75 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added models for TransactionCommit
076b287 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer
Added models for SpanningTree
ccab4d0 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer ahelwer mentioned this pull request Jan 26, 2024
Closed
@ahelwer
Fixed models for SpanningTree
027fd13 
Signed-off-by: Andrew Helwer <[email protected]>
@ahelwer ahelwer mentioned this pull request Jan 26, 2024
Closed
@ahelwer ahelwer marked this pull request as ready for review January 26, 2024 20:47
@ahelwer ahelwer merged commit 45a0205 into tlaplus:master Jan 26, 2024
4 checks passed
@ahelwer ahelwer deleted the add-tlc-models branch January 26, 2024 21:05
lemmy pushed a commit to lemmy/Examples that referenced this pull request Apr 5, 2024
@ahelwer @lemmy
Added TLC models for all viable specs (tlaplus#110)
d3dd8f5 
Signed-off-by: Andrew Helwer <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Add TLC models for all specs for which it's viable
2 participants
@ahelwer @lemmy