当变量值对(即映射)之一被取消时，不会保留变量值对

Question

我有以下简单模型，我尝试模拟数据集中所选数据的无效。数据到Val(d2v(映射是一个名为动态的签名字段，其实例对应于模型的不同状态(之前和之后(。当我尝试模拟这个模型时，我得到了两个不相关的动态实例，即使我显式地将两个动态实例的 d2v 映射设置为相同(当然，传递数据实例的映射以取消谓词除外(。换句话说，两个动态实例的变量-值配对不匹配。我错过了什么？

sig Data {}
sig Val {}
sig Dynamic {
d2v: Data -> lone Val,
}
pred nullify [dyn, dyn': Dynamic, d:Data] {
d in dyn.d2v.univ implies
dyn'.d2v = dyn.d2v - (d -> d.(dyn.d2v))
else
dyn'.d2v = dyn.d2v
}
run nullify for exactly 3 Data,
exactly 3 Val,
exactly 2 Dynamic

以下是来自Alloy的两个Dynamic.d2v实例的示例评估：

sig Dynamic
Dynamic$0
field d2v
Data$2 -> Val$2
Dynamic$1
field d2v
Data$0 -> Val$1
Data$1 -> Val$0

其中 Data$2 是删除谓词的参数。例如，我所期望的是以下内容：

sig Dynamic
Dynamic$0
field d2v
Data$2 -> Val$2
Data$0 -> Val$1
Data$1 -> Val$0
Dynamic$1
field d2v
Data$0 -> Val$1
Data$1 -> Val$0

Answer 1

您确定实例将 dyn 和 dyn 绑定到 Dynamic$0 和 Dynamic$1 吗？例如，它可以将它们绑定到 Dynamic$1，满足谓词的 else 臂。