First community module with optional *Tests and

*Proofs (latter incomplete).

Basic Azure Pipeline included too.

.gitignore

@@ -0,0 +1,5 @@
+lib/
+dist/
+build/
+*.toolbox/
+*.tlaps/

SequencesExt.java

@@ -0,0 +1,79 @@
+/*******************************************************************************
+ * 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
+ ******************************************************************************/
+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.TupleValue;
+import tlc2.value.impl.Value;
+
+public final class SequencesExt {
+
+	private SequencesExt() {
+		// no-instantiation!
+	}
+
+	public static BoolValue IsASet(final Value val) {
+		if (val instanceof TupleValue) {
+			return isASetNonDestructive(((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);
+		}
+	}
+
+	// O(n log n) runtime and O(1) space.
+	private static BoolValue isASetDestructive(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 isASetNonDestructive(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;
+	}
+}

SequencesExt.tla

@@ -0,0 +1,30 @@
+---------------------------- MODULE SequencesExt ----------------------------
+
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE Naturals
+  (*************************************************************************)
+  (* Imports the definitions from the modules, but doesn't export them.    *)
+  (*************************************************************************)
+
+-----------------------------------------------------------------------------
+
+ToSet(s) ==
+  (*************************************************************************)
+  (* The image of the given sequence s. Cardinality(ToSet(s)) <= Len(s)    *)
+  (* see https://en.wikipedia.org/wiki/Image_(mathematics)                 *)
+  (*************************************************************************)
+  { s[i] : i \in 1..Len(s) }
+
+IsASet(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.                                            *)
+  (*************************************************************************)
+  \A i,j \in 1..Len(s): i # j => s[i] # s[j]
+
+=============================================================================

SequencesExtProofs.tla

@@ -0,0 +1,8 @@
+------------------------- MODULE SequencesExtProofs -------------------------
+EXTENDS FiniteSets, Sequences, SequencesExt, Naturals, Integers, TLAPS
+
+(* TODO: Meaningful theorems for the operators in SequencesExt. *)
+THEOREM TBD == TRUE
+OBVIOUS
+
+=============================================================================

SequencesExtTests.tla

@@ -0,0 +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(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}]))
+
+=============================================================================

azure-pipelines.yml

@@ -0,0 +1,31 @@
+trigger:
+ - master
+
+pool:
+   vmImage: 'Ubuntu-16.04'
+
+steps:
+  - task: Ant@1
+    inputs:
+      buildFile: 'build.xml' 
+      javaHomeOption: 'JDKVersion'
+      jdkVersionOption: '1.8'
+      jdkArchitectureOption: 'x64'
+
+  - task: GitHubRelease@0
+    inputs:
+      gitHubConnection:  CommunityModules
+      #repositoryName: '$(Build.Repository.Name)' 
+      #action: 'create' # Options: create, edit, delete
+      #target: '$(Build.SourceVersion)' # Required when action == Create || Action == Edit
+      tagSource: 'manual' # Required when action == Create# Options: auto, manual
+      tag: '$(Build.BuildNumber)' # Required when action == Edit || Action == Delete || TagSource == Manual
+      #title: # Optional
+      #releaseNotesSource: 'file' # Optional. Options: file, input
+      #releaseNotesFile: # Optional
+      #releaseNotes: # Optional
+      assets: 'dist/CommunityModules-*.jar' # Optional
+      #assetUploadMode: 'delete' # Optional. Options: delete, replace
+      #isDraft: false # Optional
+      #isPreRelease: false # Optional
+      #addChangeLog: true # Optional

build.xml

@@ -0,0 +1,37 @@
+<project name="CommunityModules" default="dist" basedir=".">
+
+  <property name="src" location="."/>
+  <property name="build" location="build"/>
+  <property name="dist" location="dist"/>
+  <property name="lib" location="lib"/>
+
+  <target name="init" description="Create the build and dist directory structure">
+    <mkdir dir="${build}"/>
+    <mkdir dir="${dist}"/>
+    <mkdir dir="${lib}"/>
+  </target>
+
+  <target name="compile" depends="init" description="compile the java module overwrites">
+    <get src="https://nightly.tlapl.us/dist/tla2tools.jar" dest="${lib}"/>
+    <javac srcdir="${src}" destdir="${build}" classpath="${lib}/tla2tools.jar"
+           source="1.8"
+           target="1.8"
+           includeantruntime="false"/>
+  </target>
+
+  <target name="dist" depends="compile" description="Combine the module overwrites and the TLA+ definitions into a distribution">
+    <tstamp/>
+    <jar jarfile="${dist}/CommunityModules-${DSTAMP}${TSTAMP}.jar">
+         <fileset dir="${build}/"
+             includes="*.class"/>
+         <fileset dir="${src}/"
+             includes="*.tla,*.java,LICENSE,README.md"/>
+    </jar>
+  </target>
+
+  <target name="clean" description="Delete the ${build} and ${dist} directory trees">
+    <delete dir="${build}"/>
+    <delete dir="${dist}"/>
+    <delete dir="${lib}"/>
+  </target>
+</project>