From e73c95512b4bae2c8562c2825473b4032f7fc818 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 3 Oct 2026 14:00:26 -0700 Subject: [PATCH] Add pure tests for more operators with Java module overrides Check the overrides exhaustively against pure TLA+ definitions over small inputs. Folds with an unspecified order are only compared on operators for which the order does not matter. Operators defined via CHOOSE are checked for membership in the set they choose from. [Tests] Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- tests/BagsExtTests.tla | 7 +++ tests/BitwiseTests.tla | 12 +++++ tests/DyadicRationalsTests.tla | 36 +++++++++++++++ tests/FiniteSetsExtTests.tla | 10 +++++ tests/FunctionsTests.tla | 16 +++++++ tests/IOUtilsTests.tla | 6 +++ tests/SVGTests.tla | 11 +++++ tests/SequencesExtTests.tla | 81 ++++++++++++++++++++++++++++++++++ tests/VectorClocksTests.tla | 19 ++++++++ 9 files changed, 198 insertions(+) diff --git a/tests/BagsExtTests.tla b/tests/BagsExtTests.tla index 3294681..f4e6fc0 100644 --- a/tests/BagsExtTests.tla +++ b/tests/BagsExtTests.tla @@ -52,6 +52,13 @@ ASSUME LET B == ({1}:>2) @@ ({-2}:>1) @@ ({3}:>3) IN FoldBag(LAMBDA x,y : x \union y, {}, B) = TLAFoldBag(LAMBDA x,y : x \union y, {}, B) +\* FoldBag does not fix the order in which it combines elements, so it is +\* only compared on operators for which the order does not matter. +ASSUME \A D \in SUBSET {-2, 1, 3} : \A B \in [D -> 1..3] : + /\ FoldBag(LAMBDA x,y : x+y, 0, B) = TLAFoldBag(LAMBDA x,y : x+y, 0, B) + /\ FoldBag(LAMBDA x,y : x*y, 1, B) = TLAFoldBag(LAMBDA x,y : x*y, 1, B) + /\ FoldBag(LAMBDA x,y : IF x > y THEN x ELSE y, -9, B) = TLAFoldBag(LAMBDA x,y : IF x > y THEN x ELSE y, -9, B) + ASSUME FoldBag(LAMBDA x,y : x+y, 0, (1:>2) @@ (2:>1) @@ (3:>3)) = 13 ASSUME FoldBag(LAMBDA x,y : x+y, 0, (1:>2) @@ (-2:>1)) = 0 diff --git a/tests/BitwiseTests.tla b/tests/BitwiseTests.tla index 9e9364f..b053b39 100644 --- a/tests/BitwiseTests.tla +++ b/tests/BitwiseTests.tla @@ -165,4 +165,16 @@ ASSUME \A n \in 0..64 : AssertEq(Not(n), NotPure(n)) ASSUME(\A n \in ZeroToM : AssertEq(shiftR(n, 1), (n \div 2))) +shiftRPure(n, pos) == + LET RECURSIVE shiftRPureR(_,_) + shiftRPureR(x, p) == + IF p = 0 + THEN x + ELSE LET odd(z) == z % 2 = 1 + m == IF odd(x) THEN (x-1) \div 2 ELSE x \div 2 + IN shiftRPureR(m, p - 1) + IN shiftRPureR(n, pos) + +ASSUME \A n \in 0..64, pos \in 0..8 : AssertEq(shiftR(n, pos), shiftRPure(n, pos)) + ============================================================================= diff --git a/tests/DyadicRationalsTests.tla b/tests/DyadicRationalsTests.tla index 4730719..e593db0 100644 --- a/tests/DyadicRationalsTests.tla +++ b/tests/DyadicRationalsTests.tla @@ -14,4 +14,40 @@ ASSUME(Half([num |-> 1, den |-> 128]) = [num |-> 1, den |-> 256]) ASSUME(Half([num |-> 1, den |-> 256]) = [num |-> 1, den |-> 512]) ASSUME(Half([num |-> 2, den |-> 8]) = [num |-> 1, den |-> 8]) + +----------------------------------------------------------------------------- + +(***************************************************************************) +(* Reduce is LOCAL to DyadicRationals, so its Java override is checked via *) +(* Add and Half against copies of their definitions that use a pure *) +(* Reduce. The pure GCD is undefined for a zero numerator, hence only *) +(* positive numerators. *) +(***************************************************************************) +LOCAL INSTANCE Integers +LOCAL INSTANCE FiniteSetsExt + +LOCAL GCDPure(n, m) == + LET Divisors(q) == {d \in 1..q : \E e \in 1..q : q = d * e} + IN Max(Divisors(n) \cap Divisors(m)) + +LOCAL ReducePure(p) == + LET gcd == GCDPure(p.num, p.den) + IN IF gcd = 1 THEN p + ELSE [num |-> p.num \div gcd, den |-> p.den \div gcd] + +LOCAL AddPure(p, q) == + IF p = Zero THEN q ELSE + LET lcn == Max({p.den, q.den}) + qq == [num |-> q.num * (lcn \div q.den), den |-> q.den * (lcn \div q.den)] + pp == [num |-> p.num * (lcn \div p.den), den |-> p.den * (lcn \div p.den)] + IN ReducePure([num |-> qq.num + pp.num, den |-> lcn]) + +LOCAL HalfPure(p) == + ReducePure([num |-> p.num, den |-> p.den * 2]) + +LOCAL SomeDyadics == + [num : 1..9, den : {1, 2, 4, 8, 16}] + +ASSUME \A p \in SomeDyadics : Half(p) = HalfPure(p) +ASSUME \A p, q \in SomeDyadics : Add(p, q) = AddPure(p, q) ============================================================================= diff --git a/tests/FiniteSetsExtTests.tla b/tests/FiniteSetsExtTests.tla index 05bb62b..20aec36 100644 --- a/tests/FiniteSetsExtTests.tla +++ b/tests/FiniteSetsExtTests.tla @@ -67,6 +67,16 @@ 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 + +FoldSetPure(op(_,_), base, set) == + MapThenFoldSet(op, base, LAMBDA x : x, LAMBDA s : CHOOSE x \in s : TRUE, set) + +\* FoldSet does not fix the order in which it combines elements, so it is +\* only compared on operators for which the order does not matter. +ASSUME \A S \in SUBSET (-2..3) : + /\ FoldSet(LAMBDA x,y : x + y, 0, S) = FoldSetPure(LAMBDA x,y : x + y, 0, S) + /\ FoldSet(LAMBDA x,y : x * y, 1, S) = FoldSetPure(LAMBDA x,y : x * y, 1, S) + /\ FoldSet(LAMBDA x,y : {x} \cup y, {}, S) = FoldSetPure(LAMBDA x,y : {x} \cup y, {}, S) ----------------------------------------------------------------------------- ASSUME ChooseUnique({2, 3, 4, 5}, LAMBDA x : x % 3 = 1) = 4 diff --git a/tests/FunctionsTests.tla b/tests/FunctionsTests.tla index a05d7b5..69f54b8 100644 --- a/tests/FunctionsTests.tla +++ b/tests/FunctionsTests.tla @@ -54,6 +54,22 @@ ASSUME FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, [n \in 1..9999 |-> n], {}) ASSUME FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, [n \in 1..9999 |-> n], 2..9998) = 2..9998 +\* FoldFunction and FoldFunctionOnSet do not fix the order in which they combine +\* elements, so they are only compared on operators for which the order does not matter. +ASSUME + LET FoldFunctionOnSetPure(op(_,_), base, fun, indices) == + MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) + FoldFunctionPure(op(_,_), base, fun) == + FoldFunctionOnSetPure(op, base, fun, DOMAIN fun) + Check(f) == + /\ FoldFunction(+, 0, f) = FoldFunctionPure(+, 0, f) + /\ FoldFunction(LAMBDA x,y: {x} \cup y, {}, f) = FoldFunctionPure(LAMBDA x,y: {x} \cup y, {}, f) + /\ \A I \in SUBSET DOMAIN f : + /\ FoldFunctionOnSet(+, 0, f, I) = FoldFunctionOnSetPure(+, 0, f, I) + /\ FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, f, I) = FoldFunctionOnSetPure(LAMBDA x,y: {x} \cup y, {}, f, I) + IN /\ \A f \in [{1,2,3} -> {-1,0,2}] : Check(f) + /\ \A f \in [{"a","b","c"} -> {-1,0,2}] : Check(f) + ASSUME AssertError( "The third argument of FoldFunction should be a function, but instead it is:\nTRUE", FoldFunction(+, 23, TRUE)) diff --git a/tests/IOUtilsTests.tla b/tests/IOUtilsTests.tla index 1f3e86c..9beb3b7 100644 --- a/tests/IOUtilsTests.tla +++ b/tests/IOUtilsTests.tla @@ -25,6 +25,12 @@ ASSUME(atoi("0") = 0) ASSUME(atoi("-0") = 0) ASSUME(atoi("-1") = -1) +\* atoi chooses from the unbounded set Int, which TLC cannot enumerate. +atoiPure(str) == + CHOOSE i \in -1000..1000 : ToString(i) = str + +ASSUME \A i \in -1000..1000 : AssertEq(atoi(ToString(i)), atoiPure(ToString(i))) + ASSUME AssertError( "The argument of atoi should be a string, but instead it is:\n\"\"", atoi("")) diff --git a/tests/SVGTests.tla b/tests/SVGTests.tla index 1384acb..b9d344b 100644 --- a/tests/SVGTests.tla +++ b/tests/SVGTests.tla @@ -133,6 +133,17 @@ ASSUME( 3 :> [x |-> 16, y |-> 9 ] ) ) +PointOnLinePure(from, to, segment) == + [x |-> from.x + ((to.x - from.x) \div segment), + y |-> from.y + ((to.y - from.y) \div segment)] + +\* The override truncates towards zero whereas \div rounds down, thus the two +\* only agree if the resulting coordinates are non-negative. +ASSUME \A fx, fy, tx, ty \in 0..6, segment \in 1..4 : + LET from == [x |-> fx, y |-> fy] + to == [x |-> tx, y |-> ty] + IN AssertEq(PointOnLine(from, to, segment), PointOnLinePure(from, to, segment)) + ASSUME(LET elem == Text(0, 0, ToString(<<1,2,3>>), <<>>) IN diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla index 3ab2732..82939da 100644 --- a/tests/SequencesExtTests.tla +++ b/tests/SequencesExtTests.tla @@ -22,6 +22,13 @@ ASSUME(LET s == {"t","l","a","p","l","u","s"} seq == SetToSeq(s) IN Len(seq) = Cardinality(s) /\ ToSet(seq) = s) +\* SetToSeq is defined via CHOOSE, so its pure counterpart is the set of all +\* sequences that it may choose from. +SetToSeqPure(S) == + { f \in [1..Cardinality(S) -> S] : \A i, j \in 1..Cardinality(S) : i # j => f[i] # f[j] } + +ASSUME \A S \in SUBSET {"a", "b", "c", "d"} : SetToSeq(S) \in SetToSeqPure(S) + ASSUME(Reverse(<<>>) = <<>>) ASSUME(Reverse(<<1,2,3>>) = <<3,2,1>>) ASSUME(Reverse(<<1,1,2>>) = <<2,1,1>>) @@ -57,6 +64,12 @@ ASSUME(~IsPrefix(<<2>>, <<1>>)) ASSUME(~IsPrefix(<<2,1>>, <<1,2>>)) ASSUME(~IsPrefix(<<1,2>>, <<2,1>>)) +IsPrefixPure(s, t) == + Len(s) <= Len(t) /\ SubSeq(s, 1, Len(s)) = SubSeq(t, 1, Len(s)) + +ASSUME \A s, t \in BoundedSeq(1..2, 3) : AssertEq(IsPrefix(s, t), IsPrefixPure(s, t)) +ASSUME \A s, t \in {"", "a", "b", "ab", "ba", "abc"} : AssertEq(IsPrefix(s, t), IsPrefixPure(s, t)) + ASSUME(~IsStrictPrefix(<<>>, <<>>)) ASSUME(IsStrictPrefix(<<>>, <<1>>)) ASSUME(IsStrictPrefix(<<1>>, <<1,2>>)) @@ -83,6 +96,11 @@ ASSUME(Contains(<<{3},{4}>>, {4})) ASSUME(Contains(<<{3},{4}>>, {3})) ASSUME(~Contains(<<{3},{4}>>, {2})) +ContainsPure(s, e) == + \E i \in 1..Len(s) : s[i] = e + +ASSUME \A s \in BoundedSeq(1..3, 4), e \in 0..4 : AssertEq(Contains(s, e), ContainsPure(s, e)) + ----------------------------------------------------------------------------- ASSUME LET cons(x,y) == <> @@ -120,6 +138,26 @@ ASSUME AssertError( "The third argument of FoldFunction should be a function, but instead it is:\nTRUE", FoldSeq(+, 23, TRUE)) +FoldSeqPure(op(_, _), base, seq) == + MapThenFoldSet(op, base, LAMBDA i : seq[i], LAMBDA S : CHOOSE x \in S : TRUE, DOMAIN seq) + +FoldLeftPure(op(_, _), base, seq) == + MapThenFoldSet(LAMBDA x,y : op(y,x), base, LAMBDA i : seq[i], LAMBDA S : Max(S), DOMAIN seq) + +FoldRightPure(op(_, _), seq, base) == + MapThenFoldSet(op, base, LAMBDA i : seq[i], LAMBDA S : Min(S), DOMAIN seq) + +\* FoldSeq does not fix the order in which it combines elements, so it is +\* only compared on operators for which the order does not matter. +ASSUME LET cons(x,y) == <> + IN \A seq \in BoundedSeq(1..3, 4): + /\ AssertEq(FoldSeq(+, 0, seq), FoldSeqPure(+, 0, seq)) + /\ AssertEq(FoldSeq(LAMBDA x,y: {x} \cup y, {}, seq), FoldSeqPure(LAMBDA x,y: {x} \cup y, {}, seq)) + /\ AssertEq(FoldLeft(cons, 0, seq), FoldLeftPure(cons, 0, seq)) + /\ AssertEq(FoldLeft(-, 0, seq), FoldLeftPure(-, 0, seq)) + /\ AssertEq(FoldRight(cons, seq, 0), FoldRightPure(cons, seq, 0)) + /\ AssertEq(FoldRight(-, seq, 0), FoldRightPure(-, seq, 0)) + ----------------------------------------------------------------------------- ASSUME LongestCommonPrefix({<<>>}) = <<>> @@ -439,6 +477,18 @@ ASSUME AssertEq(SelectLastInSeq(<<>>, Op), 0) ASSUME AssertEq(SelectLastInSeq(<<1,1,2>> , LAMBDA e : e = 1), 2) ASSUME AssertEq(SelectLastInSeq(<<1,1,2,2>>, LAMBDA e : e = 2), 4) +SelectInSeqPure(seq, Test(_)) == + LET I == { i \in 1..Len(seq) : Test(seq[i]) } + IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i <= j ELSE 0 + +SelectLastInSeqPure(seq, Test(_)) == + LET I == { i \in 1..Len(seq) : Test(seq[i]) } + IN IF I # {} THEN CHOOSE i \in I : \A j \in I : i >= j ELSE 0 + +ASSUME \A seq \in BoundedSeq(1..3, 4), v \in 0..3 : + /\ AssertEq(SelectInSeq(seq, LAMBDA e : e = v), SelectInSeqPure(seq, LAMBDA e : e = v)) + /\ AssertEq(SelectLastInSeq(seq, LAMBDA e : e = v), SelectLastInSeqPure(seq, LAMBDA e : e = v)) + ASSUME AssertEq(SelectInSubSeq(<<>>, 1, Len(<<>>), Op), 0) ASSUME AssertEq(SelectInSubSeq(<<1,1,2>> , 2, 3, LAMBDA e : e = 1), 2) ASSUME AssertEq(SelectInSubSeq(<<1,1,2,2>>, 2, 4, LAMBDA e : e = 2), 3) @@ -473,6 +523,11 @@ ASSUME AssertEq(Suffixes(<<>>), {<<>>}) ASSUME AssertEq(Suffixes(<<1>>), {<<>>, <<1>>}) ASSUME AssertEq(Suffixes(<<1,2>>), {<<>>, <<1,2>>, <<2>>}) ASSUME AssertEq(Suffixes(<<1,2,3>>), {<<>>, <<3>>, <<2,3>>, <<1,2,3>>}) + +SuffixesPure(s) == + { SubSeq(s, l, Len(s)) : l \in 1..Len(s) } \cup {<<>>} + +ASSUME \A s \in BoundedSeq(1..3, 4) : AssertEq(Suffixes(s), SuffixesPure(s)) ----------------------------------------------------------------------------- ASSUME AssertEq(RemoveFirst(<<>>, 1), <<>>) @@ -487,8 +542,34 @@ ASSUME AssertEq(RemoveFirstMatch(<<1,2>>, LAMBDA e: e = 1), <<2>>) ASSUME AssertEq(RemoveFirstMatch(<<1,2,1>>, LAMBDA e: e = 1), <<2,1>>) ASSUME AssertEq(RemoveFirstMatch(<<1,2,1,2>>, LAMBDA e: e = 2), <<1,1,2>>) +RemoveFirstPure(s, e) == + IF \E i \in 1..Len(s): s[i] = e + THEN RemoveAt(s, SelectInSeqPure(s, LAMBDA v: v = e)) + ELSE s + +RemoveFirstMatchPure(s, Test(_)) == + IF \E i \in 1..Len(s): Test(s[i]) + THEN RemoveAt(s, SelectInSeqPure(s, Test)) + ELSE s + +ASSUME \A s \in BoundedSeq(1..3, 4), e \in 0..3 : + /\ AssertEq(RemoveFirst(s, e), RemoveFirstPure(s, e)) + /\ AssertEq(RemoveFirstMatch(s, LAMBDA v : v = e), RemoveFirstMatchPure(s, LAMBDA v : v = e)) + /\ AssertEq(RemoveFirstMatch(s, LAMBDA v : v >= e), RemoveFirstMatchPure(s, LAMBDA v : v >= e)) + ----------------------------------------------------------------------------- ASSUME LET seq == <<"a","b","c","d","e">> IN AssertEq(FoldLeftDomain (LAMBDA acc, idx : acc \o seq[idx], "", seq), "abcde") ASSUME LET seq == <<"a","b","c","d","e">> IN AssertEq(FoldRightDomain(LAMBDA idx, acc : acc \o seq[idx], seq, ""), "edcba") + +FoldLeftDomainPure(op(_, _), base, seq) == + FoldLeftPure(op, base, [i \in DOMAIN seq |-> i]) + +FoldRightDomainPure(op(_, _), seq, base) == + FoldRightPure(op, [i \in DOMAIN seq |-> i], base) + +ASSUME LET cons(x,y) == <> + IN \A seq \in BoundedSeq(1..3, 4): + /\ AssertEq(FoldLeftDomain(cons, 0, seq), FoldLeftDomainPure(cons, 0, seq)) + /\ AssertEq(FoldRightDomain(cons, seq, 0), FoldRightDomainPure(cons, seq, 0)) ============================================================================= diff --git a/tests/VectorClocksTests.tla b/tests/VectorClocksTests.tla index e9fc842..7a84433 100644 --- a/tests/VectorClocksTests.tla +++ b/tests/VectorClocksTests.tla @@ -37,4 +37,23 @@ ASSUME IsCausalOrder( LAMBDA vc: DOMAIN vc), VectorClock) +\* CausalOrder is defined via CHOOSE, so its pure counterpart is the set of all +\* logs that it may choose from. +CausalOrderPure(log, clock(_)) == + { f \in [ 1..Len(log) -> Range(log)] : + Range(f) = Range(log) /\ IsCausalOrder(f, clock) } + +\* Node 1 sends a message to node 2 after its first event, and both nodes +\* have one more event that is concurrent with the other node's events. +SmallLog == + << [node |-> 1, vc |-> <<1, 0>>], + [node |-> 2, vc |-> <<0, 1>>], + [node |-> 2, vc |-> <<1, 2>>], + [node |-> 1, vc |-> <<2, 0>>] >> + +ASSUME \A p \in Permutations(DOMAIN SmallLog) : + LET log == << SmallLog[p[1]], SmallLog[p[2]], SmallLog[p[3]], SmallLog[p[4]] >> + IN CausalOrder(log, LAMBDA l: l.vc, LAMBDA l: l.node, LAMBDA vc: DOMAIN vc) + \in CausalOrderPure(log, LAMBDA l: l.vc) + =============================================================================