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

Question

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

我想要做的——但还没有实现——定义一个谓词Link，它模拟两个节点的链接，使得一个节点成为另一个节点的后继者（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 节点可以链接到？

Answer 1

问题是您希望 Link 是一个 操作，它会更改 succ 的值。为了对 Alloy 中的更改进行建模，您需要添加一个有序签名，该签名代表系统的不同状态。所以你的签名看起来像这样：

open util/ordering[time]

sig Time {}
sig Data {}

sig Node {
    data: Data,
    succ: Node lone -> Time
}

但这也会改变你所有的谓词。不能说某个节点是孤立的或终结的，只能说是在T时某个节点是孤立的。

如果您有软件抽象，这将在第 6.1 节中介绍。除了那本书之外，我不熟悉任何关于 Alloy 建模时间的好的指南。