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

[tlaplus] Re: Creating function sets lazily

Sorry, I meant hash["b"].

On Tuesday, February 22, 2022 at 10:16:56 PM UTC-5 thomas...@xxxxxxxxx wrote:
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/99b0f219-d423-4d48-b92e-0a25542bb048n%40googlegroups.com.