suggested additions / changes for SequencesExt

.github/workflows/main.yml

@@ -20,22 +20,6 @@ jobs:
     - name: Get current date
       id: date
       run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
-    # Do not download and install TLAPS over and over again.
-    - uses: actions/cache@v1
-      id: cache
-      with:
-        path: tlaps/
-        key: tlaps1.4.5
-    - name: Get TLAPS
-      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
-      run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
-    - name: Install TLAPS
-      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
-      run: |
-        chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin
-        ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps
-    - name: Run TLAPS
-      run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I modules/ modules/SequencesExtTheorems_proofs.tla
     - name: Build with Ant
       run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
     - name: Copied CommunityModules-SomeDate.jar to CommunityModules.jar

modules/Functions.tla

@@ -27,10 +27,18 @@ Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t]
 
 
 (***************************************************************************)
-(* A map is an injection iff each element in the domain maps to a distinct *)
-(* element in the range.                                                   *)
+(* A function is injective iff it maps each element in its domain to a     *)
+(* distinct element.                                                       *)
+(*                                                                         *)
+(* This definition is overridden by TLC in the Java class SequencesExt.    *)
+(* The operator is overridden by the Java method with the same name.       *)
 (***************************************************************************)
-Injection(S,T) == { M \in [S -> T] : \A a,b \in S : M[a] = M[b] => a = b }
+IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
+
+(***************************************************************************)
+(* Set of injections between two sets.                                     *)
+(***************************************************************************)
+Injection(S,T) == { M \in [S -> T] : IsInjective(M) }
 
 
 (***************************************************************************)
@@ -57,7 +65,7 @@ ExistsBijection(S,T)  == Bijection(S,T) # {}
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Jul 10 20:32:37 CEST 2013 by merz
+\* Last modified Sun Dec 27 09:38:06 CET 2020 by merz
 \* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav
 \* Last modified Fri May 03 12:55:35 PDT 2013 by tomr
 \* Created Thu Apr 11 10:30:48 PDT 2013 by tomr

modules/SequencesExt.tla

@@ -18,19 +18,6 @@ ToSet(s) ==
   (*************************************************************************)
   { s[i] : i \in DOMAIN s }
 
-IsInjective(s) == 
-  (*************************************************************************)
-  (* TRUE iff the sequence s contains no duplicates where two elements     *)
-  (* a, b of s are defined to be duplicates iff a = b.  In other words,    *)
-  (* Cardinality(ToSet(s)) = Len(s)                                        *)
-  (*                                                                       *)
-  (* This definition is overridden by TLC in the Java class SequencesExt.  *)
-  (* The operator is overridden by the Java method with the same name.     *)
-  (*                                                                       *)
-  (* Also see Functions!Injective operator.                                *)
-  (*************************************************************************)
-  \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
-
 SetToSeq(S) == 
   (**************************************************************************)
   (* Convert a set to some sequence that contains all the elements of the   *)
@@ -121,6 +108,12 @@ RemoveAt(s, i) ==
 
 -----------------------------------------------------------------------------
 
+Cons(elt, seq) == 
+    (***************************************************************************)
+    (* Cons prepends an element at the beginning of a sequence.                *)
+    (***************************************************************************)
+    <<elt>> \o seq
+
 Front(s) == 
   (**************************************************************************)
   (* The sequence formed by removing its last element.                      *)

modules/tlc2/overrides/Functions.java

