Download Formal Refinement Support

D33.4 - Refinement Support (Public)
[((i = 1 and has1) or (i = 2 and has2)) and
((i = 1 and m1 > card1) or
(i = 2 and m2 > card2))] &
reject!i -> RemReq(i)
EffTran
= i: Index @
[((i = 1 and has1) or (i = 2 and has2)) and
((i = 1 and m1 <= card1) or
(i = 2 and m2 <= card2))] &
([i = 1] & transfer.(1).tgt1.m1 -> MkTran(1)
[]
[i = 2] & transfer.(2).tgt2.m2 -> MkTran(2))
@ mu X @ (
([] i : Index @
RecTranReq(i) [] RejTran(i) [] EffTran(i)
); X
)
end
Next, by applying the copy-rule to the operation calls and further simplifying the
model, we obtain the following actions.
...
actions
RecTranReq = i: Index @
[i = 1 => not has1 and i = 2 => not has2] &
pay.i?j:(i <> j)?n:(n > 0) -> (
cases i:
1 -> has1 := true; src1 := i; tgt1 := j; m1 := n,
2 -> has2 := true; src2 := i; tgt2 := j; m2 := n
end
)
RejTran
= i: Index @
[((i = 1 and has1) or (i = 2 and has2)) and
((i = 1 and m1 > card1) or
(i = 2 and m2 > card2))] &
reject!i -> (
cases i:
1 -> has1 := false,
2 -> has2 := false
end
)
33