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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 23 Feb 2022 08:18:03 +0100*References*: <aa184e59-2e0c-44d9-a2c3-ea631681edean@googlegroups.com>

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
--
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. |

**Follow-Ups**:**Re: [tlaplus] Creating function sets lazily***From:*tlaplus-google-group

**Re: [tlaplus] Creating function sets lazily***From:*Igor Konnov

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

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