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

How to check if a variable increases or stays the same at each new state?

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?