在 Alloy 中构建关系

Question

在哲学家用餐问题中，我们有一个 table 哲学家和叉子。

sig P {}
sig F {}

对于这个问题，我想要以下代表 table 的关系：

P1 -> F1
F1 -> P2
P2 -> F2
F2 -> P3
P3 -> F3
F3 -> P1

即每个 P 将指向一个 F，每个 F 将指向一个 P，这将形成一个圆圈。我想调用一个函数来获得这个关系：

fun table : (P+F) one -> one (P+F) { ... }

我一直在努力使这项工作成功，但感觉我缺少一些基本的东西，而这些东西也与我遇到的其他问题有关。不知怎么的，我错过了 'constructor'.

有什么指点吗？

额外

@Hovercouch 提供了一个有助手 sig 的可行解决方案。但是，这需要对 P 和 F 进行非自然扩展并引入新的 sig。这也可以通过以下方式解决：

sig P, F {}
one sig Table {
    setting : (P+F) one -> one (P+F)
} {
    # P = # F
    all p : P, f : F | P in p.^setting and F in f.^setting
}
run {} for 6

这解决了非自然继承问题。

但是，对于一个非常简单的问题，它似乎仍然非常全球化并且需要做大量工作。仍然保持开放状态，看看是否有其他解决方案。

Answer 1

如果您愿意添加辅助对象，我们可以通过制作一个 abstract sig Thing 然后制作 Thing:

的 P 和 F 实例来实现

abstract sig Thing {
    next: Thing
} {
    Thing = this.^@next
}

sig F extends Thing {} {
    next in P
}

sig P extends Thing {} {
    next in F
}

fact SameNumberOfThings {
    #P = #F
}

run {} for 6

Answer 2

这里可能涉及表达能力和易处理性之间的设计权衡。

肯定存在什么才算干净或直观的问题；你说 P 和 F 的 'next'-ness 是 "an aspect of the table setting" 而不是 "an aspect of P or F"。我想我理解你的想法，但我认为你不可能再成功地定义一种原则性方法来区分 P 和 F 的 "aspects" 以及它们出现在其域或范围内的关系在过去的几千年里，任何一位试图可靠地区分本质和偶然性的哲学家。

如果我们承认这种区别是不可靠的，但我们仍然发现它有用，那么问题就变成了 "who made the rule that a relation defined as part of a signature must relate to an (intrinsic) aspect of the individuals involved, and not to an extrinsic relation which is not an aspect of the individuals?" 答案是：你做到了，而不是 [的创造者] Alloy。如果一个人过分坚持自己对想要用来表达某物的结构的直觉，那么就会存在一定的风险，即坚持不仅该事物应该是可表达的，而且我们应该能够使用特定的结构来表达它。这种坚持可以教会我们很多关于符号的知识，但有时更容易接受符号的设计者也有直觉。

Daniel Jackson 的 Software Abstractions 中的问题Does Alloy allow freestanding declarations?（在在关于高阶量化的 3.5.3 节之后的讨论）和 必须将所有关系声明为字段吗？（在关于基本字段声明的 4.2.2 节之后的讨论中）。讨论的要点是 "If you want to declare some relations that don't belong naturally to any existing signatures, you can simply declare them as fields of a singleton signature." 已作必要的修改，给出的示例看起来很像您附录中的 Table 信号。

TL;DR 是的，您可能会觉得它有点麻烦，但是包含您不想在其第一个成员上定义的关系的单例签名确实与既定的习语一样接近，因为诸如此类。

在 Alloy 中构建关系

Constructing a relation in Alloy

alloy