CODEWITHSUNDEEP
alloy
Sophia
Sophia

Reputation: 11

Alloy ternary relation override

I have a ternary relation in a sig Record, and I have a predicate changeRecord to modify the third element if the first two element are matched. But the ++ override only check the domain (the first element), how can I do that? 

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) // ***
}

The *** line currently replaces any tuples starting with a1, with a1 -> a2 -> val, but I want that replacement only happen on lines like a1 -> a2 -> someothervalue.

Upvotes: 1

Views: 291

Answers (1)

Attila Karoly
Attila Karoly

Reputation: 1021

Here's a first version that overrides only the tuples that match a1->a2 with a1->a2->val'. It involves several steps and I'm sure more experienced Alloy users can accomplish the same task more succinctly, perhaps along a different line of thinking.

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'
}

The idea is to separate those tuples in r1.allowance that match a1->a2 in steps 1. and 2., subtract them from r1.allowance in step 3., override them by a1->a2->val' in step 4. and finally 'assign' the overridden set plus r1_allowance_without_a1_a2_val to r2.allowance in step 5. Please note that for a certain a1->a2 pair there may be several tuples with different vals in r1.allowance and these all will be overridden by a1->a2->val' and then, of course, only one a1->a2->val' will appear in r2.allowance. Remark: I haven't checked the correctness of this solution extensively.

Upvotes: 1

Related Questions