This shows you the differences between two versions of the page.
| |
| codebase:architecture [2024/09/28 15:58] – created - external edit 127.0.0.1 | codebase:architecture [2025/09/23 01:14] (current) – [Modules] typo: "can by run" => "can be run"; LaTex => LaTeX hfwei |
|---|
| ==== Modules ==== | ==== Modules ==== |
| |
| * [[../src/pcal|pcal]]: Converts the pcal language into TLA+ that can by run by TLC2. | * [[../src/pcal|pcal]]: Converts the pcal language into TLA+ that can be run by TLC2. |
| * [[../src/tla2tex|tla2tex]]: “Pretty Prints” TLA+ code into LaTex. This LaTex can then be used for publishing. | * [[../src/tla2tex|tla2tex]]: “Pretty Prints” TLA+ code into LaTeX. This LaTeX can then be used for publishing. |
| * [[../src/tla2sany|tla2sany]]: Contains the AST and parsing logic for the TLA+ language. The AST classes generated from parsing are used by TLC2. | * [[../src/tla2sany|tla2sany]]: Contains the AST and parsing logic for the TLA+ language. The AST classes generated from parsing are used by TLC2. |
| * [[../src/tlc2|tlc2]]: The model checker to validate the AST generated by tla2sany. This is the largest and most complex part of the codebase by far. | * [[../src/tlc2|tlc2]]: The model checker to validate the AST generated by tla2sany. This is the largest and most complex part of the codebase by far. |
hfwei