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

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



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