Alloy's formula translation

Question

I have a little alloy specification as follows:

sig class {parents : set class}
fact f1{all p:class | not p in p.^parents}
run{} for exactly 4 class

First, I thought alloy would translate f1 into boolean matrix, then perform closure operation on it. But it seems it does not do this kind of translation (it looks like it runs something before boolean matrix creation.). So how exactly this f1 gets translated? Does it use relation predicate? I am just very curious about alloy's translation.

Answer 1

Boolean matrices are used to represent expression in Alloy. So, you start with a unary matrix for each sig, a binary matrix for each binary relation, a ternary matrix for each ternary relation, and so on. Then, translation of "complex" expression (e.g., involving relational algebra operators) is done by manipulating (composing) those matrices you started with. For each Alloy operator (e.g., transitive closure (^), relational join (.), in, not, etc.) there is a corresponding algorithm that performs a bunch of matrix operations such that the semantics of that operator is correctly implemented.

So in this example, the all quantifier is first unrolled, meaning that for each atom p of type class the body is translated (something like:

• m0 = matrix(p) //returns matrix corresponding to p
• m1 = matrix(parents) //returns matrix corresponding to parents
• m2 = ^m1
• m3 = m0.m2
• m4 = m0 in m3
• m5 = not m4

), and finally, all those body translations are AND'ed.