三元算子中合金的自反传递闭包答案

【问题标题】：Reflexive Transitive Closure in Alloy in Ternary Operator三元算子中合金的自反传递闭包
【发布时间】：2015-05-11 01:01:16
【问题描述】：

我有一个合金模型

sig BinaryTree{
    root : Node,
    nodes: set Node,
    left, right : Node -> Node
}

现在，我在它上面定义了一个谓词，它是有效的语法

pred Connected[t: BinaryTree, l:Node -> Node, r: Node -> Node]
{
    all n: t.nodes | n in t.root.*(l+r)
}

但是，我不明白为什么它是有效的，因为 * 的行为，自反传递闭包表示对于

foo.*bar

您可以通过反复将 bar 应用于 foo 来获得所有可能获得的集合。因此，foo、foo.bar、foo.bar.bar 等。

但是，您得到的始终是“bar”的结果，而不是不同的结果。应用闭包的结果，必须始终是“类型”栏。

在我上面给出的代码示例中，结果应该始终是 (l+r)，这意味着一个集合包含类型 (node->node)。

但我应用于 n 的“in”关键字实际上应该应用于一组 (node)，而不是 (node->node)。为什么这行得通？为什么它隐式地将 (node->node) 转换为一组 (nodes)，使得 n: node 正在针对该集合进行评估以包含在其中？

【问题讨论】：

【解决方案1】：

您的误解来自您赋予字段的类型。

在您的示例中，字段 root 不是 Node 类型，而是 BinaryTree -> Node 类型，因为它将 BinaryTree 与 Node 相关联。

就像你的字段root，关系Node -> Node也是arity 2。

如果您只是对类型进行推理，则以下内容可以代表您的谓词：

Node in BinaryTree . BinaryTree -> Node . *(Node -> Node + Node -> Node )

什么时候开发的：

Node in BinaryTree . BinaryTree -> Node . *(Node -> Node)

* 操作符只是简单地“反转”一个关系，这样A->B 元组就变成了B->A 元组。然后你有：

Node in BinaryTree . BinaryTree -> Node . (Node -> Node)

现在来说明如何“。”使用（点连接）运算符，考虑示例： A1 。 A2->B A1、A2 和 B 分别是签名 A 和 B 的原子集，此表达式返回 A2->B 中存在的 B 原子集，使得 A2 在 A1 中。

点运算符左侧的类型因此被删除为以下关系的类型。

因此我们终于：

Node in Node .(Node->Node) 

Node in Node

我希望你明白为什么它现在可以工作了:)

【讨论】：