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

What Stephan did not mention is that you can have TLC check your condition by simply entering [][x' >= x]_x as a property to check in the Properties part of the Model Overview page. Since x is a variable of your spec, there is no need to declare it elsewhere.

Leslie

On Sunday, December 6, 2015 at 1:46:41 AM UTC-8, Stephan Merz wrote:

It is a bit hard to understand from your posting what exactly you are trying to achieve. The property that you state is expressed in TLA+ as the temporal formula

Monotonic == [][x' >= x]_x

This definition of formula Monotonic would appear in a TLA module that contains a declaration

VARIABLE x

Now the question is what algorithm Monotonic is a property of. For example, you could write the specification

CONSTANT N

Init == x = 0
Next == x < N /\ x' = x+1
Spec == Init /\ [][Next]_x

and use TLC to check that

Spec => Monotonic

holds (by entering Monotonic as a property to be checked of specification Spec). TLC will require you to instantiate the parameter N, say by the number 10. This is necessary so that the instance that TLC verifies has a finite state space.

There are many other algorithms that satisfy property Monotonic. In TLA+, there is no formal distinction between specifications and properties of algorithms: both are expressed using temporal formulas. These concepts and many more are explained in the TLA+ documentation that is available on the Web, in particular the TLA+ Hyperbook.

Regards,
Stephan