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

*From*: robmi...@xxxxxxxxx*Date*: Sat, 5 Dec 2015 14:49:00 -0800 (PST)

I am new to TLA. I have a variable called x which should increase or stay the same at each new state. I thought I would put this in the invariant and it would work but it didn't. x' >= x. It doesn't know what x is. How do I check for this? Thanks.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] TLA+ logic** - Next by Date:
**quick question about TLA** - Previous by thread:
**Re: [tlaplus] TLA+ logic** - Next by thread:
**Re: How to check if a variable increases or stays the same at each new state?** - Index(es):