On Wednesday, November 25, 2020 at 1:55:18 PM UTC-5 Markus Alexander Kuppe wrote:
On 25.11.20 10:31, Stephan Merz wrote:
> 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.
With the new-ish Randomization module [1,2], you could trick TLC to
check a more "interesting" subset of all functions.
Markus
[1]
https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/Randomization.tla
[2] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf