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

Re: [tlaplus] Paramaterized Instantiation and Universal Quantification

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.