From b583fa26aad7517098750c0b074fa849d0727f99 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 3 Oct 2026 14:17:03 -0700 Subject: [PATCH] Make the IsInjective override accept records and lazy functions Fall back to toFcnRcd, which also converts records and function constructors that TLC has not yet evaluated to an explicit function. Fixes tlaplus/model-checker-hardening Github issue #196 https://github.com/tlaplus/model-checker-hardening/issues/196 [Bug] Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- modules/tlc2/overrides/Functions.java | 8 +++++--- tests/FunctionsTests.tla | 7 +++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/modules/tlc2/overrides/Functions.java b/modules/tlc2/overrides/Functions.java index 106c00f..34d573f 100644 --- a/modules/tlc2/overrides/Functions.java +++ b/modules/tlc2/overrides/Functions.java @@ -65,9 +65,11 @@ public static BoolValue IsInjective(final Value val) { if (val instanceof SetOfRcdsValue) { // Input e.g. [a: 1, b: 2] return isInjectiveNonDestructive(((SetOfRcdsValue) val).values); - } else if (val instanceof FcnRcdValue) { - // Input e.g. [a |-> 1, b |-> 2] - return isInjectiveNonDestructive(((FcnRcdValue) val).values); + } + final Value fcn = val.toFcnRcd(); + if (fcn instanceof FcnRcdValue) { + // Input e.g. [a |-> 1, b |-> 2] or [x \in BOOLEAN |-> x] + return isInjectiveNonDestructive(((FcnRcdValue) fcn).values); } throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, new String[] { "IsInjective", "function", Values.ppr(val.toString()) }); diff --git a/tests/FunctionsTests.tla b/tests/FunctionsTests.tla index 69f54b8..3d566bd 100644 --- a/tests/FunctionsTests.tla +++ b/tests/FunctionsTests.tla @@ -33,6 +33,12 @@ ASSUME(IsInjective([i \in 0..2 |-> i])) ASSUME(IsInjective( "a":> [{1,2} -> {3,4}] @@ "b":> [{1,2} -> {3,5}] )) ASSUME(AssertError("The argument of IsInjective should be a function, but instead it is:\n{}", IsInjective({}))) +ASSUME(IsInjective([a |-> 1, b |-> 2])) +ASSUME(~IsInjective([a |-> 1, b |-> 1])) +\* The function constructor is not evaluated to an explicit function in this context. +ASSUME((IF IsInjective([b \in BOOLEAN |-> FALSE]) THEN <<1>> ELSE <<2>>)[1] = 2) +ASSUME((IF IsInjective([b \in BOOLEAN |-> b]) THEN <<1>> ELSE <<2>>)[1] = 1) + \* Assert that Functions#isInjectiveDestructive is side-effect free. SomeSeq == UNION {[1..m -> {1,2}] : m \in 0..Cardinality({1,2})} SomeExp == CHOOSE x \in SomeSeq: IsInjective(x) /\ Len(x) > 3 @@ -43,6 +49,7 @@ ASSUME IN /\ \A f \in [{0,1,2} -> {0,1,2,3}] : IsInjectivePure(f) = IsInjective(f) /\ \A f \in [{"a","b","c"} -> {0,1,2,3}] : IsInjectivePure(f) = IsInjective(f) /\ \A f \in [{0,1,2,3} -> {"a","b","c"}] : IsInjectivePure(f) = IsInjective(f) + /\ \A f \in [a : {0,1,2}, b : {0,1,2}, c : {0,1,2}] : IsInjectivePure(f) = IsInjective(f) ASSUME FoldFunction(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = {1,2}