Re: [tlaplus] Creating function sets lazily

[tlaplus-google-group@xxxxxxxxxxx]

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.