overloading - 在合金中隐藏子类型的字段

Question

假设我在 Alloy 4.2 中有以下签名声明:

sig Target {}

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

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

运行时，生成的实例会有从每个 B 到某个 Target 以及从 C 到某个 Target< 的箭头.

我怎样才能只隐藏 B 的箭头？
起初我尝试了以下方法:

abstract sig A {
    parent: lone A
}

sig B extends A {
    r: some Target
}

sig C extends A {
    r: some Target
}

这将使我能够控制 B 中的 r，但在编写属性时会引入很多歧义。我想让这些尽可能简单。例如:

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

上面说a的Targets是a的子Targets的集合。< br/>对于后面的声明，我将不得不将其重写为

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

这是不受欢迎的。

是否有任何解决方法可以让通用字段，但仍然可以控制显示的箭头？

Answer 1

你可以定义一个完全对应于(C <: r)的函数:

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

在 Alloy 可视化器中，您可以访问关系 $C_r。然后，您可以关闭关系 r 的“显示为弧”，但 $C_r 仍然可见。这应该隐藏属于 (B <: r) 的边集。