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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 3 Sep 2016 17:23:11 +0200*References*: <b4f7d7bf-7fe5-44c3-a034-f8eca4d3a5be@googlegroups.com> <36514f56-6c98-443a-8254-3df839772bb3@googlegroups.com>

In TLA jargon, it's a "variable". In contrast to a "constant", whose value is fixed by the model, independently of the state, variables may be assigned different values in different states. Thus, your formula is valid if x and y are declared as CONSTANTS, but not if at least one of them is a VARIABLE. Stephan |

**Follow-Ups**:**Re: [tlaplus] Curious oddity***From:*fl

**References**:**Curious oddity***From:*fl

**Re: Curious oddity***From:*fl

- Prev by Date:
**A site** - Next by Date:
**Re: [tlaplus] Curious oddity** - Previous by thread:
**Re: Curious oddity** - Next by thread:
**Re: [tlaplus] Curious oddity** - Index(es):