Skip to content

Added TLC models for all viable specs - #110

Merged
ahelwer merged 26 commits into
tlaplus:masterfrom
ahelwer:add-tlc-models
Jan 26, 2024
Merged

Added TLC models for all viable specs#110
ahelwer merged 26 commits into
tlaplus:masterfrom
ahelwer:add-tlc-models

Conversation

@ahelwer

@ahelwer ahelwer commented Jan 18, 2024

Copy link
Copy Markdown
Collaborator

WIP
Models added for:

Closes #107

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Reverted CRLF newline normalizations

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
@lemmy

lemmy commented Jan 22, 2024

Copy link
Copy Markdown
Member

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.

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
@ahelwer

ahelwer commented Jan 22, 2024

Copy link
Copy Markdown
Collaborator Author

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

lemmy commented Jan 23, 2024

Copy link
Copy Markdown
Member

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

ahelwer commented Jan 23, 2024

Copy link
Copy Markdown
Collaborator Author

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

@lemmy

lemmy commented Jan 23, 2024

Copy link
Copy Markdown
Member

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

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
@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
@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
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

Add TLC models for all specs for which it's viable

2 participants