FazBrowse GitHub Viewer | Trending |
URL:
| Home
Tools: [Download Repo ZIP]   [Original HTTPS Page]

Add BufferedRandomAccessFile spec by Calvin-L · Pull Request #145 · tlaplus/Examples · GitHub

/ Examples Public

Add BufferedRandomAccessFile spec - #145

Merged
ahelwer merged 3 commits into
tlaplus:masterfrom
Calvin-L:bufferedrandomaccessfile
Jun 20, 2024
ConversationCommits (3)ChecksFiles changed
Merged

Add BufferedRandomAccessFile spec#145
ahelwer merged 3 commits into
tlaplus:masterfrom
Calvin-L:bufferedrandomaccessfile

Conversation

Calvin-L commented Jun 14, 2024 •
edited
Loading

Copy link
Copy Markdown
Contributor

In review, @lemmy suggested adding this spec to our examples: tlaplus/tlaplus#907 (comment)

I made two small changes:

  1. Pull config out into a separate file
  2. Reduce MaxOffset from 4 to 3 so it can be checked in <10s (er, on my 8-core laptop anyway)

Add BufferedRandomAccessFile spec
23e961d 
Signed-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>

lemmy commented Jun 14, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

Duplication of the specification, both here and in the tlaplus/tlaplus repository, likely won't be an issue. However, it's important to note that the OpenAddressing.tla specification in the tlaplus/tlaplus repository is only referenced here, not duplicated.

Consider adding a comment to the spec in tlaplus/tlaplus that points to the copy here.

Add liveness tag to BRAF manifest entry
f3410da 
This tag isn't quite correct; the spec checks _action_ properties, not
full liveness properties.  But it is true that the spec uses the `[]`
operator and the config file uses the `PROPERTY` keyword.

Signed-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>

ahelwer commented Jun 16, 2024 •
edited
Loading

Copy link
Copy Markdown
Collaborator

This is very weird. CI has SANY output the following error:

ERROR:root:java -cp deps/tools/tla2tools.jar:deps/apalache/lib/apalache.jar:specifications/Bakery-Boulangerie:deps/community/modules.jar:deps/tlapm/library tla2sany.SANY -error-codes specifications/Bakery-Boulangerie/MCBakery.tla
Illegal switch: -error-codes

Will investigate.

ahelwer reviewed Jun 16, 2024
View reviewed changes
Comment thread manifest.json Outdated
Fix expected runtime (format is HH:MM:SS)
4fb4032 
Signed-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>
Calvin-L force-pushed the bufferedrandomaccessfile branch from 563b1a0 to 4fb4032 Compare June 20, 2024 21:18
ahelwer merged commit a58b556 into tlaplus:master Jun 20, 2024
Calvin-L deleted the bufferedrandomaccessfile branch June 21, 2024 05:14
lemmy mentioned this pull request Aug 22, 2026
Open
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
Show hidden characters
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

ahelwer ahelwer left review comments

Assignees

No one assigned

Labels

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

Back | FazBrowse Home | New Git URL