diff --git a/modules/FiniteSetsExt.tla b/modules/FiniteSetsExt.tla index 7b87b66..1460089 100644 --- a/modules/FiniteSetsExt.tla +++ b/modules/FiniteSetsExt.tla @@ -36,7 +36,7 @@ ReduceSet(op(_, _), set, acc) == (* An alias for FoldSet. ReduceSet was used instead of FoldSet in *) (* earlier versions of the community modules. *) (*************************************************************************) - FoldSet(op, set, acc) + FoldSet(op, acc, set) FlattenSet(S) == diff --git a/tests/FiniteSetsExtTests.tla b/tests/FiniteSetsExtTests.tla index 5a9481a..4c53a3a 100644 --- a/tests/FiniteSetsExtTests.tla +++ b/tests/FiniteSetsExtTests.tla @@ -90,7 +90,6 @@ ASSUME FoldSet(LAMBDA x,y : x + y, 0, 0 .. 10) = 55 \* Without the corresponding Java module override, this overflows TLC's stack. ASSUME FoldSet(LAMBDA x,y : x + y, 0, 0 .. 10000) = 50005000 - ----------------------------------------------------------------------------- ASSUME ChooseUnique({2, 3, 4, 5}, LAMBDA x : x % 3 = 1) = 4 @@ -122,6 +121,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 *)