[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Surjective functions as records

Hi all,

I can filter a set of functions to contain just the surjective functions like this:

{m \in [1..2 -> 3..4] : \A j \in 3..4 : \E i \in DOMAIN m: m[i] = j}

yielding the expected result:

{<<3, 4>>, <<4, 3>>}

When I try the same filtering with surjective records:

{m \in [a: 3..4, b: 3..4] : \A j \in 3..4 : \E i \in DOMAIN m: m.i = j}

the following error message is displayed:

The `Evaluate Constant _expression_� section�s evaluation failed.

Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.Value tlc2.module.TLC.PrintT(tlc2.value.impl.Value),
but it produced the following error:
Attempted to select nonexistent field "i" from the record
[a |-> 3, b |-> 3]

What is the reason for this different behaviours?

Advices are appreciated,

Siegfried Bublitz

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAL%2B9cEp8ke8AcfpRHfrazmcOSuPcv6Ac5bvXGuvMVYRXR0mr3g%40mail.gmail.com.