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

Add BufferedRandomAccessFile spec #145

Merged
merged 3 commits into from
Jun 20, 2024
Merged

Add BufferedRandomAccessFile spec #145

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
23e961d
Add BufferedRandomAccessFile spec
Calvin-L Jun 14, 2024
f3410da
Add liveness tag to BRAF manifest entry
Calvin-L Jun 14, 2024
4fb4032
Fix expected runtime (format is HH:MM:SS)
Calvin-L Jun 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ Here is a list of specs included in this repository, with links to the relevant
| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | |
| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | |
| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | |
| [Buffered Random Access File](specifications/braf) | Calvin Loncaric | | | | ✔ | |

## Examples Elsewhere
Here is a list of specs stored in locations outside this repository, including submodules.
Expand Down
33 changes: 33 additions & 0 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3415,6 +3415,39 @@
}
]
},
{
"path": "specifications/braf",
"title": "Buffered Random Access File",
"description": "Specification of a Java file caching layer",
"sources": ["https://github.com/tlaplus/tlaplus/tree/4613109641676389d97b8df209d6cf4d90d31c1c/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.tla"],
"authors": ["Calvin Loncaric"],
"tags": [],
"modules": [
{
"path": "specifications/braf/BufferedRandomAccessFile.tla",
"communityDependencies": [],
"tlaLanguageVersion": 2,
"features": [],
"models": [
{
"path": "specifications/braf/BufferedRandomAccessFile.cfg",
"runtime": "00:09:00",
Calvin-L marked this conversation as resolved.
Show resolved Hide resolved
"size": "small",
"mode": "exhaustive search",
"features": [
"alias",
"symmetry",
"liveness"
],
"result": "success",
"distinctStates": 3316,
"totalStates": 128581,
"stateDepth": 10
}
]
}
]
},
{
"path": "specifications/byihive",
"title": "RFC 3506: Voucher Transaction System",
Expand Down
24 changes: 24 additions & 0 deletions specifications/braf/BufferedRandomAccessFile.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
SPECIFICATION Spec
CONSTANT Symbols = {A, B}
CONSTANT ArbitrarySymbol = ArbitrarySymbol
CONSTANT MaxOffset = 3
CONSTANT BuffSz = 2

SYMMETRY Symmetry
ALIAS Alias

INVARIANT TypeOK
INVARIANT Inv1
\*INVARIANT Inv2 \* see note at definition of Inv2
PROPERTY Inv2CanAlwaysBeRestored
INVARIANT Inv3
INVARIANT Inv4
INVARIANT Inv5
PROPERTY Safety
PROPERTY FlushBufferCorrect
PROPERTY SeekCorrect
PROPERTY SeekEstablishesInv2
PROPERTY Write1Correct
PROPERTY Read1Correct
PROPERTY WriteAtMostCorrect
PROPERTY ReadCorrect
Loading