-- 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(<A | (P,A) <- ps>))

-- 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 = <alphabet(ps) | ps <- pss>
			 ss = <Union({inter(nth(i,as),nth(j,as)) | 
				j <- {0..N-1}, j!=i}) | i <- <0..N-1>>  
			 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(<(alphabet(ps),ListPar(ps)) | ps <- pss>)

-- and the mixed abstraction analogue:

StructuredMixedAbs(compress)(pss)(X,S) =
                         let N = #pss
			 as = <alphabet(ps) | ps <- pss>
			 ss = <Union({inter(nth(i,as),nth(j,as)) | 
				j <- {0..N-1}, j!=i}) | i <- <0..N-1>>  
			 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 <xs>
                  else let 
                         m=if (xl/n)*n==xl then n else (n+1)
                    within
                    <take(m)(xs)>^groupsof(n)(drop(m)(xs))

take(n)(xs) = if n==0 then <> else <head(xs)>^take(n-1)(tail(xs))

drop(n)(xs) = if n==0 then xs else drop(n-1)(tail(xs))