Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix the order of the arguments in ReduceSet #76

Merged
merged 2 commits into from
Aug 26, 2022

Conversation

konnov
Copy link
Contributor

@konnov konnov commented Aug 26, 2022

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

Here is the one-line fix.

@konnov konnov requested a review from lemmy August 26, 2022 16:52
@lemmy
Copy link
Member

lemmy commented Aug 26, 2022

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
Copy link
Contributor Author

konnov commented Aug 26, 2022

Good point. Just added the test.

@lemmy lemmy merged commit 9a76515 into tlaplus:master Aug 26, 2022
@lemmy
Copy link
Member

lemmy commented Aug 26, 2022

ReduceSet should probably be removed eventually.

@konnov konnov deleted the igor/bugfix-in-reduce branch August 26, 2022 17:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

2 participants