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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

--
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/1db3377c-78a4-3e97-5f16-76bc701ca3f1%40lemmster.de.