This is an open repository dedicated to contributions from the TLA+ commmunity. Here you are able to submit the snippets, operators, and modules that you wrote for your specifications and that you want to share with the rest of the TLA+ community.
(For us to gauge demand, please star (eyes up and right) this repository if you use the CommunityModules.)
| Name | Short description | Module Override? | Contributors |
|---|---|---|---|
| Functions.tla | Notions about functions including injection, surjection, and bijection. | @muenchnerkindl | |
| Graphs.tla | Common operators on directed and undirected graphs. | Leslie Lamport | |
| SequencesExt.tla | Various operators to manipulate sequences. | ✔ | @muenchnerkindl,@lemmy, @hwayne |
| Relation.tla | Basic operations on relations, represented as binary Boolean functions over some set S. | @muenchnerkindl | |
| FiniteSetsExt.tla | An Operator to do folds without having to use RECURSIVE. | ✔ | @hwayne,@lemmy |
| Bitwise.tla | Bitwise And and shift-right. | ✔ | @lemmy,@pfeodrippe |
| DifferentialEquations.tla | see page 178ff of Specifying Systems | Leslie Lamport | |
| Json.tla | Print TLA+ values as JSON values. | ✔ | @kuujo |
| SVG.tla | see https://github.com/will62794/tlaplus_animation | ✔ | @will62794, @lemmy |
| ShiViz.tla | Visualize error-traces of multi-process PlusCal algorithms with an Interactive Communication Graphs. | @lemmy | |
| TLCExt.tla | Assertion operators and experimental TLC features. | ✔ | @lemmy, @will62794 |
| IOUtils.tla | Input/Output of TLA+ values & Spawn system commands from a spec. | ✔ | @lemmy, @lvanengelen |
Just copy & paste the snippet, the operators or the set of modules you are interested in.
Alternatively, you can download a library archive and add it to TLC's or the Toolbox's TLA+ library path. The advantage of the library archive is that TLC will evaluate an operator faster if the operator comes with a (Java) implementation (see e.g. SequencesExt.Java). Run TLC with -DTLA-Library=/path/to/lib/archive or add the library archive to the Toolbox (File > Preferences > TLA+ Preferences > TLA+ library path locations). The latest release is at the stable URL https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules.jar.
Being a community-driven repository puts the community in charge to check the validity and correctness of submissions. The maintainers of this repository will try to keep this place in order, but we can't guarantee the quality of the modules and therefore cannot provide any assistance on eventual malfunctions.
If you have one or more snippets, operators, or modules you'd like to share, please open an issue or create a pull request. Before submitting your operator or module, please consider adding documentation. The more documentation there is, the more likely it is that someone will find it useful.
