Add TLCExt!TLCFP operator that equals the (lower 32 bit) value that TLC

gives to the given input when the value is being fingerprinted. [Feature][TLC] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
tlaplus · Aug 25, 2023 · ddec63c · ddec63c
1 parent 42c3587
commit ddec63c
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 2 deletions.
diff --git a/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLCExt.tla b/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLCExt.tla
@@ -1,6 +1,7 @@
 ------------------------------- MODULE TLCExt -------------------------------
 
 LOCAL INSTANCE TLC
+LOCAL INSTANCE Integers
   (*************************************************************************)
   (* Imports the definitions from the modules, but doesn't export them.    *)
   (*************************************************************************)
@@ -45,7 +46,7 @@ Trace ==
 
 -----------------------------------------------------------------------------
 
-(* HERE BE DRAGONS! The operators below are experimental! *)
+(* HERE BE DRAGONS! The operators below are experimental! You will probably not need them! *)
 
 CounterExample ==
     (****************************************************************************)
@@ -153,4 +154,12 @@ TLCCache(expression, closure) ==
   (******************************************************************************)
   expression
 
+TLCFP(var) ==
+  (******************************************************************************)
+  (* Equals the value that TLC gives to the given input when the value is       *)
+  (* being fingerprinted.                                                       *)
+  (* Implementation note: Equals the lower 32 bits until TLC supports longs     *)
+  (******************************************************************************)
+  CHOOSE i \in Int: TRUE
+
 ============================================================================
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java b/tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java
@@ -53,10 +53,12 @@
 import tlc2.tool.coverage.CostModel;
 import tlc2.tool.impl.Tool;
 import tlc2.util.Context;
+import tlc2.util.FP64;
 import tlc2.util.IdThread;
 import tlc2.value.Values;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.CounterExample;
+import tlc2.value.impl.IntValue;
 import tlc2.value.impl.ModelValue;
 import tlc2.value.impl.RecordValue;
 import tlc2.value.impl.StringValue;
@@ -345,4 +347,12 @@ public static Value tlcEval2(final Tool tool, final ExprOrOpArgNode[] args, fina
 		// expression--nothing is cached!
 		return null; // Returning null here causes Tool.java to evaluate the original expression.
 	}
+
+	@TLAPlusOperator(identifier = "TLCFP", module = "TLCExt", warn = false)
+	public static synchronized IntValue tlcFingerprint(final Value val) {
+		val.deepNormalize();
+		// TLC has no value to represent a long, thus, downcast to int.
+		// However, note tla2sany.semantic.NumeralNode#bigVal
+		return IntValue.gen(FP64.Hash(val.fingerPrint(FP64.New())));
+	}
 }
diff --git a/...rt.tlatools/test/tlc2/tool/doinitfunctor/DoInitFunctorInvariantMinimalErrorStackTest.java b/...rt.tlatools/test/tlc2/tool/doinitfunctor/DoInitFunctorInvariantMinimalErrorStackTest.java
@@ -45,7 +45,7 @@ public void testSpec() {
 		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "1", "1", "1"));
 
 		assertTrue(recorder.recordedWithStringValues(EC.TLC_MODULE_ARGUMENT_ERROR_AN,
-				"first", ">", "integer", "<<1, 1>>"));
+				"first", ">=", "integer", "<<1, 1>>"));
 
 		String errorStack = "0. Line 8, column 3 to line 9, column 13 in DoInitFunctorMinimalErrorStack\n"
 				+ "1. Line 8, column 6 to line 8, column 25 in DoInitFunctorMinimalErrorStack\n"