Markus Alexander Kuppe

Move the module https://github.com/tlaplus/Examples/blob/master/specifications/Huang/DyadicRationals.tla here and add a definition `DyadicRational` (similar to Int, Nat, Reals) with an appropriate (Java) module override. /cc @muenchnerkindl

`Functions.tla` here clashes with `Functions.tla` in TLAPM

6

There is a name clash between the `Functions.tla` in CommunityModules and `Functions.tla` in TLAPM, with the `Functions.tla` in CommunityModules (`CM!Functions.tla`) having a superset of operators compared to the version in...

Add PlusPy's `Messaging.tla`

1

PlusPy introduces a (generic) [Messaging module](https://github.com/tlaplus/PlusPy/blob/master/modules/lib/Messaging.tla) that we should move to the CommunityModules. /cc @johnyf

Most animations have an area where they show a table/grid that contains multiple Texts. The SVG module should have a definition for high-level Grid/Tables.

Consider bundling CommunityModules.jar as part of a TLC release

6

https://github.com/dgpv/bip32_template_parse_tplaplus_spec/issues/1 shows that users are reluctant to adopt CM because it adds an additional dependency. Thus, we should consider bundling/shipping a snapshot of CM with new TLC releases. Requirements: *...

SVG!Group expects *sequence* of elements

2

https://github.com/tlaplus/CommunityModules/blob/dd647242998a8694846a17874344bf7299c43f56/modules/SVG.tla#L96-L98 What is the meaning of the order given by the sequence? Is it the z coordinate of the svg?

Add benchmarks for the explicit-state model checker TLC

15

The model checker (https://github.com/tlaplus/tlaplus) is optimized for throughput and has a single hot path. I can come up with benchmarks for a) scalability and b) throughput. One is a spec...

``` TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened....

Process Picker broken when JVM binds to random port

1

When port conflicts occur, a user may choose to let the JVM bind to a random port by omitting the [`address` attribute] (https://docs.oracle.com/cd/E19501-01/819-3664/abgdm/index.html) or by passing `address=0` as command-line arguments....

Hi Dan, I added a reference to this repository in https://github.com/lemmy/lets-prove-blocking-queue because they are similar in spirit. Since you mention left-pad, perhaps you might also want to link to https://github.com/lemmy/lets-prove-blocking-queue....