[tlaplus] Specifying an arbitrary function and then using it in TLC

[Vic Putz <vbputz@xxxxxxxxx>]

In https://groups.google.com/u/1/g/tlaplus/c/jnlmYhh4jmo/m/HTGFDZimCAAJ, when asked about a generic hash function in TLA, Ron Pressler wrote:

> Unless what you're specifying is at the level of the hash function itself, you might be

> thinking about this at too-low a level. If the algorithm you're specifying should work with 

> any hash function, make that a part of your specification: ∃ hash ∈ [Source → Bits].... If 

> there are other requirements on the hash, add them to the quantifier. 

Which is a lovely high-level way to specify that such a function exists.  I'm facing something similar in a toy spec I'm trying to write for a transpiler, where I can say there exists such a function mapping instructions on architecture A to those on Architecture B, something like ∃ TranslateFn ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B].  Good so far.

I'd like to use that function in a TLC model, but just using the existential quantifier doesn't expose TranslateFn.  So the next thing that looks right is TranslateFn == CHOOSE f  ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B] : TRUE , because I don't care what that function is, just that there is one and that I can use it.

But won't that ask TLC to (senselessly?) explore the whole space of possible mapping functions?  If so, is there a way around that?

Cheers; still learning (slowly...)

-- 
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/df467f71-77d1-4bed-a83c-d126d5da226fn%40googlegroups.com.