CommunityModules
CommunityModules copied to clipboard
tlaplus
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
- add TLA+ modules for function, record, and sequence of records parsers - add overriding java classes - add examples - add docs Please feel free to change the directory...
`FlattenSet({{1},{2}}) = UNION {{1},{2}}` https://github.com/tlaplus/CommunityModules/blob/e88b5536133eaf0ad68c698d618480c9a84f4192/modules/FiniteSetsExt.tla#L42-L51 @konnov @Kukovec @quicquid
This PR introduces the annotation `@supportedBy("TLC")` or `@supportedBy("TLC,Apalache")` in front of all operators, to document which operators are supported only by TLC and which operators are supported by TLC and...
The companion of https://github.com/tlaplus/tlaplus/pull/716 I think it is best to have potential discussions regarding this PR over there.
https://github.com/tlaplus/tlaplus/commit/1eb815620dedc696a5a637944853129595c47216#diff-364040e3b4487febdb3378d1e3a325421763d819b32c40520360494933a8e263R12 does not work for absolute paths. We should consider adding URI-related operators such as `Dirname`, `Basename`, `Extname`, ...
This would enable division plus floor/ceiling functions, with the following benefits: - Calculate the size of the majority of a set (currently passed in as a constant in the Paxos...
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
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...
I'm unable to run Model checking when I include the `CommunityModules.jar` file. ``` TLC threw an unexpected exception. This was probably caused by an error in the spec or model....
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