Search code examples
alloy

Disjoint union of two signatures in Alloy

I already asked about the Cartesian product and disjoint union in Alloy here . There, I considered sets as unary defined predicates.

What if I simple want to disjoint union two simple signatures in Alloy.

suppose I have the following signatures:

sig A {}
sig B {}

I would like to define a relation from A to B Û B, where I used Û for disjoint union. Is this possible directly in alloy?

Solution

  • I can think of two approaches. (But I realize, re-reading your question that I have no idea what your last paragraph means. So perhaps this is all irrelevant to your goals.)

    First: A disjoint union labels each member with a flag so you know which parent set it came from, and so that no element in the disjoint union is in both parent sets. If the point of the exercise is to ensure that you know what parent set each member of the disjoint union came from, and to ensure that no member of the disjoint union came from more than one parent set, then in this case, normal union seems to do what you need. In your example, signatures A and B are already disjoint, and it's always possible to tell whether a given atom is in A or in B. So the first approach is just to use the expression A + B.

    Second: If A + B won't do, for reasons not given in the question, and you really really want a set of pairs, then define that set of pairs. In each pair, either the first element is from A and the second element is 1 (or some other flag) or else the first element is from B and the second element is 2 (or some other flag).

    One way to write this would be:

    {v : X + Y, n : Int | (v in X and n = 1) or (v in Y and n = 2) }

    Another equivalent way would be:

    {x : X, y : Int | y = 1}
+
{x : Y, y : Int | y = 2}

    A third way is even simpler: 

    {v : X, n : 1} + {v : Y, n : 2}

    And simpler yet:

    (X -> 1) + (Y -> 2)

    Like any expression, this can be packaged in a function:

    fun du[Left, Right : set univ] : (Left + Right) -> Int {
  (Left -> 1) + (Right -> 2)
}

    And then the disjoint union of A and B can be written du[A, B].

    I repeat my advice to spend some time learning about comprehensions.