domain and range of a relation operation in Alloy

Question

Is there any operation that returns range and domain of a relation in Alloy.

Suppose I have a sig defined in Alloy as bellow:

sig A {r : B }

sig B {}

I am looking for and operation to be applied on r and give me B (probably something like r[B] that returns B)

The above situation might seem stupid as r[B] would return B, so why I am not using B at first place! Actually I find having a range and domain operations(if they ever exist) very useful in writing facts (constraints). e.g.:

sig O {sup:O}

sig M{mid: O, sup:O} {mid.sup=sup}

sig F{fid:O, sup:O}{fid.sup=sup}


fact K{
   all o:O | lone so:M | so.mid=o 
   all o:O | lone so:F | so.fid=o
   all o:O | one i:(fid+mid) | o in i[O]   //I want to say fid+mid is injective, so expecting i[O] return range of i
 }

any idea? :)

Answer 1

You will find range and domain functions for binary relations in the library module relation.als under the names ran and dom respectively. There are brief discussions in sections 3.2.5 and 3.4.3.6 of Daniel Jackson's book on Software Abstractions.

On the other hand, you can also do without the library functions. For any binary relation r, the domain and range of r can also easily be expressed as r.univ and univ.r, respectively. Using the box operator instead of dot, the range can also be expressed as r[univ]. (Note that your example r[B] will return nothing, because it's equivalent to B.r and nothing in B matches the first item of any pair in R (since the first items are all in A, not B, and in the example A and B are disjoint). If you want the subset of B which occur in the pairs of r, you want to write A.r, or equivalently r[A]. In this case, since the first item in r is always an element of A, A.r is equivalent to univ.r.

Note that the words domain and range have multiple usages. The term domain is used sometimes to denote the set of things which appear as the first item in the pairs of a relation (and range similarly for the set of things appearing as the second item in any pair), and sometimes to denote the set of things which might appear as the first (second) item in a pair. Both the library functions and the expressions r.univ and univ.r evaluate to domains and ranges in the first sense, not the second. In terms of your first example, in Alloy the domain of the relation r is not necessarily equal to the set B; it can also be a proper subset of B.

---

[Addendum] To check that the relation fid + mid is injective, one simple way would be to write

fact {
  all o : O | lone x : M + F | x.mid = o or x.fid = o
}

Use one instead of lone if you want to assert that fid + mid is also total over M + F; I don't understand 'injective' to entail that.

A terser formulation might take a more 'relational' style:

lone (mid + fid).o

Recast in this idiom, your fact would read

fact mid_fid_injective {
  all o : O | lone mid.o
  all o : O | lone fid.o
  all o : O | lone (mid + fid).o
}

But of course the first and second statements here are implied by the third, so you could get by with

fact mid_fid_injective {
  all o : O | lone (mid + fid).o
}