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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 19:31:49 +0100*References*: <df467f71-77d1-4bed-a83c-d126d5da226fn@googlegroups.com>

CHOOSE is arbitrary but deterministic choice. In other words, with your definition, TLC will generate one function (likely a very trivial one, perhaps mapping every instruction of A to the same instruction of B) and explore the spec for that particular function. If you want to explore the spec for every possible function, make the mapping a variable of your spec, add translateFn \in [...] to the initial condition and UNCHANGED translateFn to all actions. And if you want to play with different hand-picked functions, add a CONSTANT TranslateFn to your module and write ASSUME TranslateFn \in [...] then you define the particular function in the model. What is the right way to go depends on whether you want to explore if your transpiler works for some fixed function, for all functions or for some specific ones. 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/32D3FDF4-6067-44C3-97E3-77595B362A48%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC***From:*Markus Kuppe

**References**:

- Prev by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Next by Date:
**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC** - Previous by thread:
**[tlaplus] Specifying an arbitrary function and then using it in TLC** - Next by thread:
**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC** - Index(es):