Home Articles

在Alloy中隐藏一个子类型的字段

Asked
Viewed 985 times
3

假设我在合金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

上面说的是 aTargetsa '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

  • 5

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

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

    在Alloy可视化工具中,您将可以访问关系$ C_r . 然后,您可以关闭关系r的“显示为弧”,但仍然可以看到$ C_r . 这应该隐藏属于(B <:r)的边集 .

Related