Relations as Ordered Tuples

Alloy represents relations as sets of ordered tuples, and it can some times be useful to think of them this way. Intuitively, this is just an exhaustive list of every way to legally fill in the relation.

A (binary) relation mapping file system objects to their parent directories is really a set of ordered pairs. The first entry in each pair is a file system object and the second is its parent directory. In one instance, it's entries might look like this:

{< fileA, DirA >,
 < fileB, DirB >,
 < fileC, DirA >}

Now consider a relation that maps pairs of nodes in a network to their cost. This relation would be said to have arity 3, and its tuples might look like this:

{< nodeA, nodeB, 100 >,
 < nodeA, nodeC, 25 >,
 < nodeB, nodeD, 37 >,
 < nodeC, nodeD, 14 >}

Of course, if we didn't write sufficient constraints on the model, the relaion might have more than one cost per pair:

{< nodeA, nodeB, 100 >,
 < nodeA, nodeB, 50 >,
 < nodeA, nodeC, 14 >,
 < nodeC, nodeA, 37 >}

Since relations are just sets, you can take intersections, unions, set differences, and so on on them, just like any other sets. For instance, you might have a relation roads, which is an arity-2 relation on cities, stating which one have roads connecting them. It's tuples might look like this:

{< cityA, cityB >
 < cityA, cityC >
 < cityB, cityD >
 < cityC, cityD >}

There might be another relation dirtRoads which is also a relation on pairs of cities. We might write the constraint

  fact physicalWorld {
    //dirt roads are roads
    dirtRoads in roads

    //roads are two-way
    roads = ~roads
    dirtRoads = ~dirtRoads
  }

The ~ operator reverses a relation by reversing the tuples in the relation. Thus our earlier sample falue for roads did not satisfy the physicalWorld fact. It should have been

{< cityA, cityB >
 < cityB, cityA >
 < cityA, cityC >
 < cityC, cityA >
 < cityB, cityD >
 < cityD, cityB >
 < cityC, cityD >
 < cityD, cityC >}

We also might want to talk about non-dirt roads, by writing something like this:

  all r:(roads - dirtRoads) | r.foo ...

If dirtRoads were

{< cityC, cityD >
 < cityD, cityC >}

then (roads - dirtRoads) would have to be

{< cityA, cityB >
 < cityB, cityA >
 < cityA, cityC >
 < cityC, cityA >
 < cityB, cityD >
 < cityD, cityB >

and r might be any of those tuples.

You can compose two relations, A and B, to create a new relation, A.B. Each tuple ab of the new relation is created by taking a tuple a from A and a typle b from B where the last entry in a matches the first entry in b. Concatenate the tuples, but leave out the matched entry.