PSF - Process Specification Formalism

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.
image of ABP
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