Add Statistics!ChiSquare operator implemented with Apache Commons

Math3.

[Feature]

.classpath

@@ -14,5 +14,6 @@
 	<classpathentry kind="lib" path="lib/jgrapht-core-1.5.1.jar"/>
 	<classpathentry kind="lib" path="lib/slf4j-api-1.7.30.jar"/>
 	<classpathentry kind="lib" path="lib/commons-lang3-3.12.0.jar"/>
+	<classpathentry kind="lib" path="lib/commons-math3-3.6.1.jar"/>
 	<classpathentry kind="output" path="build"/>
 </classpath>

build.xml

@@ -28,7 +28,7 @@
 	</target>
 
 	<target name="compile" depends="download" description="compile the java module overwrites">
-		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar:${lib}/jgrapht-core-1.5.1.jar:${lib}/jungrapht-layout-1.4-SNAPSHOT.jar:${lib}/slf4j-api-1.7.30.jar:${lib}/slf4j-nop-1.7.30.jar:${lib}/commons-lang3-3.12.0.jar"
+		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar:${lib}/jgrapht-core-1.5.1.jar:${lib}/jungrapht-layout-1.4-SNAPSHOT.jar:${lib}/slf4j-api-1.7.30.jar:${lib}/slf4j-nop-1.7.30.jar:${lib}/commons-lang3-3.12.0.jar:${lib}/commons-math3-3.6.1.jar"
            source="1.8"
            target="1.8"
            includeantruntime="false"/>
@@ -79,6 +79,11 @@
 		        <include name="**/*.class"/>
 			</patternset>
 		</unzip>
+		<unzip src="lib/commons-math3-3.6.1.jar" dest="${build}/deps">
+			<patternset>
+		        <include name="**/*.class"/>
+			</patternset>
+		</unzip>
 		<jar jarfile="${dist}/CommunityModules-deps-${timestamp}.jar">
 			<fileset dir="${build}/modules/"
              includes="**/*.class"/>
@@ -123,6 +128,7 @@
 				<pathelement location="${lib}/slf4j-api-1.7.30.jar" />
 				<pathelement location="${lib}/slf4j-nop-1.7.30.jar" />
 				<pathelement location="${lib}/commons-lang3-3.12.0.jar" />
+				<pathelement location="${lib}/commons-math3-3.6.1.jar" />
 				<!-- The jar that has just been built by the dist target. -->
 				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
 			</classpath>

modules/Statistics.tla

@@ -0,0 +1,18 @@
+------------------------- MODULE Statistics -------------------------
+EXTENDS Naturals
+
+ChiSquare(expected, actual, alpha) ==
+    (***************************************************************************)
+    (* Performs a Chi-square goodness of fit test evaluating the null          *)
+    (* hypothesis that the observed counts conform to the frequency            *)
+    (* distribution described by the expected counts, with significance level  *)
+    (* alpha.                                                                  *)
+    (* From:                                                                   *)
+    (* https://commons.apache.org/proper/commons-math/javadocs/api-3.6.1/      *)
+    (* org/apache/commons/math3/stat/inference/ChiSquareTest.html              *)
+    (***************************************************************************)
+    \* TODO: specify the ChiSquare test
+    TRUE
+
+=========================================================================
+

modules/tlc2/overrides/Statistics.java

@@ -0,0 +1,74 @@
+/*******************************************************************************
+ * Copyright (c) 2022 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 org.apache.commons.math3.stat.inference.ChiSquareTest;
+
+import tlc2.output.EC;
+import tlc2.tool.EvalException;
+import tlc2.value.Values;
+import tlc2.value.impl.BoolValue;
+import tlc2.value.impl.FcnRcdValue;
+import tlc2.value.impl.IntValue;
+import tlc2.value.impl.StringValue;
+import tlc2.value.impl.Value;
+
+public class Statistics {
+
+	@TLAPlusOperator(identifier = "ChiSquare", module = "Statistics", warn = false)
+	public static Value chiSquare(Value expected, Value actual, final Value alpha) {
+		expected = expected.normalize().toFcnRcd();
+		if (!(expected instanceof FcnRcdValue)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "first", "ChiSquare", "function", Values.ppr(expected.toString()) });
+		}
+		actual = actual.normalize().toFcnRcd();
+		if (!(actual instanceof FcnRcdValue)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "second", "ChiSquare", "function", Values.ppr(actual.toString()) });
+		}
+		if (!(alpha instanceof StringValue)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "ChiSquare",
+					"StringValue representing a double in (0, .5]", Values.ppr(alpha.toString()) });
+		}
+
+		final double[] exp = Arrays.asList(((FcnRcdValue) expected).values).stream().map(v -> (IntValue) v)
+				.mapToDouble(i -> Double.valueOf(i.val)).toArray();
+
+		final long[] act = Arrays.asList(((FcnRcdValue) actual).values).stream().map(v -> (IntValue) v)
+				.mapToLong(i -> Long.valueOf(i.val)).toArray();
+
+		final double a = Double.valueOf(((StringValue) alpha).val.toString());
+
+		final ChiSquareTest chiSquareTest = new ChiSquareTest();
+		if (chiSquareTest.chiSquareTest(exp, act, a)) {
+			return BoolValue.ValFalse;
+		}
+		return BoolValue.ValTrue;
+	}
+}

modules/tlc2/overrides/TLCOverrides.java

@@ -41,17 +41,18 @@ public class TLCOverrides implements ITLCOverrides {
 	@Override
 	public Class[] get() {
 		try {
-                        // Remove `Json.resolves();` call when this Class is moved to `TLC`.
+			// Remove `Json.resolves();` call when this Class is moved to `TLC`.
 			Json.resolves();
 			return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class,
-                                             FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class };
+					FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class,
+					DyadicRationals.class, Statistics.class };
 		} catch (NoClassDefFoundError e) {
-                        // Remove this catch when this Class is moved to `TLC`.
-			System.out.println(
-					"gson dependencies of Json overrides not found, Json module won't work unless "
+			// Remove this catch when this Class is moved to `TLC`.
+			System.out.println("gson 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[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class,
-                                     FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class };
+		return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class,
+				Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class,
+				Statistics.class };
 	}
 }

tests/AllTests.tla

@@ -16,6 +16,7 @@ EXTENDS SequencesExtTests,
         FoldsTests,
         GraphsTests,
         BagsExtTests,
-        DyadicRationalsTests
+        DyadicRationalsTests,
+        StatisticsTests
 
 ===========================================

tests/StatisticsTests.tla

@@ -0,0 +1,14 @@
+------------------------- MODULE StatisticsTests -------------------------
+EXTENDS Statistics
+
+ASSUME LET T == INSTANCE TLC IN T!PrintT("StatisticsTests")
+
+A ==
+    [ i \in 1..6 |-> i ]
+
+ASSUME( ChiSquare(A, A, "0.001"))
+ASSUME( ChiSquare(A, A, "0.01"))
+ASSUME( ChiSquare(A, A, "0.5"))
+ASSUME(~ChiSquare([ i \in 1..6 |-> 6 ], A, "0.45"))
+ASSUME(~ChiSquare([ i \in 1..6 |-> 6 ], A, "0.5"))
+=============================================================================