Examples/specifications/braf at master · tlaplus/Examples

Name	Name	Last commit message	Last commit date
parent directory ..
BufferedRandomAccessFile.cfg	BufferedRandomAccessFile.cfg
BufferedRandomAccessFile.tla	BufferedRandomAccessFile.tla
README.md	README.md
manifest.json	manifest.json

Name

Last commit message

Last commit date

BufferedRandomAccessFile.tla

Specification of BufferedRandomAccessFile.java, a caching layer that TLC uses to speed up interaction with the filesystem.

Copied from the TLA⁺ source code on 2024/6/14.