-- compression.csp
-- This file supports various semi-automated compression techniques over
-- CSP networks.
-- The present version is that of September 1997
-- Bill Roscoe
-- In this version we assume that networks are presented to us as
-- structures comprising process/alphabet pairs arranged in list
-- arrangements.
-- The alphabet of any such list is the union of the alphabets of
-- the component processes:
alphabet(ps) = Union(set())
-- The vocabulary of a list is the set of events that are synchronised
-- between at least two members:
vocabulary(ps) = if #ps<2 then {} else
let A = snd(head(ps))
V = vocabulary(tail(ps))
A' = alphabet(tail(ps))
within
union(V,inter(A,A'))
-- The following is a function
-- that composes a process/alphabet list without any
-- compression:
ListPar(ps) = let N=#ps within
|| i:{0..N-1} @ [snd(nth(i,ps))] fst(nth(i,ps))
-- The most elementary transformation we can do on a network is to
-- hide all events in individual processes that are neither relevant to
-- the specification nor are required for higher synchronisation.
-- The following function takes as its (curried) arguments a compression
-- function to apply at the leaves, a process/alphabet list to compose
-- in parallel and a set of events which it is desired to hide (either
-- because they are genuinely internal events or irrelevant to the spec).
-- It hides as much as it can in the processes, but does not combine them
CompressLeaves(compress)(ps)(X) = let V = vocabulary(ps)
N = #ps
H = diff(X,V)
within
<(compress(P\inter(A,H)),diff(A,H)) | (P,A) <- ps>
-- The following uses this to produce a combined process
LeafCompress(compress)(ps)(X) = ListPar(CompressLeaves(compress)(ps)(X))\X
-- It is often advantageous to be able to apply lazy or mixed abstraction
-- operators in the same sort of way as the above does for hiding. The
-- following are two functions that generalize the above: they take a
-- pair of event-sets (X,S): X is the set we want to abstract and S is
-- the set of signal events (which need not be a subset of X). The
-- result is that inter(X,S) is hidden and diff(X,S) is lazily
-- abstracted. Note that you can get the effect of pure hiding (eager
-- abstraction by setting S=Events) and pure lazy abstraction by setting
-- S={}. Note also, however, that if you are trying to lazily abstract
-- a network with some natural hiding in it, that all these hidden events
-- should be treated as signals.
LeafMixedAbs(compress)(ps)(X,S) =
let V = vocabulary(ps)
N = #ps
D = diff(X,S)
H'= diff(X,V)
within
<(compress((P[|inter(A,D)|]
compress(CHAOS(inter(A,D))))\inter(A,H')),diff(A,H'))
| (P,A) <- ps>
-- The substantive function is then:
MixedAbsLeafCompress(compress)(ps)(X,S) =
ListPar(LeafMixedAbs(compress)(ps)(X,S))\X
-- The next transformation builds up a list network in the order defined
-- in the (reverse of) the list, applying a specified compression function
-- to each partially constructed unit.
InductiveCompress(compress)(ps)(X) =
compress(IComp(compress)(CompressLeaves(compress)(ps)(X))(X))
IComp(compress)(ps)(X) = let p = head(ps)
P = fst(p)
A = snd(p)
A' = alphabet(ps')
ps' = tail(ps)
within
if #ps == 1 then P\X
else
let Q = IComp(compress)(ps')(diff(X,A))
within
(P[A||A']compress(Q))\inter(X,A)
InductiveMixedAbs(compress)(ps)(X,S) =
compress(IComp(compress)(LeafMixedAbs(compress)(ps)(X,S))(X))
-- Sometimes compressed subnetworks grow to big to make the above
-- function conveniently applicable. The following function allows you
-- to compress each of a list-of-lists of processes, and then
-- combine them all without trying to compress any further.
StructuredCompress(compress)(pss)(X) =
let N = #pss
as =
ss = >
within
(ListPar(<(compress(
InductiveCompress(compress)(nth(i,
pss))(diff(X,nth(i,ss)))
\(diff(X,nth(i,ss)))),
nth(i,as)) | i <- <0..N-1>>))\X
-- The analogue of ListPar
StructuredPar(pss) = ListPar(<(ListPar(ps),alphabet(ps)) | ps <- pss>)
-- and the mixed abstraction analogue:
StructuredMixedAbs(compress)(pss)(X,S) =
let N = #pss
as =
ss = >
within
(ListPar(<(compress(
InductiveMixedAbs(compress)(nth(i,
pss))(diff(X,nth(i,ss)),S)
\(diff(X,nth(i,ss)))),
nth(i,as)) | i <- <0..N-1>>))\X
-- The following are some functional programming constructs used above
nth(i,xs) = if i==0 then head(xs)
else nth(i-1,tail(xs))
fst((x,y)) = x
snd((x,y)) = y
-- The following function can be useful for partitioning a process list
-- into roughly equal-sized pieces for structured compression
groupsof(n)(xs) = let xl=#xs within
if xl==0 then <> else
if xl<=n or n==0 then
else let
m=if (xl/n)*n==xl then n else (n+1)
within
^groupsof(n)(drop(m)(xs))
take(n)(xs) = if n==0 then <> else ^take(n-1)(tail(xs))
drop(n)(xs) = if n==0 then xs else drop(n-1)(tail(xs))