I would like to know, how can I define a pair and a sequence of pair in alloy? For example, in the Z notation, we can have a variable definition like c as a sequence of pairs, ie, "c: seq (A \cross B)". Is there any equivalent to this definition in the alloy language?
Alloy is pretty expressive, and often you can translate directly from Z into Alloy. In this case, for example, you could declare a signature representing the pairs
sig Pair {first, second: X}
and then define a field as a sequence of pairs
s: seq Pair
But usually there's a better way of doing it. For example, maybe having two sequences is better; maybe the sequences can be represented as orderings; or maybe you don't need sequences at all and sets will do. Generally this is what people find when modeling with Alloy: that making things simpler for analysis makes things easier to understand and express too. Good luck!