How to end an increacing number TLA+ specification?

[than...@gmail.com]

Hi all,
I have meet a problem in TLA+. Some algorithm use an increasing number to ensure it correntness. A simple specification like bellow, as the TLC model checking process of the exapmle specification never ends, so we can not conclude the result of the specification.

My question is how to modify the specification the let it end gracefully? Is it a typical case and have a known solution?

Thanks.





VARIABLES a, b

vars == << a, b >>

Init == (* Global variables *)
/\ a = 1
/\ b = 2

Next == \/ /\ a' = a + 2
/\ b' = b
\/ /\ b' = b + 2
/\ a' = a

Spec == Init /\ [][Next]_vars

Invariant == a /= b

[Leslie Lamport]

In the Toolbox's Help pages' table of contents, go to
 

   TLA+ Toolbox Guide > Model Checking > Creating a Model > Advanced Options Page

and read the section about state constraints.