Programmable Messaging for Electronic Government - Building a Foundation - Formal Methods and Hybrid Real-Time Systems - page 230

8. receive - The function takes the identifier of the recipient as an argument
and returns the message. It extracts the first message from the outbox of the
recipient, applying val2mes and make to convert the value into a message and
then into a structure. Subsequently, it removes the message from the outbox.
The precondition states that the recipient exists and its outbox variable is
non-empty.

receive: Id × State → StateX × StructX
receive(mid, s) as (s ,m) post
let mp = get(get(outb(mid)), mesCat, make(n(1)))
in m = make(val2mes(val(eval(mp, s)))) ∧
s = change(outb(mid), del(mesCat, get(mp), get(outb(mid)))) end
pre eval(canReceive(mid), s),
canReceive: Id → BoolX

canReceive(id) ≡
let
x1 = hasPart(make(idCat, id2val(id)), get(reg)),
x2 = hasParts(mesCat, get(outb(id)))
in and(x1, x2) end

9. deliver - The function takes two arguments - the identifier of the sender
and the message to be delivered. It removes the message from the inbox of
the sender, and it adds the message to the outbox of the recipients. Func-
tion recipients provides a list of member identifiers who must receive the
message on a given state. Recipients are calculated from the idCat parts of
the variable representing the channel. In the current version of the model,
we assume the list of recipients comprises only two members id1 and id2 .
For adding the message into the outbox variables of the recipients, first the
message is converted into a value throught the mes2value function, then
this value is inserted as a new mesCat -category part. Function deliver is a
total function modeling internal behaviour of the messaging infrastructure.

value
deliver: Id × Mes × StateX → StateX
deliver(id, m, s) ≡
let

id1, id2 = recipients(m, s),
x = make(mesCat, mes2val(m)),
x1 = change(inb(id), del(mesCat, mes2val(m), get(inb(id)))),
x2 = change(outb(id1), add(x, get(outb(id1)))),
x3 = change(outb(id2), add(x, get(outb(id2))))
in con(x1, con(x2, x3))
end

In a future version of the model we plan to include a recursive function on
StateX providing an iterative behaviour. In particular, for delivering mes-
sages it will iterate over the list of recipients.