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>

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
+
 ============================================================================

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())));
+	}
 }