链接数据结构：限制链接操作

Question

我有一个带有两个签名的模型（见下文）：Data和Node。我定义了一些谓词来表征Node的居民，即：Orphan，Terminal和Isolated。

我想做但尚未实现的是定义一个谓词Link，该谓词对两个Node的链接进行建模，以使一个Node成为另一个Node的后继者（succ）。此外，我想限制操作，使链接只能建立到Isolated节点。此外，我希望限制-如果可能的话-以某种方式成为[[Link谓词的内部]]。 这是我最近的尝试：

sig Data {}

sig Node {
    data: Data,
    succ: lone Node
}

// Node characterisation
pred Isolated (n: Node) { Orphan[n] and Terminal[n] }

pred Orphan (n: Node) { no m: Node | m.succ = n }

pred Terminal (n: Node) { no n.succ }


/*
 * Link
 * 
 * May only Link n to an m, when:
 *  - n differs from m
 *  - m is an Isolated Node (DOES NOT WORK)
 *
 * After the operation: 
 *  - m is the succcessor of n
 */
pred Link (n,m: Node) {
    n != m
    Isolated[m] /* Not satisfiable */
    m = succ[n]
}

pred LinkFeasible { some n,m: Node | Link[n,m] }

run LinkFeasible

包括连词Isolated[m]使模型不令人满意。我想我明白为什么：不可能有Node既是Isolated又是另一个继承人。我仅将其包括在内是希望它可以揭示我的意图。

我的问题：如何定义Link谓词来链接两个节点，以便仅可以将Isolated节点链接到？

我有一个带有两个签名的模型（见下文）：数据和节点。我定义了一些表征Node居民的谓词，即：孤儿，终端和孤立。我想做什么-...

Answer 1

operation。为了模拟Alloy中的变化，您需要添加代表系统不同状态的有序签名。因此，您的签名将如下所示：