Add pure tests for more operators with Java module overrides

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
 

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))
+
 =============================================================================

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)
 =============================================================================

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

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))

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(""))

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

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) == <<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) == <<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) == <<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))
 =============================================================================

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)
+
 =============================================================================