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

[tlaplus] CHOOSEing a function with a unique range for each element of the domain.

Hi All,

I would like to have a function that has a unique range for each element in the domain (e.g. like an ideal hash function).

I was trying to CHOOSE my way into a function:

BitString == [1..4 -> {0,1}]
hash == CHOOSE i \in [0..3 -> BitString] : \A x, y \in 0..3: x /=y /\ i[x] /= i[y]

But when I try running hash[2] in the evaluator, I get this error:

Attempted to compute the value of an _expression_ of form
CHOOSE x \in S: P, but no element of S satisfied P.

Anyone have an idea of how I can get my desired effect?

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/78987ad6-5fb6-44d9-954f-eeef74557477n%40googlegroups.com.