-- teleph.csp
-- The binary switching network (Example 13.3.4)
include "compression.csp"
transparent normal
transparent sbisim
transparent diamond
transparent explicate
sbd(P) = sbisim(diamond(sbisim(P)))
-- The node definition is that from the book, and abstracts away from
-- the choice mechanisms about routing messages:
Node(in,out,swin,swout) = in -> (out -> Node (in,out,swin,swout)
|~| Node'(in,out,swin,swout))
[] swin -> out -> Node(in,out,swin,swout)
Node'(in,out,swin,swout) = swout -> Node(in,out,swin,swout)
[] swin -> out -> Node'(in,out,swin,swout)
-- Especially for ProBE, it would make sense to produce a version with
-- the choice mechanisms implemented properly using the algorithm
-- described in the text.
-- Our system will be based on a power of two, with a total of K * 2^K
-- of the above node processes. The following works fairly easily;
-- 4 is rather slow and anything bigger out of range at the moment.
K = 3
-- Each lane is essentially parameterized by a K-bit binary number:
lanes(0) = <<>>
lanes(n) = <<0>^l, <1>^l | l <- lanes(n-1)>
Lanes = set(lanes(K))
LaneList = lanes(K)
-- The implemented channels are:
channel down: Lanes.{0..K}
channel over: Lanes.{0..K-1}
-- So the ith node in lane l is
NODE(l,i) = normal(Node(down.l.i,down.l.i+1,over.l.i,over.c(l,i).i))
-- where, as usual,
nth(0,xs) = head(xs)
nth(n,xs) = nth(n-1,tail(xs))
-- and the dual of this node is the ith in lane c(l,i):
c(l,i) = >
cb(i,j,b) = if i==j then 1-b else b
-- The alphabet of the node is
Alpha(l,i) = {down.l.i, down.l.i+1, over.l.i, over.c(l,i).i}
-- As a process list, lane l becomes
Lane(l) = <(NODE(l,K-i),Alpha(l,K-i)) | i <- <1..K>>
-- So the entire network becomes (as a structured network)
System =
-- and the uncompressed, unabstracted network is
SYSTEM = StructuredPar(System)\{|over|}
-- You can try this on ProBE for K <= 3.
-- These lanes appear to be the most sensible structures to compress
-- when exploiting compression functions. After carrying out the
-- hiding permitted by the abstracted deadlock check it turns out that
-- (independent of K) the lane process normalises to a single state.
-- This depends on being able to hide the whole of {|down|} in the lane,
-- and the partially constructed lanes do not normalize nearly as
-- well.
-- The most efficient strategy (this being an issue when K=4) appears
-- to be to inductively build up the lanes using one compression
-- function and then apply normalisation before combining them
-- together. This is not supported by any one of the standard compression
-- strategies so we have to piece two of them together:
CompLane(l) = normal(InductiveCompress(sbd)(Lane(l))({|down|}))
-- We can then piece these together, doubling up and compressing
AlphaL(l) = Union({Alpha(l,i) | i <- {0..K-1}})
AlphaLS(ll) = if #ll==K then AlphaL(ll)
else union(AlphaLS(ll^<0>),AlphaLS(ll^<1>))
LANES(ll) = if #ll==K then CompLane(ll)
else let IF = inter(AlphaLS(ll^<0>),AlphaLS(ll^<1>))
within
normal((LANES(ll^<0>) [|IF|] LANES(ll^<1>))\IF)
-- The main deadlock check is then
assert LANES(<>) :[deadlock free [F]]
-- which can be compared to the uncompressed version
assert SYSTEM :[deadlock free [F]]
-- which only works for K<=2 as this system has 4^(K*2^K) states