时间戳

首页 > 解决方案 > 链接数据结构：限制链接操作

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

问题描述

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

我想要做的（但尚未实现）是定义一个谓词，该谓词Link对两个节点的链接进行建模，使得一个节点成为另一个节点的后继者（succ）。此外，我想限制操作，以便只能对Isolated节点进行链接。此外，我希望限制（如果可能的话）以某种方式在predicate内部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节点可以链接到？

标签： alloy

解决方案

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

open util/ordering[time]

sig Time {}
sig Data {}

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

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

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

推荐阅读