Re: [tlaplus] Creating function sets lazily

BitString has 2^6 elements, and [AllowedString -> BitString] therefore has (2^6)^5 = 2^30 elements. TLC enumerates these sets, and then evaluates IsInjective for each one of them. One could try to speed this up, as you suggest, but CHOOSE should also satisfy the axiom of determinacy

S = T /\ (\A x \in S : P(x) <=> Q(x) => (CHOOSE x \in S : P(x)) = (CHOOSE x \in T : Q(x))

and evaluate to the same value even if the sets and predicates are presented differently. (TLC already doesn't fully guarantee this.)

As long as the CHOOSE operator only occurs in constant definitions as in this example, you may consider replacing hash by a constant parameter and write

CONSTANT hash

ASSUME hash \in [AllowedStrings -> BitString] /\ IsInjective(hash)

You'll have to provide a hash function in the model, but anyway TLC only checks the spec for one fixed hash function even with the definition. Evaluating the ASSUME clause should take negligible time.

Stephan

On 23 Feb 2022, at 04:16, thomas...@gmail.com <thomasgebert@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/aa184e59-2e0c-44d9-a2c3-ea631681edean%40googlegroups.com.

--
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/B7126745-9C62-44D7-868E-D439C81331CD%40gmail.com.