This shows you the differences between two versions of the page.
| Next revision | Previous revision |
| codebase:architecture [2024/09/28 15:58] – created - external edit 127.0.0.1 | codebase:architecture [2026/02/07 13:55] (current) – typo: mplified to simplified 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. |
| ==== The Standard Flow ==== | ==== The Standard Flow ==== |
| |
| This is a generalized mplified description of how this code is normally used, and the involved components. More detail will be given on some of these components in the following sections. | This is a generalized simplified description of how this code is normally used, and the involved components. More detail will be given on some of these components in the following sections. |
| |
| - (Optional) PCal code translated into TLA+ code. [[src/pcal/trans.java|pcal.trans]]::main | - (Optional) PCal code translated into TLA+ code. [[src/pcal/trans.java|pcal.trans]]::main |
127.0.0.1