@@ -0,0 +1,83 @@
+/*******************************************************************************
+ * Copyright (c) 2019 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.overrides;
+
+import java.util.Arrays;
+
+import tlc2.output.EC;
+import tlc2.tool.EvalException;
+import tlc2.value.Values;
+import tlc2.value.impl.BoolValue;
+import tlc2.value.impl.SetEnumValue;
+import tlc2.value.impl.TupleValue;
+import tlc2.value.impl.Value;
+
+public final class Functions {
+
+	private Functions() {
+		// no-instantiation!
+	}
+
+	@TLAPlusOperator(identifier = "IsInjective", module = "Functions", warn = false)
+	public static BoolValue IsInjective(final Value val) {
+		if (val instanceof TupleValue) {
+			return isInjectiveNonDestructive(((TupleValue) val).elems);
+		} else {
+			final Value conv = val.toTuple();
+			if (conv == null) {
+				throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+						new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) });
+			}
+			return isInjectiveDestructive(((TupleValue) conv).elems);
+		}
+	}
+
+	// O(n log n) runtime and O(1) space.
+	private static BoolValue isInjectiveDestructive(final Value[] values) {
+		Arrays.sort(values);
+		for (int i = 1; i < values.length; i++) {
+			if (values[i-1].equals(values[i])) {
+				return BoolValue.ValFalse;
+			}
+		}
+		return BoolValue.ValTrue;
+	}
+
+	// Assume small arrays s.t. the naive approach with O(n^2) runtime but O(1)
+	// space is good enough. Sorting values in-place is a no-go because it
+	// would modify the TLA+ tuple. Elements can be any sub-type of Value, not
+	// just IntValue.
+	private static BoolValue isInjectiveNonDestructive(final Value[] values) {
+		for (int i = 0; i < values.length; i++) {
+			for (int j = i + 1; j < values.length; j++) {
+				if (values[i].equals(values[j])) {
+					return BoolValue.ValFalse;
+				}
+			}
+		}
+		return BoolValue.ValTrue;
+	}
+}

modules/tlc2/overrides/SequencesExt.java

@@ -24,7 +24,6 @@
  * Contributors:
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
-import java.util.Arrays;
 
 import tlc2.output.EC;
 import tlc2.tool.EvalException;
@@ -40,46 +39,6 @@ private SequencesExt() {
 		// no-instantiation!
 	}
 
-	@TLAPlusOperator(identifier = "IsInjective", module = "SequencesExt", warn = false)
-	public static BoolValue IsInjective(final Value val) {
-		if (val instanceof TupleValue) {
-			return isInjectiveNonDestructive(((TupleValue) val).elems);
-		} else {
-			final Value conv = val.toTuple();
-			if (conv == null) {
-				throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
-						new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) });
-			}
-			return isInjectiveDestructive(((TupleValue) conv).elems);
-		}
-	}
-
-	// O(n log n) runtime and O(1) space.
-	private static BoolValue isInjectiveDestructive(final Value[] values) {
-		Arrays.sort(values);
-		for (int i = 1; i < values.length; i++) {
-			if (values[i-1].equals(values[i])) {
-				return BoolValue.ValFalse;
-			}
-		}
-		return BoolValue.ValTrue;
-	}
-
-	// Assume small arrays s.t. the naive approach with O(n^2) runtime but O(1)
-	// space is good enough. Sorting values in-place is a no-go because it
-	// would modify the TLA+ tuple. Elements can be any sub-type of Value, not
-	// just IntValue.
-	private static BoolValue isInjectiveNonDestructive(final Value[] values) {
-		for (int i = 0; i < values.length; i++) {
-			for (int j = i + 1; j < values.length; j++) {
-				if (values[i].equals(values[j])) {
-					return BoolValue.ValFalse;
-				}
-			}
-		}
-		return BoolValue.ValTrue;
-	}
-
 	/*
 	 * Improve carbon footprint of SequencesExt!SetToSeq. Convert SetEnumValue to
 	 * TupleValue (linear in the number of elements) instead of generating the set

modules/tlc2/overrides/TLCOverrides.java

@@ -34,12 +34,12 @@ public class TLCOverrides implements ITLCOverrides {
 	public Class[] get() {
 		try {
 			Json.resolves();
-			return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class };
+			return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class };
 		} catch (NoClassDefFoundError e) {
 			System.out.println(
 					"com.fasterxml.jackson dependencies of Json overrides not found, Json module won't work unless "
 					+ "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.");
 		}
-		return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class };
+		return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class };
 	}
 }

tests/AllTests.tla

@@ -9,6 +9,7 @@ EXTENDS SequencesExtTests,
         JsonTests,
         BitwiseTests,
         IOUtilsTests,
-        FiniteSetsExtTests
+        FiniteSetsExtTests,
+        FunctionsTests
 
 ===========================================

tests/FunctionsTests.tla

@@ -0,0 +1,19 @@
+------------------------- MODULE FunctionsTests -------------------------
+EXTENDS Functions, Naturals, TLC, TLCExt, FiniteSets
+
+ASSUME(IsInjective(<<>>))
+ASSUME(IsInjective(<<1>>))
+ASSUME(IsInjective(<<1,2,3>>))
+ASSUME(~IsInjective(<<1,1>>))
+ASSUME(~IsInjective(<<1,1,2,3>>))
+
+ASSUME(IsInjective([i \in 1..10 |-> i]))
+ASSUME(IsInjective([i \in 1..10 |-> {i}]))
+ASSUME(IsInjective([i \in 1..10 |-> {i}]))
+ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}]))
+
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n{}", IsInjective({})))
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n[a: 1, b: 2]", IsInjective([a: 1, b: 2])))
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n(0 :> 0 @@ 1 :> 1 @@ 2 :> 2)", IsInjective([i \in 0..2 |-> i])))
+
+=============================================================================

tests/SequencesExtTests.tla

@@ -10,21 +10,6 @@ ASSUME(ToSet([i \in 1..10 |-> i]) = 1..10)
 ASSUME(ToSet(Tail([i \in 1..10 |-> i])) = 2..10)
 ASSUME(ToSet([i \in 0..9 |-> 42]) = {42})
 
-ASSUME(IsInjective(<<>>))
-ASSUME(IsInjective(<<1>>))
-ASSUME(IsInjective(<<1,2,3>>))
-ASSUME(~IsInjective(<<1,1>>))
-ASSUME(~IsInjective(<<1,1,2,3>>))
-
-ASSUME(IsInjective([i \in 1..10 |-> i]))
-ASSUME(IsInjective([i \in 1..10 |-> {i}]))
-ASSUME(IsInjective([i \in 1..10 |-> {i}]))
-ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}]))
-
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n{}", IsInjective({})))
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n[a: 1, b: 2]", IsInjective([a: 1, b: 2])))
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n(0 :> 0 @@ 1 :> 1 @@ 2 :> 2)", IsInjective([i \in 0..2 |-> i])))
-
 ASSUME(SetToSeq({}) = <<>>)
 ASSUME(SetToSeq({1}) = <<1>>)
 ASSUME(LET s == {"t","l","a","p","l","u","s"}