Impact of semantics changes of Alloy 4.2 on exercise A.1.6 of the Alloy book?

Question

According to the release notes for Alloy 4.2, there are semantics changes related to integers. These changes seem to have an impact on exercise A.1.6 of the Alloy book.

In this exercise, the following code is given as a basis (I added the "Int" at the very end to show my problem). When running the "show" predicate, the visualizer displays an instance, but this instance contains, in addition to integers, two more atoms "Univ0" and "Univ1".

module exercises/spanning

pred isTree(r: univ->univ) {}
pred spans(r1, r2: univ->univ) {}

pred show(r, t1, t2: univ->univ) {
    spans[t1,r] and isTree[t1]
    spans[t2,r] and isTree[t2]
    t1 != t2
}
run show for 3 Int

What is the meaning of these two atoms "Univ0" and "Univ1"? Why are they there? They do not appear with the same code executed on Alloy 4.1.10.

Answer 1

When there are no user-defined sigs, Alloy automatically synthesizes a new sig called "Univ". This is a convenient feature since it lets you write formulas over the whole universe without having to introduce any sigs.

When you explicitly give a scope for Int, then the universe will certainly contain all Int atoms within the given scope. If additionally there are no user-defined sigs, you'll end up having the synthesized Univ sig as well. It is debatable whether it makes sense to synthesize the Univ sig when a scope for Int is explicitly used.

To work around your problem, you have several options:

1. If you don't care what is the type of your graph nodes (i.e., you don't explicitly want the nodes to be Ints), then you can simply change the run command to say

   run show for 3 instead of run show for 3 Int.

   If you do that, you'll have no Int atoms, and only Univ atoms. If you don't like the Univ sig, simply introduce a new sig, e.g., sig Node {} in which case all atoms will be of type Node.

2. If you really want your graph to be over Ints only, you can change univ->univ to Int->Int in all your predicates.

3. If you really want your universe to contain only Int atoms (in which case you can keep univ->univ in your predicates), you can introduce a dummy signature and add a fact that ensures that its cardinality is zero.

   sig Dummy {}
   fact { no Dummy }
   

   This small change will ensure that the Univ sig is not automatically synthesized and will not affect the rest of you model.

Hope this helps.