Re: [tlaplus] Paramaterized Instantiation and Universal Quantification

[Adam Shimi <hardke...@xxxxxxxxx>]

Hi Stephan,

First, thanks a lot for your prompt and accurate answer !

You are completely right : my mental model of All was based on a call-by-name semantics instead of the obvious call-by-value.

As for the canonical encoding of general specification, I indeed thought about that (or Sequences, but these are only functions from Nat to my values' type). But the transitions of my actual specification are not atomic with respect to all my s0, s1, etc variables. Thus, I cannot use it for my purpose.

I guess not, but I am curious : is there some call-by-name mecanisms in TLA+ ?

Thanks in advance, and have a good day.
Adam