I have the following code in my TLA+ spec:
BitString == [1..6 -> {0,1}]
AllowedStrings == {"a", "b", "c", "d", "e"}
IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
hash == CHOOSE i \in [AllowedStrings -> BitString] : IsInjective(i)
I then run hash[2] in the evaluator.
This works as expected, but it takes an *extremely* long time to run, and if I increase my domain (e.g. adding "f" to AllowedStrings), it gives me an error:
Attempted to construct a set with too many elements (>100000000)
I understand the combinatorial complexity makes these giant sets, but I was wondering if there's a way to avoid generating all the sets once it gets something that satisfies CHOOSE.