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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sun, 6 Dec 2015 01:46:41 -0800 (PST)*References*: <0aabd690-0038-48a0-b1d9-018fd383324d@googlegroups.com>

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

**Follow-Ups**:**Re: How to check if a variable increases or stays the same at each new state?***From:*Leslie Lamport

**References**:

- Prev by Date:
**Re: quick question about TLA** - Next by Date:
**Recursive definitions of higher-order operators** - Previous by thread:
**How to check if a variable increases or stays the same at each new state?** - Next by thread:
**Re: How to check if a variable increases or stays the same at each new state?** - Index(es):