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

Re: [tlaplus] Creating function sets lazily


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 ) ]:


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