Rename operator IsASet to IsInjective (in TLA+ all things are sets).

Author: lemmy

SequencesExt.java

@@ -38,21 +38,21 @@ private SequencesExt() {
 		// no-instantiation!
 	}
 
-	public static BoolValue IsASet(final Value val) {
+	public static BoolValue IsInjective(final Value val) {
 		if (val instanceof TupleValue) {
-			return isASetNonDestructive(((TupleValue) val).elems);
+			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[] { "IsASet", "sequence", Values.ppr(val.toString()) });
 			}
-			return isASetDestructive(((TupleValue) conv).elems);
+			return isInjectiveDestructive(((TupleValue) conv).elems);
 		}
 	}
 
 	// O(n log n) runtime and O(1) space.
-	private static BoolValue isASetDestructive(final Value[] values) {
+	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])) {
@@ -66,7 +66,7 @@ private static BoolValue isASetDestructive(final Value[] values) {
 	// 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 isASetNonDestructive(final Value[] values) {
+	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])) {

SequencesExt.tla

@@ -15,15 +15,14 @@ ToSet(s) ==
   (*************************************************************************)
   { s[i] : i \in 1..Len(s) }
 
-IsASet(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                *)
-  (* tlc2.module.SequencesExt. The operator is overridden by the Java      *)
-  (* method with the same name.                                            *)
+  (* This definition is overridden by TLC in the Java class SequencesExt.  *)
+  (* The operator is overridden by the Java method with the same name.     *)
   (*************************************************************************)
   \A i,j \in 1..Len(s): i # j => s[i] # s[j]
 

SequencesExtTests.tla

@@ -1,15 +1,15 @@
 ------------------------- MODULE SequencesExtTests -------------------------
 EXTENDS Sequences, SequencesExt, Naturals, TLC
 
-ASSUME(IsASet(<<>>))
-ASSUME(IsASet(<<1>>))
-ASSUME(IsASet(<<1,2,3>>))
-ASSUME(~IsASet(<<1,1>>))
-ASSUME(~IsASet(<<1,1,2,3>>))
+ASSUME(IsInjective(<<>>))
+ASSUME(IsInjective(<<1>>))
+ASSUME(IsInjective(<<1,2,3>>))
+ASSUME(~IsInjective(<<1,1>>))
+ASSUME(~IsInjective(<<1,1,2,3>>))
 
-ASSUME(IsASet([i \in 1..10 |-> i]))
-ASSUME(IsASet([i \in 1..10 |-> {i}]))
-ASSUME(IsASet([i \in 1..10 |-> {i}]))
-ASSUME(~IsASet([i \in 1..10 |-> {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}]))
 
 =============================================================================