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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 6 Dec 2015 09:06:06 -0800 (PST)*References*: <0aabd690-0038-48a0-b1d9-018fd383324d@googlegroups.com> <aac30bc0-291c-4f41-8346-0b3758361be0@googlegroups.com>

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 formulaMonotonic == [][x' >= x]_xThis definition of formula Monotonic would appear in a TLA module that contains a declarationVARIABLE xNow the question is what algorithm Monotonic is a property of. For example, you could write the specificationCONSTANT NInit == x = 0Next == x < N /\ x' = x+1Spec == Init /\ [][Next]_xand use TLC to check thatSpec => Monotonicholds (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

**References**:**How to check if a variable increases or stays the same at each new state?***From:*robmi . . .

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

- Prev by Date:
**Re: Recursive definitions of higher-order operators** - Next by Date:
**Re: Recursive definitions of higher-order operators** - Previous by thread:
**Re: 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):