tlaplus / CommunityModules

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

Fix the order of the arguments in ReduceSet #76

Closed konnov closed 2 years ago

konnov commented 2 years ago

As we have just found with the new version of Apalache type checker, ReduceSet in FiniteSetsExt has the wrong order of arguments: https://github.com/informalsystems/apalache/pull/2109. Perhaps, it was introduced during refactoring.

Here is the one-line fix.

lemmy commented 2 years ago

LGTM, can you add the following basic test to the PR?

diff --git a/tests/FiniteSetsExtTests.tla b/tests/FiniteSetsExtTests.tla
index 5a9481a..5ad9135 100644
--- a/tests/FiniteSetsExtTests.tla
+++ b/tests/FiniteSetsExtTests.tla
@@ -122,6 +122,8 @@ ASSUME SymDiff({2,3}, {2,3,4}) = {4}
 ASSUME SumSet(1..3) = 6
 ASSUME ProductSet(1..4) = 24

+ASSUME ReduceSet(+, 1..5, 42) = 57
+
 -----------------------------------------------------------------------------

 (* TLC won't evaluate the assumes above if a there is no behavior *)
konnov commented 2 years ago

Good point. Just added the test.

lemmy commented 2 years ago

ReduceSet should probably be removed eventually.