我正在使用 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}
. 但有时可能需要同时保留它,有没有办法同时拥有它?
提前致谢。