You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+22-16Lines changed: 22 additions & 16 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -10,22 +10,28 @@ The Modules
10
10
-----------
11
11
12
12
| Name | Short description | Module Override? | Contributors |
13
-
| :--: | ---- | ---- | ---- |
14
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/Functions.tla">Functions.tla</a> | Notions about functions including injection, surjection, and bijection. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Functions.java)|[@muenchnerkindl](https://github.com/muenchnerkindl), [@quicquid](https://github.com/quicquid),[@lemmy](https://github.com/lemmy)|
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla">Graphs.tla</a> | Common operators on directed and undirected graphs. || Leslie Lamport, [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl)|
17
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla">SequencesExt.tla</a> | Various operators to manipulate sequences. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SequencesExt.java)|[@muenchnerkindl](https://github.com/muenchnerkindl),[@lemmy](https://github.com/lemmy), [@hwayne](https://github.com/hwayne), [@quicquid](https://github.com/quicquid)|
18
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla">Relation.tla</a> | Basic operations on relations, represented as binary Boolean functions over some set S.||[@muenchnerkindl](https://github.com/muenchnerkindl)|
19
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt.tla">FiniteSetsExt.tla</a> | An Operator to do folds without having to use RECURSIVE. |✔|[@hwayne](https://github.com/hwayne),[@lemmy](https://github.com/lemmy), [@quicquid](https://github.com/quicquid)|
20
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla">Bitwise.tla</a> | Bitwise And and shift-right. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Bitwise.java)|[@lemmy](https://github.com/lemmy),[@pfeodrippe](https://github.com/pfeodrippe)|
21
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/DifferentialEquations.tla">DifferentialEquations.tla</a> | see page 178ff of [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf)|| Leslie Lamport |
22
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla">Json.tla</a> | Print TLA+ values as JSON values. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Json.java)|[@kuujo](https://github.com/kuujo)|
23
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/SVG.tla">SVG.tla</a> | see https://github.com/will62794/tlaplus_animation|[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SVG.java)|[@will62794](https://github.com/will62794), [@lemmy](https://github.com/lemmy)|
24
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla">ShiViz.tla</a> | Visualize error-traces of multi-process PlusCal algorithms with an [Interactive Communication Graphs](https://bestchai.bitbucket.io/shiviz/). ||[@lemmy](https://github.com/lemmy)|
25
-
| <ahref="https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLCExt.tla">TLCExt.tla</a> | Assertion operators and experimental TLC features (now part of TLC). |[✔](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java)|[@lemmy](https://github.com/lemmy), [@will62794](https://github.com/will62794)|
26
-
| <ahref="https://github.com/tlaplus/CommunityModules/blob/master/modules/IOUtils.tla">IOUtils.tla</a> | Input/Output of TLA+ values & Spawn system commands from a spec. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/IOUtils.java)|[@lemmy](https://github.com/lemmy), [@lvanengelen](https://github.com/lvanengelen)|
|[`Bitwise.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla)| Bitwise And and shift-right. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Bitwise.java)|[@lemmy](https://github.com/lemmy), [@pfeodrippe](https://github.com/pfeodrippe)|
16
+
|[`Combinatorics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Combinatorics.tla)| Binomial coefficient (N choose K) and factorial operator |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Combinatorics.java)|[@lemmy](https://github.com/lemmy)|
17
+
|[`CSV.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CSV.tla)| Operations on CSV files |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CSV.java)|[@lemmy](https://github.com/lemmy)|
18
+
|[`DifferentialEquations.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/DifferentialEquations.tla)| see page 178 of [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf)|| Leslie Lamport |
19
+
|[`DyadicRationals.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/DyadicRationals.tla)| Operations on [dyadic rational numbers](https://en.wikipedia.org/wiki/Dyadic_rational)|[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/DyadicRationals.java)|[@lemmy](https://github.com/lemmy)|
|[`Functions.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Functions.tla)| Notions about functions (range, anti-function, injection, surjection, bijection) and folds (`FoldFunction`, `FoldFunctionOnSet`). |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Functions.java)| Thomas L. Rodeheffer, [@muenchnerkindl](https://github.com/muenchnerkindl), [@quicquid](https://github.com/quicquid), [@lemmy](https://github.com/lemmy)|
23
+
|[`Graphs.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla)| Common operators on directed and undirected graphs || Leslie Lamport, [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl)|
24
+
|[`GraphViz.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/GraphViz.tla)| Generate GraphViz file through TLC |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/GraphViz.java)|[@lemmy](https://github.com/lemmy)|
25
+
|[`HTML.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/HTML.tla)| Format strings into HTML tags ||[@afonsof](https://github.com/afonsof)|
26
+
|[`IOUtils.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/IOUtils.tla)| Input/Output of TLA+ values & Spawn system commands from a spec. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/IOUtils.java)|[@lemmy](https://github.com/lemmy), [@lvanengelen](https://github.com/lvanengelen), [@afonsof](https://github.com/afonsof)|
27
+
|[`Json.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla)| JSON serialization and deserialization into TLA+ values. |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Json.java)|[@kuujo](https://github.com/kuujo), [@lemmy](https://github.com/lemmy), [@jobvs](https://github.com/jobvs), [@pfeodrippe](https://github.com/pfeodrippe)|
28
+
|[`Relation.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla)| Basic operations on relations, represented as binary Boolean functions over some set S. ||[@muenchnerkindl](https://github.com/muenchnerkindl)|
|[`ShiViz.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla)| Visualize error-traces of multi-process PlusCal algorithms with an [Interactive Communication Graphs](https://bestchai.bitbucket.io/shiviz/). ||[@lemmy](https://github.com/lemmy)|
|[`SVG.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/SVG.tla)| see [will62794/tlaplus_animation](https://github.com/will62794/tlaplus_animation)|[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SVG.java)|[@will62794](https://github.com/will62794), [@lemmy](https://github.com/lemmy)|
33
+
|[`TLCExt.tla`](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLCExt.tla)| Assertion operators and experimental TLC features (now part of TLC). |[✔](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java)|[@lemmy](https://github.com/lemmy), [@will62794](https://github.com/will62794)|
34
+
|[`VectorClocks.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/VectorClocks.tla)| Causal order operations on vector clocks (e.g. `CausalOrder`, `IsCausalOrder`) |[✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/VectorClocks.java)|[@lemmy](https://github.com/lemmy)|
0 commit comments