Remove predicate relations in Alloy

Question

I'm learning how to use Alloy, and I've coded this:

module test/SlotsAndFillers

sig Slot { content: one Filler}
sig Filler { slots: set Slot}

fact AllSlotsAreOwned {
    all s:Slot | some x:Filler | s in x.slots
}

fact ImproperParthoodSlots {
    all x:Filler | some y, z:Slot |  y in x.slots implies z in x.slots and x in z.content
}

fact SlotInheritance {
    all x, y : Filler, z, z' : Slot | x != y and z != z' and z in y.slots and x in z.content and z' in x.slots implies z' in y.slots
}

fact SingleOccupancy {
    all x:Slot, y:Filler  | x in y.slots implies one z:Filler | z in x.content
}

fact MutualOccupancyIsIdentity {
    all x, y: Filler, z, z': Slot | x != y and z != z' and
    z in y.slots and x in z.content and z' in x.slots and y in z'.content implies x = y
}

pred show() {}

run show

When I execute and show models, in addition to both relations content and slots, the models also have new relations, named $show_x, $show_y and $show_z. By testing, I understood that these relations are present if I add things inside the predicate. But for this code, show is empty and there are still these relations. So I've two questions: where do they come from and how to remove them? I know that I can hide them, but then the models look all (nearly) the same. So I would like to explore different models that uses only my two relations and not new ones.

Do not hesitate to reformulate or retitle this post.

Thanks!

Answer 1

When you are executing a run command followed by a predicate, you are actually generating instances satisfying that predicate. From my understanding, when the predicate is named, the instance visualizer tries to highlight which elements of the instance satisfy the predicate. In your case, "everything" is conforming to this empty predicate and so the name of your predicate is shown everywhere.

A simple workaround is to simply not name the predicate that you give as parameter to the run command:

module test/SlotsAndFillers

sig Slot { content: one Filler}
sig Filler { slots: set Slot}

fact AllSlotsAreOwned {
    all s:Slot | some x:Filler | s in x.slots
}

fact ImproperParthoodSlots {
    all x:Filler | some y, z:Slot |  y in x.slots implies z in x.slots and x in z.content
}

fact SlotInheritance {
    all x, y : Filler, z, z' : Slot | x != y and z != z' and z in y.slots and x in z.content and z' in x.slots implies z' in y.slots
}

fact SingleOccupancy {
    all x:Slot, y:Filler  | x in y.slots implies one z:Filler | z in x.content
}

fact MutualOccupancyIsIdentity {
    all x, y: Filler, z, z': Slot | x != y and z != z' and
    z in y.slots and x in z.content and z' in x.slots and y in z'.content implies x = y
}

run {}

EDIT:

It seems that this fix doesn't solve the problem. Indeed quantification variables defined in facts are still displayed by the instance viewer. The only option left (I can think of) to get rid of them is to manually disable their representation in the Theme Menu.

(for the 3 relations $x,$y, $z, set "show as arcs" to off)