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

*From*: "thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>*Date*: Tue, 22 Feb 2022 19:16:56 -0800 (PST)

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)

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.

**Follow-Ups**:**Re: [tlaplus] Creating function sets lazily***From:*Stephan Merz

**[tlaplus] Re: Creating function sets lazily***From:*thomas...@xxxxxxxxx

- Prev by Date:
**Re: [tlaplus] TLA+ on Mac questions:** - Next by Date:
**[tlaplus] Re: Creating function sets lazily** - Previous by thread:
**Re: [tlaplus] TLA+ on Mac questions:** - Next by thread:
**[tlaplus] Re: Creating function sets lazily** - Index(es):