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

[thomas...@gmail.com]

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?

[tlaplus-go...@lemmster.de]

https://github.com/tlaplus/CommunityModules/blob/07ef2bc96e2af839318bbd96ae3ef7b80985f5b4/modules/Functions.tla#L42-L49

Markus

[thomas...@gmail.com]

That worked...thanks!