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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Fri, 19 May 2017 11:58:05 +0200*References*: <b60fab65-1be5-40a4-ae73-05d61de7a616@googlegroups.com> <02A9A052-C23B-4AB6-ABB7-1EFBB5F70AFD@gmail.com> <fa1e2fbf-7605-4bbb-bb01-9dab9f6a854a@googlegroups.com>

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

**References**:**Paramaterized Instantiation and Universal Quantification***From:*Adam Shimi

**Re: [tlaplus] Paramaterized Instantiation and Universal Quantification***From:*Stephan Merz

**Re: [tlaplus] Paramaterized Instantiation and Universal Quantification***From:*Adam Shimi

- Prev by Date:
**Re: [tlaplus] Paramaterized Instantiation and Universal Quantification** - Next by Date:
**Re: Paramaterized Instantiation and Universal Quantification** - Previous by thread:
**Re: [tlaplus] Paramaterized Instantiation and Universal Quantification** - Next by thread:
**Re: Paramaterized Instantiation and Universal Quantification** - Index(es):