我正在使用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,并使用为每个点获得的映射来获取新图中的关联连接。
我的问题是:
{A$0->b$0, A$0->B$0}
变为{A$0->B$0}
。但是有时可能需要同时保留两者,有没有办法同时保留两者?提前致谢。
你问:
不要mapping_relX_nodes在他的事实步骤仍是我们知道的?
没有完整的工作模型进行测试,很难给出绝对坚定的答案。但是Alloy是纯声明性的,而mapping_rel1_nodes
etc等的使用似乎不是局部变量,因此,事实第四个合相中的引用将与其他合相中的引用绑定在一起。(如果未绑定,则不绑定。)
当我在评估器中控制它们并在适当的实例上手动执行操作时,它可以工作,但表示为事实,它不返回任何实例。我读了这篇文章,我想知道是否还有其他工具来控制表达式和变量,例如debug print还是其他?
从来没听说过。以我的经验,当某些东西在评估器中似乎可以按预期工作,但我无法使它在事实或谓词中起作用时,我几乎总是无法获得事实或谓词的语义。
这些关系具有相同的对数关系,但是rel0是双射的,其他的只是二元关系。由于rel0的双射性,这些关系的并集必须是双射的吗?
不可以(除非我完全误解了您的问题)。
根据我在评估器中的经验,当有一个元组重复时,其中一个将被删除:{A $ 0-> b $ 0,A $ 0-> B $ 0}变为{A $ 0-> B $ 0}。但是有时可能需要同时保留两者,有没有办法同时保留两者?
是的; 合金搭配套装。(因此,重复项不会被“删除”-只是集合中没有重复项。)要区分两个原本相同的元组,您可以(a)向该元组添加另一个值(这样,对变成三元组,三元组变成4元组,而n元组成为Ar + 1(n + 1)的元组,或(b)为表示元组的对象定义签名。由于签名的成员具有对象身份,而不是值身份,因此它们可用于区分不同的配对出现,例如A $ 0-> B $ 0。
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句