Sequences

Sequences are ordered lists of elements in TLA+. You need to EXTENDS Sequences to use sequence operators.

Creating Sequences

<<1, 2, 3>>         \* a sequence of three elements

<<>>                 \* the empty sequence
<< "hello" >>       \* a sequence with one element

Sequences are 1-indexed:

s[1]                 \* first element

s[Len(s)]            \* last element

Operator

Meaning

`Len(s)`	Length of s
`Head(s)`	First element
`Tail(s)`	All elements except the first
`Append(s, e)`	Add e to the end
`s \o t`	Concatenate sequences s and t
`SubSeq(s, m, n)`	Subsequence from index m to n

A sequence is actually a function from 1..n to values. So DOMAIN s = 1..Len(s).

Stack (LIFO):

Push(s, e) == <<e>> \o s

Pop(s)     == Tail(s)
Peek(s)    == Head(s)

Queue (FIFO):

Enqueue(s, e) == Append(s, e)

Dequeue(s)    == Tail(s)
Front(s)      == Head(s)

The spec on the right models a simple bounded stack.