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

*From*: tlaplus-google-group@xxxxxxxxxxx*Date*: Wed, 23 Feb 2022 10:38:56 -0800*References*: <aa184e59-2e0c-44d9-a2c3-ea631681edean@googlegroups.com> <B7126745-9C62-44D7-868E-D439C81331CD@gmail.com>

Hi, the definition of this hash function maps a universe of six elements to 2^6 bits. Unless this is intentional, you could, e.g., use the identity hash function [ s \in AllowedStrings |-> s ], which is also a perfect hash function. For readers, assume that hash is injective. Anyway, to expand on Stephan's solution, below is a definition that TLC evaluates quickly. You can use it to define the CONSTANT hash or re-define the original operator hash: EXTENDS Randomization, FiniteSets [...] SomeHash == \* Run TLC with the same -fp and -seed for RandomSubset to pick the same subset. CHOOSE f \in [ AllowedStrings -> RandomSubset( Cardinality(AllowedStrings), BitString ) ]: IsInjective(f) Markus > On Feb 22, 2022, at 11:18 PM, Stephan Merz <stephan.merz@xxxxxxxxx> wrote: > > 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. -- 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/37C102CD-B2FE-4299-83B8-4097611024A0%40lemmster.de.

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

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

- Prev by Date:
**Re: [tlaplus] Creating function sets lazily** - Next by Date:
**[tlaplus] Defining multiple possible actions in one line** - Previous by thread:
**Re: [tlaplus] Creating function sets lazily** - Next by thread:
**[tlaplus] Defining multiple possible actions in one line** - Index(es):