search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

Add Fold operators for Bags.tla (in new BagsExt.tla) #64

Closed lemmy closed 2 years ago

lemmy commented 2 years ago

@muenchnerkindl noted that we lack fold operators for the Bags.tla module. @konnov Does Apalache already have folds for bags?

konnov commented 2 years ago

@konnov Does Apalache already have folds for bags?

No, we don't. But I think it should be relatively easy to implement them via FoldFunction.

lemmy commented 2 years ago

@muenchnerkindl added a TLA+ operator definition of BagsExt!FoldBag in https://github.com/tlaplus/CommunityModules/commit/b961f70ef7725b9e30a5457cffe16f90015c0e31. The Java module override for TLC still has to be done.

lemmy commented 2 years ago

The module override of the Functions.tla module should either be immediately applicable like with sequences or at least provide inspiration on how a dedicated module override for BagsExt.tla would look like. For testing Java module overrides, a useful trick is to define the pure TLA+ operator with a different name in the test module and assert equality for the pure and overridden operator for various inputs: https://github.com/tlaplus/CommunityModules/blob/b961f70ef7725b9e30a5457cffe16f90015c0e31/tests/FunctionsTests.tla#L30-L34

For reference, the original module override of the Bags.tla standard module is at https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/module/Bags.java

lemmy commented 2 years ago

https://github.com/tlaplus/CommunityModules/pull/66