0

我正在使用 Alloy 对图形转换进行建模。我将我的转换指定为应用于图表不同部分的不同转换。所以我有一个签名：

sig Transformation {
    nodes : some Node,
    added_node : one Special_Node
}

为了应用这种转换，我在签名的事实部分声明了 3 个关系，它们适用于图形的不同部分。关系的左侧与输入图相关，右侧与输出图相关：

some mapping_rel0_nodes : rel0In one -> one rel0Out|{
    C1 && C2 && C3 
}
&&
some mapping_rel1_nodes : rel1In   ->  some (rel1Out+special_Node) | {
    C1' && C2' && C3'
}
&&
some mapping_rel2_nodes : rel2In   ->  some (rel2Out+special_Node) |{
    C1'' && C2'' && C3''
} && 
 out.nodes <: connections = ~mapping_rel2_nodes.inpCnx.mapping_rel2_nodes +
                            ~mapping_rel1_nodes.inpCnx.mapping_rel1_nodes +
                            ~mapping_rel0_nodes.inpCnx.mapping_rel0_nodes

每个关系都适用于图形的不相交的不同部分，但它们通过它们之间的连接来连接。CX、CX' 和 CX'' 是应用于关系的约束。节点具有以下签名：

sig Node{
    connections : set Node
}{
    this !in this.@connections
}

为了获得新连接，我获取输入图中的所有连接 inpCnx 并使用为每个点获得的映射来获得新图中的关联连接。

我的问题是：

  • mapping_relX_nodes 在他的事实步骤中仍然是已知的吗？
  • 当我在评估器中控制它们并在适当的实例上手动执行操作时，它可以工作，但表示为事实，它不返回任何实例。我读了这篇文章，我想知道是否有其他工具来控制表达式和变量，比如调试打印或其他？
  • 这些关系具有相同的元数，但 rel0 是双射的，其他只是二元关系。由于 rel0 的双射性，这些关系的并集必须是双射的吗？
  • 根据我在评估器中的经验，当一个元组重复时，其中一个会被删除：{A$0->b$0, A$0->B$0}变成{A$0->B$0}. 但有时可能需要同时保留它，有没有办法同时拥有它？

提前致谢。

4

1 回答 1

0

你问：

mapping_relX_nodes在他的事实步骤中仍然是已知的吗？

如果没有一个完整的工作模型来测试，很难给出一个绝对确定的答案。但是 Alloy 纯粹是声明性的，并且mapping_rel1_nodesetc. 的使用似乎不是局部变量，因此您的事实的第四个连词中的引用将与其他连词中的引用以相同的方式绑定。（或者不绑定，如果他们没有绑定的话。）

当我在评估器中控制它们并在适当的实例上手动执行操作时，它可以工作，但表示为事实，它不返回任何实例。我读了这篇文章，我想知道是否有其他工具来控制表达式和变量，比如调试打印或其他？

从来没听说过。根据我的经验，当某些东西似乎在评估器中按预期工作但我无法让它在事实或谓词中工作时，我几乎总是未能正确地获得事实或谓词的语义。

这些关系具有相同的元数，但 rel0 是双射的，其他只是二元关系。由于 rel0 的双射性，这些关系的并集必须是双射的吗？

不（除非我完全误解了你的问题）。

根据我在评估器中的经验，当一个元组重复时，其中一个被删除：{A$0->b$0, A$0->B$0} 变为 {A$0->B$0}。但有时可能需要同时保留它，有没有办法同时拥有它？

是的; 合金适用于套装。（所以重复项没有被“删除”——只是集合没有重复项。）为了区分两个原本相同的元组，您可以（a）向元组添加另一个值（所以对变成三元组，三元组变成 4 元组，n 元组变成元组 n+1)，或者 (b) 为表示元组的对象定义签名。由于签名的成员具有对象标识，而不是值标识，因此它们可用于区分不同出现的对，例如 A$0->B$0。

于 2013-10-27T01:29:12.837 回答