Mathematics for Computer Science

Chapter 13 State Machines388

outgoing-msgs, a finite sequence ofM, whose initial value is calledall-msgs

tagbit2f0;1g, initially 1

received-msgs, a finite sequence ofM, initially empty

ackbit.2f0;1g, initially 0

msg-channel, a finite sequence ofMf0;1g, initially empty,

ack-channel, a finite sequence off0;1g, initially empty

The transitions are:

SEND: (a)action:send-msg.m;b/

precondition:mDrightend.outgoing-msgs/ANDbDtagbit

effect: add.m;b/to the lefthand end ofmsg-channel, any number 0

of times

(b)action:send-ack.b/

precondition:bDackbit

effect: addbto the righthand end ofack-channel, any number 0 of

times

RECEIVE: (a)action:receive-msg.m;b/
precondition:.m;b/Drightend.msg-channel/
effect: removerightendofmsg-channel;
ifb¤ackbit, then [addmto the lefthand end ofreceive-msgs;ackbitWD
b.]
(b)action:receive-ack.b/
precondition:bDleftend.ack-channel./
effect: removeleftendofack-channel.
ifbDtagbit, then [removerightendofoutgoing-msgs(if nonempty);
tagbitWDtagbit]

Our goal is to show that whentagbit¤ackbit, then

outgoing-queue
received-msgsDall-msgs: (13.1)

This requires three auxiliary invariants. For the first of these, we need a defini-

tion.

Lettag-sequencebe the sequence consisting of bits inack-channel, in right-to-

left order, followed bytagbit, followed by the tag components of the elements of

msg-channel, in left-to-right order, followed byackbit.

Property 2: tag-sequenceconsists of one of the following: