The Alternating Bit Protocol
The Alternating Bit Protocol is a simple communication protocol
that is often used as a test case,
either for some algebraic formalism or for some tool
for the analysis or verification of concurrent systems.
Although it is simple, it contains many interesting ingredients
from concurrency theory.
Description
We can represent the Alternating Bit Protocol with the following picture.
It consists of a
Sender, a
Receiver, and channels
K
and
L.
Sender
First,
Sender reads a message at his input port.
This message is extended with a control bit to form a frame and this
frame is sent along channel
K.
The sending of the frame proceeds until
Sender receives an
acknowledgement of a succesful transmission over channel
L.
After a succesful transmission
Sender flips the control bit
and starts all over again.
channel K
Channel
K transmits frames from
Sender to
Receiver.
There are two situations that can occur.
The frame is properly transmitted, or the frame is corrupted during
transmission.
Receiver
Receiver reads a frame from channel
K.
It is assumed that
Receiver is able to tell, e.g. by performing
a checksum control, whether or not the frame has been corrupted.
When the frame is correct,
Receiver checks the control bit
in the frame.
If this bit matches the internal control bit of
Receiver,
the message in the frame is sent to the output port,
Receiver
sends an acknowledgement with the control bit to
Sender over
channel
L.
Receiver then flips his internal control bit and waits for
another frame.
In all other cases,
Receiver sends a negative acknowledgement
(with a flipped control bit), and waits for a retransmission of the
frame.
channel L
Channel
L is used to transmit acknowledgements from
Receiver
to
Sender.
Like channel
K, it is able to corrupt data.
It is assumed that
Sender can tell whether an acknowledgement has
been corrupted.
Specification
data module Bits
begin
exports
begin
sorts
BIT
functions
0 : -> BIT
1 : -> BIT
flip : BIT -> BIT
end
equations
[B1] flip(0) = 1
[B2] flip(1) = 0
end Bits
data module Data
begin
exports
begin
sorts
DATA
functions
'a : -> DATA
'b : -> DATA
'c : -> DATA
'd : -> DATA
'e : -> DATA
end
end Data
data module Frames
begin
exports
begin
sorts
FRAME
functions
frame : BIT # DATA -> FRAME
frame-error : -> FRAME
end
imports
Data, Bits
end Frames
data module Acknowledgements
begin
exports
begin
sorts
ACK
functions
ack : BIT -> ACK
ack-error : -> ACK
end
imports
Bits
end Acknowledgements
process module ABP
begin
imports
Bits, Data, Frames, Acknowledgements
atoms
input : DATA
send-frame : FRAME
receive-ack-or-error : ACK
receive-frame : FRAME
send-frame-or-error : FRAME
receive-frame-or-error : FRAME
output : DATA
send-ack : ACK
receive-ack : ACK
send-ack-or-error : ACK
frame-comm : FRAME
frame-or-error : FRAME
ack-comm : ACK
ack-or-error : ACK
processes
Sender
Receive-Message : BIT
Send-Frame : BIT # DATA
Receive-Ack : BIT # DATA
K
K : BIT # DATA
Receiver
Receive-Frame : BIT
Send-Ack : BIT
Send-Message : BIT # DATA
L
L : BIT
ABP
sets
of atoms
H = { send-frame(f), receive-frame(f) | f in FRAME }
+ { send-frame-or-error(f), receive-frame-or-error(f)
| f in FRAME }
+ { send-ack(a), receive-ack(a) | a in ACK }
+ { send-ack-or-error(a), receive-ack-or-error(a) | a in ACK }
I = { frame-comm(f), frame-or-error(f) | f in FRAME }
+ { ack-comm(a), ack-or-error(a) | a in ACK }
of BIT
Bit-Set = { 0, 1 }
communications
send-frame(f) | receive-frame(f) = frame-comm(f) for f in FRAME
send-frame-or-error(f) | receive-frame-or-error(f) =
frame-or-error(f) for f in FRAME
send-ack(a) | receive-ack(a) = ack-comm(a) for a in ACK
send-ack-or-error(a) | receive-ack-or-error(a) =
ack-or-error(a) for a in ACK
variables
f : -> FRAME
b : -> BIT
d : -> DATA
a : -> ACK
definitions
Sender = Receive-Message(0)
Receive-Message(b) = sum(d in DATA, input(d) . Send-Frame(b,d))
Send-Frame(b,d) = send-frame(frame(b,d)) . Receive-Ack(b,d)
Receive-Ack(b,d) = (
receive-ack-or-error(ack(flip(b)))
+ receive-ack-or-error(ack-error)
) . Send-Frame(b,d)
+ receive-ack-or-error(ack(b)) . Receive-Message(flip(b))
K = sum(d in DATA, sum(b in Bit-Set, receive-frame(frame(b,d)) . K(b,d) ))
K(b,d) = (
skip . send-frame-or-error(frame(b,d))
+ skip . send-frame-or-error(frame-error)
) . K
Receiver = Receive-Frame(0)
Receive-Frame(b) = (
sum(d in DATA, receive-frame-or-error(frame(flip(b),d)))
+ receive-frame-or-error(frame-error)
) . Send-Ack(flip(b))
+ sum(d in DATA, receive-frame-or-error(frame(b,d)) .
Send-Message(b,d)
)
Send-Ack(b) = send-ack(ack(b)) . Receive-Frame(flip(b))
Send-Message(b,d) = output(d) . Send-Ack(b)
L = sum(b in Bit-Set, receive-ack(ack(b)) . L(b) )
L(b) = (
skip . send-ack-or-error(ack(b))
+ skip . send-ack-or-error(ack-error)
) . L
ABP = hide(I, encaps(H, Sender || Receiver || K || L ))
end ABP
Compilation
Assuming the specification resides in file
ABP, it should be
compiled with the command:
% psf -s ABP
Simulation
Compilation gives the file
ABP.til, which can be simulated with
the command:
% sim ABP.til
Choose
ABP as start process.
Animation
With the tool
simanim we can combine the simulation with animation.
For the animation we use:
Anim::Windows 440 220 -text 61 10
Anim::CreateItem recti rect 30 110 20 20 "I"
Anim::CreateItem ovals oval 120 110 20 20 "S"
Anim::CreateItem ovalr oval 360 110 20 20 "R"
Anim::CreateItem rectl rect 240 30 40 10 "L"
Anim::CreateItem rectk rect 240 190 40 10 "K"
Anim::CreateLine toS pos 50 110 item ovals chop -arrow last
Anim::TextposLine toS toS s
Anim::CreateLine fromR item ovalr chop pos 430 110 -arrow last
Anim::TextposLine fromR fromR s
Anim::CreateLine StoK item ovals se item rectk w -arrow last
Anim::TextposLine StoK StoK ne
Anim::TextposItem atK rectk s n
Anim::CreateLine KtoR item rectk e item ovalr sw -arrow last
Anim::TextposLine KtoR KtoR nw
Anim::CreateLine RtoL item ovalr nw item rectl e -arrow last
Anim::TextposLine RtoL RtoL sw
Anim::TextposItem atL rectl n s
Anim::CreateLine LtoS item rectl w item ovals ne -arrow last
Anim::TextposLine LtoS LtoS se
proc ANIM_action {line} {
if {[regexp {^input\('(.*)\)$} $line match arg1]} {
Anim::Clear recti
Anim::Clear ovals
Anim::CreateText toS "$arg1"
Anim::ActivateLine toS
Anim::AddClear ovals {line toS} {text toS}
} elseif {[regexp {^skip frame-comm\(frame\((.*), '(.*)\)\)$} $line match arg1 arg2]} {
Anim::Clear ovals
Anim::CreateText StoK "$arg2 ($arg1)"
Anim::ActivateLine StoK
Anim::AddClear rectk {line StoK} {text StoK}
} elseif {[regexp {^skip<(0|1)>$} $line match]} {
Anim::Clear rectk
Anim::CreateText atK "$match"
Anim::AddClear rectk {text atK}
} elseif {[regexp {^skip frame-or-error\(frame\((.*), '(.*)\)\)$} $line match arg1 arg2]} {
Anim::Clear rectk
Anim::CreateText KtoR "$arg2 ($arg1)"
Anim::ActivateLine KtoR
Anim::AddClear ovalr {line KtoR} {text KtoR}
} elseif {[regexp {^skip frame-or-error\(frame-error\)$} $line match]} {
Anim::Clear rectk
Anim::CreateText KtoR "error"
Anim::ActivateLine KtoR
Anim::AddClear ovalr {line KtoR} {text KtoR}
} elseif {[regexp {^output\('(.*)\)$} $line match arg1]} {
Anim::Clear ovalr
Anim::CreateText fromR "$arg1"
Anim::ActivateLine fromR
Anim::AddClear ovalr {line fromR} {text fromR}
} elseif {[regexp {^skip ack-comm\(ack\((.*)\)\)$} $line match arg1]} {
Anim::Clear ovalr
Anim::CreateText RtoL "ack($arg1)"
Anim::ActivateLine RtoL
Anim::AddClear rectl {line RtoL} {text RtoL}
} elseif {[regexp {^skip<(2|3)>$} $line match]} {
Anim::Clear rectl
Anim::CreateText atL "$match"
Anim::AddClear rectl {text atL}
} elseif {[regexp {^skip ack-or-error\(ack\((.*)\)\)$} $line match arg1]} {
Anim::Clear rectl
Anim::CreateText LtoS "ack($arg1)"
Anim::ActivateLine LtoS
Anim::AddClear recti {line LtoS} {text LtoS}
Anim::AddClear ovals {line LtoS} {text LtoS}
} elseif {[regexp {^skip ack-or-error\(ack-error\)$} $line match]} {
Anim::Clear rectl
Anim::CreateText LtoS "error"
Anim::ActivateLine LtoS
Anim::AddClear ovals {line LtoS} {text LtoS}
}
}
proc ANIM_choose {line} {
if {[regexp {^input\('(.*)\)$} $line match arg1]} {
Anim::AddList recti $match
} elseif {[regexp {^skip frame-comm\(frame\((.*), '(.*)\)\)$} $line match arg1 arg2]} {
Anim::AddList ovals $match
} elseif {[regexp {^skip<(0|1)>$} $line match]} {
Anim::AddList rectk $match
} elseif {[regexp {^skip frame-or-error\(frame\((.*), '(.*)\)\)$} $line match arg1 arg2]} {
Anim::AddList rectk $match
} elseif {[regexp {^skip frame-or-error\(frame-error\)$} $line match]} {
Anim::AddList rectk $match
} elseif {[regexp {^output\('(.*)\)$} $line match arg1]} {
Anim::AddList ovalr $match
} elseif {[regexp {^skip ack-comm\(ack\((.*)\)\)$} $line match arg1]} {
Anim::AddList ovalr $match
} elseif {[regexp {^skip<(2|3)>$} $line match]} {
Anim::AddList rectl $match
} elseif {[regexp {^skip ack-or-error\(ack\((.*)\)\)$} $line match arg1]} {
Anim::AddList rectl $match
} elseif {[regexp {^skip ack-or-error\(ack-error\)$} $line match]} {
Anim::AddList rectl $match
}
}
Assuming the animation resides in file
abp.tcl we can start
the animation with the command:
% simanim ABP.til abp.tcl
