TLA+ Specs of TLA+ Tools like TLC, TLaTeX, etc.

[Chris Ortiz]

Hi TLA+ Community,

Good morning. I would like to know if there are TLA+ Specs of the TLA+ tool ecosystem out there that we can refer to? Kindly let me know where I can find them if they exist. If not, there should be no reason why we cannot demonstrate writing TLA+ spec for the specification of the software that helps evangalize TLA+.

Thanks, and best regards,

Chris (zitro)

[Markus Kuppe]

Hi Chris,

TLC's model checking algorithm (BFS exploration + error-trace construction):
* https://github.com/tlaplus/examples/blob/master/specifications/TLC/TLCMC.tla
* https://github.com/tlaplus/examples/blob/master/specifications/TLC/MCReachability.tla

TLC's off-heap fingerprint set (OffHeapDiskFPSet.java); an in-memory variant was
re-verified independently in https://arxiv.org/abs/2311.14452:
* https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla
* https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.ConcurrentFlusher.tla

TLC's filesystem caching layer, with a refinement proof:
* https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.tla
* https://github.com/tlaplus/examples/blob/master/specifications/braf/BufferedRandomAccessFile.tla

TLC's lazy enumeration order for SUBSET S:
* https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/value/impl/SubsetValue.tla

Multi-core on-the-fly SCC decomposition, the algorithm class behind parallel
liveness checking:
* https://github.com/tlaplus/tlaplus/blob/master/general/performance/Bloemen/BloemenSCC.tla

SANY's level checking, i.e. Specifying Systems 17.2 and the reference comment in
LevelNode.java:
* https://github.com/tlaplus/examples/blob/master/specifications/LevelChecking/LevelSpec.tla

The grammar of TLA+, and of TLC's .cfg files, both written in TLA+:
* https://github.com/tlaplus/examples/blob/master/specifications/SpecifyingSystems/Syntax/TLAPlusGrammar.tla
* https://github.com/tlaplus/examples/blob/master/specifications/SpecifyingSystems/TLC/ConfigFileGrammar.tla

The PlusCal translation step, plus the PlusCal-to-TLA+ location mapping the
Toolbox uses to jump between code and translation:
* https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/pcal/PlusCal.tla
* https://github.com/tlaplus/tlaplus/blob/master/general/docs/TLAToPCal.tla
* https://github.com/tlaplus/tlaplus/blob/master/general/docs/RemoveRedundantParens.tla

How the Toolbox colors proof steps from TLAPM's per-obligation statuses:
* https://github.com/tlaplus/tlaplus/blob/master/general/docs/ProofStatus.tla
* https://github.com/tlaplus/tlaplus/blob/master/general/docs/ColorPredicates.tla

M.

[Chris Ortiz]

Thank you very much Markus. I will take a look at them. These will help me understand those tools better. 

Thanks, and best regards,

Chris (zitro)