The Concurrent Alternating Bit Protocol

• Description
• Specification
• Compilation
• Simulation
• Animation

Description

Specification

data module CABP-data
begin
    exports
    begin
	sorts
	    BIT,
	    DATA,
	    FRAME,
	    ACK
	functions
	    0 : -> BIT
	    1 : -> BIT
	    inv : BIT -> BIT
	    'a : -> DATA
	    'b : -> DATA
	    'c : -> DATA
	    'd : -> DATA
	    'e : -> DATA
	    frame : DATA # BIT -> FRAME
	    ack : BIT -> FRAME
	    ce : -> FRAME
	    ae : -> FRAME
	    ac : -> FRAME
    end
    equations
    [B1] inv(0) = 1
    [B2] inv(1) = 0
end CABP-data

process module CABP
begin
    imports
	CABP-data
    atoms
	input : DATA
	output : DATA
	send-SK : FRAME
	rec-SK : FRAME
	comm-SK : FRAME
	send-KR : FRAME
	rec-KR : FRAME
	comm-KR : FRAME
	send-RAS : FRAME
	rec-RAS : FRAME
	comm-RAS : FRAME
	send-ASL : FRAME
	rec-ASL : FRAME
	comm-ASL : FRAME
	send-LAR : FRAME
	rec-LAR : FRAME
	comm-LAR : FRAME
	send-ARS : FRAME
	rec-ARS : FRAME
	comm-ARS : FRAME
    processes
	S
	Receive-Message : BIT
	Send-Frame : FRAME
	K
	K : FRAME
	R
	Receive-Frame : BIT
	AS
	Ack-Sender : BIT
	L
	L : BIT
	AR
	Ack-Receiver : BIT
	CABP
    sets
	of DATA
	    DATA-set = { 'a, 'b, 'c, 'd, 'e }
	of BIT
	    BIT-set = { 0, 1 }
	of atoms
	    H = { send-SK(fr), rec-SK(fr),
		send-KR(fr), rec-KR(fr),
		send-RAS(fr), rec-RAS(fr),
		send-ASL(fr), rec-ASL(fr),
		send-LAR(fr), rec-LAR(fr),
		send-ARS(fr), rec-ARS(fr) | fr in FRAME }
    communications
	send-SK(fr) | rec-SK(fr) = comm-SK(fr) for fr in FRAME
	send-KR(fr) | rec-KR(fr) = comm-KR(fr) for fr in FRAME
	send-RAS(fr) | rec-RAS(fr) = comm-RAS(fr) for fr in FRAME
	send-ASL(fr) | rec-ASL(fr) = comm-ASL(fr) for fr in FRAME
	send-LAR(fr) | rec-LAR(fr) = comm-LAR(fr) for fr in FRAME
	send-ARS(fr) | rec-ARS(fr) = comm-ARS(fr) for fr in FRAME
    variables
	b : -> BIT
	d : -> DATA
	fr : -> FRAME
    definitions
	S = Receive-Message(0)
	Receive-Message(b) = sum(d in DATA-set, input(d) . Send-Frame(frame(d, b)))
	Send-Frame(frame(d, b)) =
			send-SK(frame(d, b)) .
			Send-Frame(frame(d, b))
		    +   rec-ARS(ac) .
			Receive-Message(inv(b))

	K = sum(fr in FRAME, rec-SK(fr) . K(fr))
	K(fr) = (
		    skip .
		    send-KR(fr)
		+   skip .
		    send-KR(ce)
		+   skip
		) . K

	R = Receive-Frame(0)
	Receive-Frame(b) =
		    sum(d in DATA-set,
			rec-KR(frame(d, b)) .
			output(d) .
			send-RAS(ac) .
			Receive-Frame(inv(b))
		    )
		+   sum(d in DATA-set,
			rec-KR(frame(d, inv(b))) .
			Receive-Frame(b)
		    )
		+   rec-KR(ce) .
		    Receive-Frame(b)

	AS = Ack-Sender(1)
	Ack-Sender(b) =
		    rec-RAS(ac) .
		    Ack-Sender(inv(b))
		+   send-ASL(ack(b)) .
		    Ack-Sender(b)

	L = sum(b in BIT-set, rec-ASL(ack(b)) . L(b))
	L(b) = (
		    skip .
		    send-LAR(ack(b))
		+   skip .
		    send-LAR(ae)
		+   skip
		) . L

	AR = Ack-Receiver(0)
	Ack-Receiver(b) =
		    (
			rec-LAR(ae)
		    +   rec-LAR(ack(inv(b)))
		    ) . Ack-Receiver(b)
		+   rec-LAR(ack(b)) .
		    send-ARS(ac) .
		    Ack-Receiver(inv(b))

	CABP = encaps(H, S || K || R || AS || L || AR)
end CABP

Compilation

Assuming the specification resides in file CABP, it should be compiled with the command:

% psf -s CABP

Simulation

Compilation gives the file CABP.til, which can be simulated with the command:

% sim CABP.til

Choose CABP as start process.

Animation

With the tool simanim we can combine the simulation with animation. For the animation we use:

Anim::Windows 440 200 -text 61 10

Anim::CreateItem recti rect 30 150 20 20 "I"
Anim::CreateItem ovals oval 120 150 20 20 "S"
Anim::CreateItem rectk rect 240 150 40 10 "K"
Anim::CreateItem ovalr oval 360 150 20 20 "R"
Anim::CreateItem rectl rect 240 50 40 10 "L"
Anim::CreateItem ovalas oval 360 50 20 20 "AS"
Anim::CreateItem ovalar oval 120 50 20 20 "AR"

Anim::CreateLine toS item recti e item ovals chop -arrow last
Anim::TextposLine toS toS s
Anim::CreateLine StoK item ovals chop item rectk w -arrow last
Anim::TextposLine StoK StoK n
Anim::TextposItem atK rectk s n
Anim::CreateLine KtoR item rectk e item ovalr chop -arrow last
Anim::TextposLine KtoR KtoR n
Anim::CreateLine fromR item ovalr chop pos 430 150 -arrow last
Anim::TextposLine fromR fromR s

Anim::CreateLine RtoAS item ovalr chop item ovalas chop -arrow last
Anim::TextposLine RtoAS RtoAS w
Anim::CreateLine AStoL item ovalas chop item rectl e -arrow last
Anim::TextposLine AStoL AStoL s
Anim::TextposItem atL rectl n s
Anim::CreateLine LtoAR item rectl w item ovalar chop -arrow last
Anim::TextposLine LtoAR LtoAR s
Anim::CreateLine ARtoS item ovalar chop item ovals chop -arrow last
Anim::TextposLine ARtoS ARtoS e

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 {^comm-SK\(frame\('(.*), (.*)\)\)$} $line match arg1 arg2]} {
	Anim::Clear ovals
	Anim::CreateText StoK "$arg1 ($arg2)"
	Anim::ActivateLine StoK
	Anim::AddClear rectk {line StoK} {text StoK}
    } elseif {[regexp {^skip<(0|1|2)>$} $line match]} {
	Anim::Clear rectk
	Anim::CreateText atK "$match"
	Anim::AddClear rectk {text atK}
    } elseif {[regexp {^comm-KR\(frame\('(.*), (.*)\)\)$} $line match arg1 arg2]} {
	Anim::Clear rectk
	Anim::Clear ovalr
	Anim::CreateText KtoR "$arg1 ($arg2)"
	Anim::ActivateLine KtoR
	Anim::AddClear ovalr {line KtoR} {text KtoR}
    } elseif {[regexp {^comm-KR\((.*)\)$} $line match arg1]} {
	Anim::Clear rectk
	Anim::Clear ovalr
	Anim::CreateText KtoR "$arg1"
	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 {^comm-RAS\((.*)\)$} $line match arg1]} {
	Anim::Clear ovalr
	Anim::CreateText RtoAS "$arg1"
	Anim::ActivateLine RtoAS
	Anim::AddClear ovalas {line RtoAS} {text RtoAS}
    } elseif {[regexp {^comm-ASL\((.*)\)$} $line match arg1]} {
	Anim::Clear ovalas
	Anim::CreateText AStoL "$arg1"
	Anim::ActivateLine AStoL
	Anim::AddClear ovalas {line AStoL} {text AStoL}
    } elseif {[regexp {^skip<(3|4|5)>$} $line match]} {
	Anim::Clear ovalas
	Anim::CreateText atL "$match"
	Anim::AddClear rectl {text atL}
    } elseif {[regexp {^comm-LAR\((.*)\)$} $line match arg1]} {
	Anim::Clear rectl
	Anim::Clear ovalar
	Anim::CreateText LtoAR "$arg1"
	Anim::ActivateLine LtoAR
	Anim::AddClear ovalar {line LtoAR} {text LtoAR}
    } elseif {[regexp {^comm-ARS\((.*)\)$} $line match arg1]} {
	Anim::Clear ovalar
	Anim::CreateText ARtoS "$arg1"
	Anim::ActivateLine ARtoS
	Anim::AddClear ovals {line ARtoS} {text ARtoS}
    }
}

proc ANIM_choose {line} {
    if {[regexp {^input\('(.*)\)$} $line match arg1]} {
	Anim::AddList recti $match
    } elseif {[regexp {^comm-SK\(frame\('(.*), (.*)\)\)$} $line match arg1 arg2]} {
	Anim::AddList ovals $match
    } elseif {[regexp {^skip<(0|1|2)>$} $line match]} {
	Anim::AddList rectk $match
    } elseif {[regexp {^comm-KR\(frame\('(.*), (.*)\)\)$} $line match arg1 arg2]} {
	Anim::AddList rectk $match
    } elseif {[regexp {^comm-KR\((.*)\)$} $line match arg1]} {
	Anim::AddList rectk $match
    } elseif {[regexp {^output\('(.*)\)$} $line match arg1]} {
	Anim::AddList ovalr $match
    } elseif {[regexp {^comm-RAS\((.*)\)$} $line match arg1]} {
	Anim::AddList ovalr $match
    } elseif {[regexp {^comm-ASL\((.*)\)$} $line match arg1]} {
	Anim::AddList ovalas $match
    } elseif {[regexp {^skip<(3|4|5)>$} $line match]} {
	Anim::AddList rectl $match
    } elseif {[regexp {^comm-LAR\((.*)\)$} $line match arg1]} {
	Anim::AddList rectl $match
    } elseif {[regexp {^comm-ARS\((.*)\)$} $line match arg1]} {
	Anim::AddList ovalar $match
    }
}

Assuming the animation resides in file cabp.tcl we can start the animation with the command:

% simanim CABP.til cabp.tcl