[tlaplus] Creating function sets lazily

["thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>]

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.

-- 
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/aa184e59-2e0c-44d9-a2c3-ea631681edean%40googlegroups.com.