合金三元关系覆盖

Question

我在 sig Record 中有一个三元关系，如果前两个元素匹配，我有一个谓词 changeRecord 来修改第三个元素。但是 ++ 覆盖只检查域（第一个元素），我该怎么做？

sig Account{}
sig Record{
    allowance: Account -> Account -> one Int
}
pred changeRecord(a1, a2: Account, r1, r2: Record, val: Int){
    val > 0
    a1 != a2
    r2.allowance = r1.allowance ++ (a1 -> a2 -> val) // ***
}

*** 行当前用 a1 -> a2 -> val 替换任何以 a1 开头的元组，但我希望这种替换只发生在像 a1 -> a2 -> someothervalue 这样的行上。

Answer 1

这是第一个版本，它仅覆盖匹配 a1->a2 和 a1->a2->val' 的元组。 它涉及几个步骤，我相信更有经验的 Alloy 用户可以更简洁地完成相同的任务，或许可以采用不同的思路。

pred changeRecord[a1, a2: Account, r1, r2: Record, val': Int] {
    val' > 0
    a1 != a2

// step 1.
    let val_for_a1_a2_in_r1 = a2.(a1.(r1.allowance)) |
// step 2.
    let a1_a2_val_in_r1 = a1->a2->val_for_a1_a2_in_r1 |
// step 3.
    let r1_allowance_without_a1_a2_val = r1.allowance - a1_a2_val_in_r1 |
// step 4.
    let a1_a2_val' = a1_a2_val_in_r1 ++ a1->a2->val' |
// step 5.
    r2.allowance = r1_allowance_without_a1_a2_val + a1_a2_val'
}

想法是在步骤 1. 和 2. 中分离 r1.allowance 中匹配 a1->a2 的那些元组，在步骤 3. 中从 r1.allowance 中减去它们，用 a1->a2->val' 覆盖它们在步骤 4 中。最后在步骤 5 中将覆盖集加上 r1_allowance_without_a1_a2_val '分配'给 r2.allowance。请注意，对于某个 a1->a2 对，在 r1.allowance 中可能有几个具有不同 val 的元组，这些都将是被 a1->a2->val' 覆盖，然后当然只有一个 a1->a2->val' 会出现在 r2.allowance 中。 备注：这个方案的正确性我没有仔细检查过。