Monotonic sequence in TLA+

Graham Hay

I wanted to declare an invariant, that a sequence was monotonic, i.e. always increasing. <<1, 2, 3>> would pass, as would <<1, 3, 5>>; but <<1, 2, 1>> would not.

I thought I might be able to use forall:

MonotonicSeq ==
    IF Len(seq) > 1 THEN
        \A e \in Tail(seq):
            e > Head(seq)
    ELSE TRUE

but was quickly disillusioned:

Error: Evaluating invariant MonotonicSeq failed.
TLC encountered a non-enumerable quantifier bound
<<2>>.

Apparently that syntax only works with sets.

Eventually I worked out how to write a recursive operator:

RECURSIVE Monotonic(_)

Monotonic(seq) ==
    IF Len(seq) > 1 THEN
        /\ Len(SelectSeq(seq, LAMBDA X : X < Head(seq))) = 0
        /\ Monotonic(Tail(seq))
    ELSE TRUE

Leave a comment