As I'm new to alloy, this is most likely a simple question. I've been through the on-line tutorials and am now reading the Software Abstractions, revised edition. On page 34 there is an example at the bottom of the page:
r' = {b:B, a:A, c:C | a->b->c in r}
where the text says that this defines a new relation of B->A->C. I don't see how an explicit order for r' is achieved by this statement.
It's the property of set comprehension
{a: A | somePredicate1[a]} is of type A and returns a set containing all atoms for which somePredicate1 holds;{a: A, b: B | somePredicate2[a, b]} is of type A->B and returns a relation containing all a->b tuples for which somePredicate2 holds;The syntax of set comprehension basically consists of two parts (1) type declaration (before the | character), and (2) predicate which must hold for every element in the returned set.
