TLX.Sequences (TLX v0.5.2)

Copy Markdown

Sequence operation constructors for use in TLA+ expressions.

These require EXTENDS Sequences in the TLA+ module. Use extends [:Sequences] in your spec to include it.

len(s)              # Len(s)
append(s, x)        # Append(s, x)
head(s)             # Head(s)
tail(s)             # Tail(s)
sub_seq(s, m, n)    # SubSeq(s, m, n)
concat(s, t)        # s \o t
seq_set(s)          # Seq(s) — type of finite sequences over s
select_seq(:x, s, pred)  # SelectSeq(s, LAMBDA x: pred)

Summary

Functions

append(s, x)

Append element to sequence: Append(s, x)

concat(s, t)

Sequence concatenation: s \o t

head(s)

First element of sequence: Head(s)

len(s)

Sequence length: Len(s)

select_seq(var, s, pred)

Sequence filter: SelectSeq(s, LAMBDA var: pred) in TLA+.

seq_set(s)

Set of all finite sequences over s: Seq(s) (type constraint).

sub_seq(s, m, n)

Subsequence: SubSeq(s, m, n)

tail(s)

All but first element: Tail(s)

Functions

append(s, x)

Append element to sequence: Append(s, x)

concat(s, t)

Sequence concatenation: s \o t

head(s)

First element of sequence: Head(s)

len(s)

Sequence length: Len(s)

select_seq(var, s, pred)

Sequence filter: SelectSeq(s, LAMBDA var: pred) in TLA+.

Var-first signature mirrors filter/3, choose/3, set_map/3 — the binding variable is always the first argument for three-arg binding operators in TLX.

seq_set(s)

Set of all finite sequences over s: Seq(s) (type constraint).

sub_seq(s, m, n)

Subsequence: SubSeq(s, m, n)

tail(s)

All but first element: Tail(s)