Home

Awesome

Community Repository

This is an open repository dedicated to contributions from the TLA+ community. Here you can 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.)

The Modules

NameShort descriptionModule Override?Contributors
BagsExt.tlaAdditional operators on bags (e.g. BagAdd, BagRemove, FoldBag, etc.)@muenchnerkindl, @lemmy
Bitwise.tlaBitwise And and shift-right.@lemmy, @pfeodrippe
Combinatorics.tlaBinomial coefficient (N choose K) and factorial operator@lemmy
CSV.tlaOperations on CSV files@lemmy
DifferentialEquations.tlasee page 178 of Specifying SystemsLeslie Lamport
DyadicRationals.tlaOperations on dyadic rational numbers@lemmy
FiniteSetsExt.tlaAdditional operators on finite sets (e.g. FoldSet, Min, Max, Quantify, etc.)@hwayne, @lemmy, @quicquid, @mryndzionek, @will62794, @konnov
Folds.tlaBasic Fold operator (MapThenFoldSet).@quicquid, @muenchnerkindl, @konnov
Functions.tlaNotions about functions (range, anti-function, injection, surjection, bijection) and folds (FoldFunction, FoldFunctionOnSet).Thomas L. Rodeheffer, @muenchnerkindl, @quicquid, @lemmy
Graphs.tlaCommon operators on directed and undirected graphsLeslie Lamport, @lemmy, @muenchnerkindl
GraphViz.tlaGenerate GraphViz file through TLC@lemmy
HTML.tlaFormat strings into HTML tags@afonsof
IOUtils.tlaInput/Output of TLA+ values & Spawn system commands from a spec.@lemmy, @lvanengelen, @afonsof
Json.tlaJSON serialization and deserialization into TLA+ values.@kuujo, @lemmy, @jobvs, @pfeodrippe
Relation.tlaBasic operations on relations, represented as binary Boolean functions over some set S.@muenchnerkindl, @lemmy
SequencesExt.tlaAdditional operators on sequences (e.g. ToSet, Reverse, ReplaceAll, SelectInSeq, etc.)@muenchnerkindl, @lemmy, @hwayne, @quicquid, @konnov, @afonsof
ShiViz.tlaVisualize error-traces of multi-process PlusCal algorithms with an Interactive Communication Graphs.@lemmy
Statistics.tlaStatistics operators (ChiSquare, etc.)@lemmy
SVG.tlasee will62794/tlaplus_animation@will62794, @lemmy
TLCExt.tlaAssertion operators and experimental TLC features (now part of TLC).@lemmy, @will62794
VectorClocks.tlaCausal order operations on vector clocks (e.g. CausalOrder, IsCausalOrder)@lemmy

How to use it

You must be running Java 9 or higher.

Just copy & paste the snippet, the operators, or the set of modules you are interested in.

Alternatively, clone this repository and pass -DTLA-Library=/path/to/CommunityModules/modules when running TLC.

Another option is to download a library archive and add it to TLC's or the Toolbox's TLA+ library path. The advantage of doing this is that TLC will evaluate an operator faster if the operator comes with a Java implementation (see e.g. SequencesExt.Java). The latest release is at the stable URL https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar.

If you are using the Toolbox, add the library archive under File > Preferences > TLA+ Preferences > TLA+ library path locations. Screencast how to install the CommunityModules into the TLA+ Toolbox

If you are using the VS Code extension, a recent version of the community modules is bundled with the nightly build. If you are not using the nightly build or need to use another version, see this.

If you are running TLC via tla2tools.jar, ensure the JAR is on the classpath: either place it next to tla2tools.jar or add it explicitly with java -cp tla2tools.jar:CommunityModules-deps.jar ....

Being a community-driven repository puts the community in charge of checking the validity and correctness of submissions. The maintainers of this repository will try to keep this place in order. Still, we can't guarantee the quality of the modules and, therefore, cannot provide any assistance on eventual malfunctions.

Contributing

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.

If you change an existing module and tests start failing, check all tests that assert (usually AssertError operator) specific error messages, i.e., line numbers and module names. Note that even an unrelated change further up in the file might have changed the line number and could lead to a failing test case.

Test

Run

ant test

Download

CI