Question

Suppose I have the following signature declarations, in Alloy 4.2:

sig Target {}

abstract sig A {
    parent: lone A,
    r: some Target
}

sig B extends A {}
sig C extends A {}

When running, the resulting instances would have arrows from every B to some Target, and from C to some Target.

How would I be able to hide only the arrows from B?
I tried the following, at first:

abstract sig A {
    parent: lone A
}

sig B extends A {
    r: some Target
}

sig C extends A {
    r: some Target
}

This would give me control over r in B, but it introduces a lot of ambiguity when writing properties. I would like to keep these as simple as possible. For example:

all a: A | a.r = parent.a.r

The above says that a's Targets is the set of a's children's Targets.
With the latter declarations, I would have to rewrite this to

all b: B | b.r = parent.b.((B <: r) + (C <: r))
all c: C | c.r = parent.c.((B <: r) + (C <: r))

which is undesirable.

Is there any workaround to be able to have a general field, but still have control over what arrows are displayed?

Was it helpful?

Solution

You can define a function that exactly corresponds to (C <: r):

fun C_r : A -> Target {
    (C <: r)
}

In the Alloy visualizer, you wil have access to relation $C_r. Then, you can turn off "Show as arcs" for relation r, but still have $C_r visible. This should hide the set of edges that belong to (B <: r).

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top