在Alloy中隐藏一个子类型的字段-Java 学习之路

假设我在合金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 's children' s Targets 的集合 .
对于后面的声明，我将不得不重写它

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

这是不可取的 .

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

1 Answer