Re: [tlaplus] Paramaterized Instantiation and Universal Quantification

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi Adam,

> 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.

not sure I understand this: the actions of a TLA+ specifications must correspond to atomic transitions. But I leave it to you to figure out if you can adapt the function-based approach or not.

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

No, the point of TLA+ is to be declarative (what Leslie calls "simple math"). Programming language semantics are much more complicated than that. Of course, you can model references explicitly – just like you'd model memory cells – but your spec will become much more complicated as well.

Best regards,
Stephan