Accumulation of union of sets

Question

I have two classes A and B and a relation with extra data of class R on them.

So, A and B are related to each other via R.

sig A {}
sig B {}

sig R {
    a : A,
    b : B,
    data : Bool
}

here, Bool is defined as:

sig Bool {}
sig True, False extends Bool {}

Now, I extend A like this:

sig A{
    allb : some B
}

Which contains all instances of B for which there is a relation between this A and that B and where the data is of type True.

I want to express the following logical statement as an Alloy fact:

Formal version of text above http://dropproxy.com/f/3B

I assume here that True == 1 and False != 1 and that the sets A and R contain all instances of A and R respectively.

What I've tried so far is to define a fun trueR(a : A) which should return all R's for which R.a = a and r.data = True and a fact allbIsRTrue which states that for each A allb should be the sum of the R.b's returned by trueR.

However, here is where I get stuck, I can't find the right construct to sum over sets in the reference and tries with sum have resulted in syntax errors.

How would I specify my formal constraint as an Alloy fact?

Answer 1

I think you want to use set comprehension. In Alloy, this is the syntax for set comprehension

{x: X | f(x)}

The expression above evaluates to a set of X's for which f(x) holds.

In your example, to express the fact for allB you can write something like

fact fAllB {
    all a: A | 
        a.allB = {b: B | 
            some r: R | r.ra = a and r.rb = b and r.data = True}
}

In English, this fact reads "for all a of set A, a.allB is a set of all B's such that there exist some r which "connects" those exact a and b and for which r.data is True.

Note the following modifications I made to the rest of your model:

• I made the Bool sig abstract because you probably don't want bools that are neither True nor False

• I made the True and False sigs singleton sigs (i.e., one sig) because you probably want to have exactly one atom of each of them

• I renamed relations a and b to ra and rb to avoid name aliasing and potential confusion

Here is the rest of your model that I used for this example

abstract sig Bool {}
one sig True, False extends Bool {}

sig A {
  allB: set B
} 
sig B {}
sig R {
  ra : A,
  rb : B,
  data : Bool
}