A new reserved keyword “seq” has been added for declaring a field as a sequence of atoms. In the following example, for each person p, “p.books” is a sequence of Book:

sig Book { }
sig Person {
	books: seq Book
}

The actual type of a sequence of Book is “Int->Book”. So if s is a sequence of Book, then the first element is s[0] and you can get the set of all elements by writing “univ.s”

You can also use “seq” in existential quantifications, like this:

some s: seq Book | FORMULA

Currently, the Alloy Analyzer does not support analysis of a model with universal quantifiers over sets or relations (including sequences).

You can also use “seq” in function argument declaration, like this:

fun getAllElements [s: seq Book] : set Book {
  univ.s
}

Just like the other multiplicity symbols, when you use “seq” in a function argument declaration, we do not enforce that you always call the function/predicate with a well-formed sequence. So it is only for documentation purpose, to denote s is a binary relation from Int->Book.

Note: for effifiency, we bound the length of allowed sequences. You can change this bound by setting the scope on “seq”. For example, if you want to allow sequences of up to 4 elements, you write

check SomeAssertion for 4 seq

To make it easier to manipulate sequences, we provide a number of helper functions: (these are defined in the pre-included util/sequniv.als file)

Feature Description
#s Return the number of elements in sequence s.
s.elems Return the set of elements in sequence s.
s.first If #s > 0, it returns the first element of s. Otherwise, it returns the empty set
s.last If #s > 0, it returns the last element of s. Otherwise, it returns the empty set
s.rest If #s > 1, it returns s with its first element removed. Otherwise, it returns the empty sequence
s.butlast If #s > 1, it returns s with its last element removed. Otherwise, it returns the empty sequence
s.isEmpty It returns true if #s==0.
s.hasDups It returns true if s contains duplicate elements.
s.inds If #s > 0, it returns the set of integers {0 .. (#s)-1}. Otherwise, it returns the empty set
s.lastIdx If #s > 0, it returns the integer (#s)-1. Otherwise, it returns the empty set
s.afterLastIdx If (#s < the longest allowed sequence length), it returns #s. Otherwise, it returns the empty set
s.idxOf [x] If x does not appear in s, it returns the empty set. Otherwise, it returns the first index where x appears in s.
s.lastIdxOf [x] If x does not appear in s, it returns the empty set. Otherwise, it returns the last index where x appears in s.
s.indsOf [x] If x does not appear in s, it returns the empty set. Otherwise, it returns the set of indices where x appears in s.
s.add [x] If (#s < the longest allowed sequence length), it appends x to s. Otherwise, it returns s.
s.setAt [i, x] Precondition: 0 <= i <= #s. It returns a new sequence where the i-th entry is changed to x. Unsatisfiable if precondition is not satisfied.
s.insert [i, x] Precondition: 0 <= i <= #s. It returns a new sequence where x is inserted at index i. Unsatisfiable if precondition is not satisfied. Note: if #s was already equal to the longest allowed sequence length, then the last element of s will be removed first.
s.delete [i] Precondition: 0 <= i. It returns the result of deleting the element at index i. Unsatisfiable if precondition is not satisfied. Note: if i >= #s, the input sequence is returned.
a.append [b] Returns the result of concatenating sequence a and sequence b. (If the resulting sequence is too longer, it will be truncated)
s.subseq [from, to] Returns the subsequence between from and to, inclusively. Note: if the bounds are not within the sequence’s limits, i.e., from < 0 or to >= #s, then the empty sequence is returned.