\documentstyle[11pt,zed,a4wide]{article}
\hyphenation{euro-gam}
\def\EG{EuroGam}
\def\T#1{\hbox{\tt #1}}
\def\N#1{\hbox{\rm #1}}
\def\nt#1{\hbox{\sf #1}}
\def\lb{\hbox{\it [}}
\def\rb{\hbox{\it ]}}
\def\signed#1#2{{\unskip\nobreak\hfil\penalty50
  \hskip2em\hbox{}\nobreak\hfil#1\quad#2
  \parfillskip=0pt \finalhyphendemerits=0 \par}}       % TeXBook, p106
 
\title{Eurogam Frontend Crate Server}
\author{David Brightly}
\date{Edition 1.0\\September 1990}
\begin{document}
\begin{titlepage}
% a front or cover page for EG docs suitable for inclusion inside
% a titlepage environment in a LaTeX document
% for use with Plain TeX uncomment the \nopagenumbers and the \eject
 
\hoffset=.5in
\hsize=5.25in
\vsize=10.25in
%---gives left and right margins of 1.5in
\font\small=cmssbx10 scaled \magstep2
\font\medium=cmssbx10 scaled \magstep3
\font\large=cmssbx10 scaled \magstep4
%\nopagenumbers
\hrule height 0pt
\parindent=0pt
%\parskip=0pt
\hskip 3.9in
\large
EDOC024\par
\vskip .5in
\large
EUROGAM PROJECT\par
\vskip 1.5in
\hrule height 2pt
\vskip 20pt
\large
NSF DATA ACQUISITION SYSTEM\par
\vskip .5in
\baselineskip 25pt
Eurogam Frontend Crate Server\par
\vskip 20pt
\hrule height 2pt
\vskip 1in
\medium
Edition 1.0\par
\vskip 5pt
September 1990\par
\vfill
\medium
NSF Software Systems Group\par
\vskip 5pt
UK Science and Engineering Research Council\par
\vskip 5pt
Daresbury Laboratory\par
\vskip .5in
%\eject
\end{titlepage}
\maketitle
% \noindent [This document is not yet complete but there is ample material
% to convey the main ideas.
% People might like to take an early look at it in its present form and
% prepare comments while I'm away over the next two weeks.
% I haven't written up the XDR bindings for all the procedures yet, and
% the section on implementation recommendations needs expansion.
% Author's remarks are in square brackets.
% \signed{D.B.}{Thursday 16 August 1990]}
 
\section{Introduction}     %----------------------------
This document elaborates on the description of a ``Frontend Crate
Server'' outlined in \cite[section 3]{EGSS}.
It defines a program model suitable for use in all \EG\ frontend crates
supporting Ge cards, BGO cards, histogrammer unit, trigger unit, 
and apparatus control and environment monitoring interfaces.
The program models the electronics in a crate as a set of abstract
``registers'' and provides a remote procedure call interface to client
programs running elsewhere whereby programmable registers can be
inspected and updated.
 
Aspects of the program are described in the Z specification language
\cite{Spivey}.
The specification covers the remote procedure call interface and details
of the internal data structures needed to support it. 
The construction of these data structures by compiling a textual description
of a \EG\ hardware configuration is also outlined, together with XDR bindings
for the remotely callable procedures. 
The document concludes with some implementation recommendations and 
general remarks on the software environment in which the program is
expected to run.
 
\section{Crate Management Functions}     %----------------------------
This section will describe how crates are treated as allocatable resources.
We will need to talk about the crates themselves and also about {\sl
capabilities\/}. These are tokens drawn from a large name space, possession
of which by a client program confers access rights to a crate.
For background to the capability concept see any text on distributed
systems, such as \cite{CD}.
\begin{zed}
   [CRATE, CAPABILITY]
\end{zed}
We will consider an environment in which possibly more than one \EG\ system
is available, so we will need a set of crates from which a \EG\ can be built:
\begin{axdef}
   crates: \power CRATE
\end{axdef}
All client-callable server procedures will return a success or failure
report:
\begin{zed}
REPORT ::= ok \mid crate\_not\_known \mid crate\_already\_in\_use 
   \mid capability\_invalid
\end{zed}
Rather than treat crates individually we will adopt for the time being a 
God-like viewpoint which observes the state of all the crates.
Later on we will add further constraints to these schemas so that they
describe single crates.
We have a function which maps allocated crates to the capabilities that
have been issued to confer access to the crates:
\begin{schema}{CrateManager}
   capabilities: CRATE \p\inj CAPABILITY 
\end{schema}   
Initially, no crates are allocated---this would be the state following
a power cut, say.
\begin{schema}{InitCrateManager}
   \Delta CrateManager
\where
   capabilities' = \empty
\end{schema}
To obtain exclusive access to a crate a client submits a known but
unallocated crate and receives in return a capability for that crate.
The only constraint on the capability is that it should not currently
be associated with an allocated crate.
\begin{schema}{ClaimCrateOK}
   \Delta CrateManager  \\
   crate?: CRATE  \\
   capability!: CAPABILITY  \\
\where
   crate? \in crates \\
   crate? \not\in \dom capabilities  \\
   capability! \not\in \ran capabilities  \\
   capabilities' = capabilities \oplus \{crate? \mapsto capability!\}  \\
\end{schema}
A successful operation returns an $ok$ status report:
\begin{schema}{EGOk}
   status!: REPORT
\where
   status! = ok
\end{schema}
Operations may fail for several reasons---the crate may not be one of the set
known to the system:
\begin{schema}{CrateNotKnown}
   \Xi CrateManager  \\
   crate?: CRATE  \\
   status!: REPORT
\where
   crate? \not\in crates  \\
   status! = crate\_not\_known
\end{schema}
---it may already be allocated to another client:
\begin{schema}{CrateAlreadyInUse}
   \Xi CrateManager  \\
   crate?: CRATE  \\
   status!: REPORT
\where
   crate? \in \dom capabilities  \\
   status! = crate\_already\_in\_use
\end{schema}
---or a submitted capability may not match that associated with a crate (perhaps
by accident or possibly through attempted fraud):
\begin{schema}{CapabilityInvalid}
   \Xi CrateManager  \\
   crate?: CRATE  \\
   capability?: CAPABILITY  \\
   status!: REPORT
\where
   crate? \in crates  \\
   capability? \not= capabilities (crate?)  \\
   status! = capability\_invalid
\end{schema}
In none of these failure cases does the state of the system change.
The complete $ClaimCrate$ operation can be summarised as
\begin{zed}
   ClaimCrate \defs (ClaimCrateOk \land EGOk) \lor CrateNotKnown 
       \lor CrateAlreadyInUse
\end{zed}
A client can successfully release a crate providing the crate is currently
allocated and the client knows the associated capability:
\begin{schema}{FreeCrateOk}
   \Delta CrateManager  \\
   crate?: CRATE  \\
   capability?: CAPABILITY \\
   status!: REPORT
\where
   crate? \in \dom capabilities  \\
   capability? = capabilities(crate?) \\
   capabilities' = capabilities \hide \{crate? \mapsto capability!\}  \\
   status! = ok
\end{schema}
Releasing a crate may fail for the additional reason that it is known about
but not in use:
\begin{schema}{CrateNotInUse}
   \Xi CrateManager  \\
   crate?: CRATE  \\
   status!: REPORT
\where
   crate? \in crates  \\
   crate? \not\in \dom capabilities \\
   status! = crate\_not\_in\_use
\end{schema}
The complete $FreeCrate$ operation can be characterised as:
\begin{zed}
   FreeCrate \defs (FreeCrateOk \land EGOk) \lor CrateNotInUse \lor 
      CrateNotKnown \lor CapabilityInvalid
\end{zed}
\clearpage
\section{Specifying a \EG\ Configuration} %----------------------
Earlier papers have posited a software interface to the \EG\ frontend
crates couched in terms of abstract registers which are mapped onto
physical hardware registers in modules.
This section will describe the logical ``infrastructure'' of sets and 
functions needed to support the mapping.
A subsequent section will show how these sets and functions are constructed.
 
\subsection{Given sets}
We will need some ``given sets'' for our specification.
These are essentially the ``types'' of the objects that the specification will
talk about.
\begin{zed}
   [ARRAYPOSITION]
\end{zed}
Objects of type $ARRAYPOSITION$ will denote the ``holes'' in the array into
which detectors are inserted. 
They will be names like G23, denoting a Ge detector position, and
S23d, denoting position d in the surrounding BGO shield.
\begin{zed}
   [DETECTOR]
\end{zed}
Objects of type $DETECTOR$ will denote actual detectors.
They will be names like GUOC17 and SUC11.
\begin{zed}
   [DETECTORTYPE]
\end{zed}
Types of detectors, typically either Ge or BGO.
\begin{zed}
   [MODULE]
\end{zed}
Objects of type $MODULE$ will denote physical modules such as VXI Ge
cards that can occupy slots in crates.
Modules will be individually identified by (say) serial numbers such as G\#003,
denoting the Ge card with serial number 003.
\begin{zed}
   MODULETYPE ::= G \mid B \mid T \mid H \mid RC \mid RM
\end{zed}
Types of modules used in \EG\ such as Ge cards, BGO cards, Trigger units,
Histogrammers, Readout Controllers, and Resource Managers.
\begin{zed}
   [SOCKET]
\end{zed}
Objects of type $SOCKET$ will represent physical labelled sockets on the front
panels of individual modules into which cables can be inserted.
Different modules will have different sockets even if the modules are of
the same type. 
For example, G\#003.BNC1 would refer to BNC socket number 1 on Ge module
G\#003.
\begin{zed}
   [SUBCHANNEL]
\end{zed}
Ge and BGO modules consist of several similar independent subsystems each
serving a single detector.
A $SUBCHANNEL$ will be a small integer denoting one such channel.
\begin{zed}
   [CRATE]
\end{zed}
Objects of type $CRATE$ will represent the individual crates comprising
a \EG\ system, such as VXI1.
\begin{zed}
   [NETADDR]
\end{zed}
Objects of type $NETADDR$ will denote network addresses for the
Resource Manager modules associated with each crate.
These addresses may be IP addresses or host names---it doesn't matter
for the purpose of the specification.
\begin{zed}
   [SLOT]
\end{zed}
Objects of type $SLOT$ will represent slots in crates for modules.
For example, VXI1.N2 will denote slot 2 of crate VXI1.
Note that different crates have different slots.
\begin{zed}
   [REGISTER]
\end{zed}
Objects of type $REGISTER$ will denote abstract names for the software
addressable registers of modules such as G23.PoleZero, G17.E1, and
Trigger.TimingWindow.
Different modules will have different registers even if of the same type.
\begin{zed}
   [PROPERTY]
\end{zed}
Objects of type $PROPERTY$ will represent the abstract properties of
\EG\ modules, such CFD levels, timing windows, and polezero adjusters
with which registers are associated.
The  set of properties can be completed only when the register sets of
each type of module have been finalised.
\begin{zed}
   [VMEADDRESS]
\end{zed}
Objects of type $VMEADDRESS$ will be integers denoting VME addresses.
 
\subsection{Fixed functions}
 
The following functions are independent of any particular \EG\
\sloppy
configuration---they merely extract information implicit in the 
objects they take as arguments.
 
\begin{axdef}
   dtype: DETECTOR \fun DETECTORTYPE  \\
   mtype: MODULE \fun MODULETYPE  \\
   incrate: SLOT \fun CRATE  \\
   onmodule: SOCKET \fun MODULE   \\
   feeds: SOCKET \fun SUBCHANNEL  \\
   atposition: REGISTER \p\fun ARRAYPOSITION  \\
   ofdetector: REGISTER \p\fun DETECTOR  \\
   property: REGISTER \fun PROPERTY  \\
   supportedby: PROPERTY \fun MODULETYPE
\end{axdef}
 
\begin{description}
\item $dtype$ tells what type any detector is.
For example, \[dtype (\N{GUOC17}) = \N{Ge}\]
\item $mytpe$ tells what type any module is.
For example, \[mtype (\N{G\#003}) = \N{G}\]
\item $incrate$ tells which crate any slot belongs to.
For example, \[incrate (\N{VXI1.N3}) = \N{VXI1}\]
\item $onmodule$ tells which module's front panel a socket is on.
For example, \[onmodule (\N{G\#003.BNC1}) = \N{G\#003}\]
\item $feeds$ tells which subchannel of a module a given socket
feeds into.
For example, perhaps \[feeds (\N{G\#003.BNC1}) = 1\]
\item $atposition$ tells which detector position a register refers to.
For example, \[atposition (\N{G23.Bias}) = \N{G23}\]
\item $ofdetector$ tells which detector a register refers to.
For example, \[ofdetector (\N{GUOC17.Bias}) = \N{GUOC17}\]
\item $property$ tells what ``type'' 
each abstract register is.
For example, \[property (\N{G23.Bias}) = \N{Bias}\]
\item $supportedby$ relates properties and module types.
For example, \[supportedby (\N{PoleZero}) = \N{G}\]
\end{description}
We have $atposition$ because we want to name the registers after the
data acquisition channels they control rather than use labels based on
VXI crate and slot positions which won't mean much to users.
However, not all registers will refer to array positions.
Some will refer to aspects of Trigger, Histogrammer, or other modules.
We also want registers that refer to detectors so that, for example,
detector biases can be set in a natural way. 
Hence the $ofdetector$ function.
%\clearpage
\subsection{A \EG\ configuration}
We will represent any particular \EG\ configuration with a 
collection of sets of objects drawn from the above types and some 
functions between them:
 
\begin{schema}{EuroGam}
   holes: \power ARRAYPOSITION \\
   detectors: \power DETECTOR \\
   crates: \power CRATE    \\
   modules: \power MODULE  \\
   slots: \power  SLOT  \\
   sockets: \power SOCKET  \\
   registers:  \power REGISTER  \\
   triggers: \power MODULE  \\
   histogrammers: \power MODULE
\zbreak
   sitsin: DETECTOR \p\inj ARRAYPOSITION  \\
   occupies: MODULE \p\inj SLOT  \\
   basedat: SLOT \p\fun VMEADDRESS \\
   hostedby: CRATE \inj NETADDRESS  \\
   wiredto: ARRAYPOSITION \p\inj SOCKET  \\
   biasedby: ARRAYPOSITION \p\inj SOCKET  
\where
   detectors = \dom sitsin  \\
   holes = \ran sitsin \\
   modules = \dom occupies  \\
   slots = \ran occupies \subseteq \dom basedat
\zbreak
   incrate \limg slots \rimg \subseteq crates \\
   slots \subseteq \dom basedat  \\
   onmodule \limg sockets \rimg \subseteq modules \\
   wiredto \limg holes \rimg \subseteq sockets \\
   atposition \limg registers \rimg = \dom wiredto \cup \dom biasedby
\end{schema}
\begin{description}
\item $holes$ is the set of occupied detector positions in this
particular \EG; this will depend on the mechanical configuration
of the array and detectors.
\item $detectors$ is the set of detectors actually mounted in the
array.
\item $sitsin$ is a function which tells which position each and every
detector occupies.
\item $crates$ is the set of electronics crates associated with the array.
\item $modules$ is the set of modules in the crates.
\item $occupies$ is a function telling which slot is taken by each module.
\item $slots$ is just the set of the occupied slots in crates.
\item $basedat$ is a function returning the VME base address of each
occupied slot.
\item $sockets$ is the set of front panel sockets on all the modules
in the crates.
\item $wiredto$ is a function playing a central role in the 
configuration, telling which VXI module socket every detector position
is cabled to.
\item $biasedby$ is a similar function to $wiredto$, telling which high voltage
bias socket each detector position is connected to.
\item $registers$ is the set of (names of) software controllable 
registers in the modules.
\end{description}
Note that $wiredto$ and $biasedby$ map array positions rather than 
actual detectors to module sockets.
This is because the array cabling will be relatively static---it's the
detectors that will move in and out of the array---and $wiredto$ and $biasedby$
capture this relationship.
 
\subsection{Implementing register access}
This section will show how abstract registers are mapped onto physical
VME addresses by in-crate software.
Essentially, there are three classes of register.
Firstly we have registers referring to specific array positions:
\begin{schema}{LocateArrayRegister}
   \Xi EuroGam  \\
   r? :  REGISTER  \\
   modtype! : MODULETYPE  \\
   crate! : CRATE  \\
   addr! : VMEADDRESS   \\
   prop! : PROPERTY  \\
   subchan! : SUBCHANNEL    
\where
   r? \in \dom atposition \\
   prop! = property(r?)  \\
   modtype! = mtype \circ onmodule \circ wiredto \circ atposition(r?)   \\
   crate! = incrate \circ occupies \circ onmodule \circ wiredto 
           \circ atposition(r?)   \\
   addr! = basedat \circ occupies \circ onmodule \circ wiredto 
           \circ atposition(r?)   \\
   subchan! = feeds \circ wiredto \circ atposition(r?) 
\end{schema}
Secondly, we have registers referring to the trigger unit, histogrammer
unit, and possibly others:
\begin{schema}{LocateGeneralRegister[X]}
   \Xi EuroGam  \\
   r? :  REGISTER  \\
   modtype! : MODULETYPE  \\
   crate! : CRATE  \\
   addr! : VMEADDRESS   \\
   prop! : PROPERTY  \\
   subchan! : SUBCHANNEL    
\where
   \exists m : X \spot  \\
\t1   supportedby \circ property(r?) = mtype (m)  \\   
\t1   prop! = property(r?)  \\
\t1   modtype! = mtype (m)  \\
\t1   crate! = incrate \circ occupies (m)  \\
\t1   addr! = basedat \circ occupies (m)  \\
\t1   subchan! = 0
\end{schema}
Finally, we have registers that refer to particular detectors:
\begin{schema}{LocateDetectorRegister}
   \Xi EuroGam  \\
   r? :  REGISTER  \\
   modtype! : MODULETYPE  \\
   crate! : CRATE  \\
   addr! : VMEADDRESS   \\
   prop! : PROPERTY  \\
   subchan! : SUBCHANNEL    
\where
   r? \in \dom ofdetector \\
   ofdetector (r?) \in \dom sitsin  \\
   prop! = property(r?)  \\
   modtype! = mtype \circ onmodule \circ wiredto \circ sitsin \circ ofdetector(r?) \\
   crate! = incrate \circ occupies \circ onmodule \circ wiredto 
           \circ sitsin \circ ofdetector(r?) \\
   addr! = basedat \circ occupies \circ onmodule \circ wiredto 
           \circ sitsin \circ ofdetector(r?)  \\
   subchan! = feeds \circ wiredto \circ sitsin \circ ofdetector(r?) 
\end{schema}
Combining these, we can locate an arbitrary register:
\begin{zed}
   LocateRegister \defs LocateArrayRegister \lor LocateGeneralRegister[triggers] \\
\t1 \lor LocateGeneralRegister[histogrammers] \lor LocateDetectorRegister
\end{zed}
These schemas assume that to access the hardware we need to know five things:
\begin{itemize}
\item the ``type'' of the register;
\item the type of the module in which the register resides;
\item the crate housing this module;
\item the module's VME base address;
\item which subchannel of the module the register applies to.
\end{itemize}
Note that the constraints on the sets and functions implied by $EuroGam$
guarantee that these outputs are defined. 
 
We will assume that registers hold typed pieces of data drawn from the set
\[[VALUE]\]
and that we have a given relation on values and register properties that tells us
when they are type-comaptible:
\begin{axdef}
   compatible : VALUE \rel PROPERTY
\end{axdef}
A $Read$ operation returns such a value from the hardware:
\begin{schema}{Read}
   \Xi\EG  \\
   modtype? : MODULETYPE  \\
   crate? : CRATE  \\
   addr? : VMEADDRESS   \\
   prop? : PROPERTY  \\
   subchan? : SUBCHANNEL  \\
   value ! : VALUE
\end{schema}
and a $Write$ operation takes a value and applies it to the hardware:
\begin{schema}{Write}
   \Xi\EG  \\
   modtype? : MODULETYPE  \\
   crate? : CRATE  \\
   addr? : VMEADDRESS   \\
   prop? : PROPERTY  \\
   subchan? : SUBCHANNEL  \\
   value? : VALUE
\end{schema}
We will refrain from making any statements about what the hardware system
does with the data.
For example, it need not always be the case that 
\[Write \comp Read \implies value! = value? \]
since we are warned not to expect all hardware registers to be readable.
 
In practice we would associate a procedure or package of procedures with
module type $modtype!$ which could determine a register's VME address given
the $addr!$, $prop!$, and $subchan!$ arguments.
Such a procedure package would have to ``know'' all about the internal register
structure of modules of this type.
 
\section{Register Access Functions}     %----------------------------
This section will describe operations based on the abstract registers
introduced previously.
First, a schema encapsulating the crate access protection mechanism
which we will use to abbreviate the descriptions:
\begin{schema}{CrateAccess}
   \Xi CrateManager  \\
   crate?: CRATE  \\
   capability?: CAPABILITY
\where
   capability? = capabilities (crate?)
\end{schema}
To read a register successfully a client must submit a valid crate 
and corresponding capability, and a register which resides in that
crate. 
The value currently held in the register is returned.
\begin{schema}{ReadRegisterOk}
   \Xi\EG  \\
   CrateAccess  \\
   register?: REGISTER  \\
   value!: VALUE
\where
   register? \in registers  \\
   LocateRegister \comp Read
\end{schema}
Writing a register successfully requires the client to submit in addition a
value which is type-compatible with the register.
The register is updated with the value submitted.
\begin{schema}{WriteRegisterOk}
   \Xi\EG  \\
   CrateAccess  \\
   register?: REGISTER  \\
   value?: VALUE
\where
   register? \in registers  \\
   (value?, property (register?)) \in compatible  \\
   LocateRegister \comp Write
\end{schema}
Initialising a register is like writing it except that the value 
comes from the server not the client.
We will assume that for each register the server knows a safe value.
In practice, it is likely that registers sharing the same property will
also share the same safe value.
\begin{axdef}
   safe: REGISTER \fun VALUE
\end{axdef}
\begin{zed}
   InitialiseRegisterOk \defs WriteRegisterOk [safe(register?)/value?]
\end{zed}
The next operations use a pattern argument to select registers.
For the time being we will regard the pattern matching as a given
relation between registers and patterns:
\begin{zed}
   [PATTERN]
\end{zed}
\begin{axdef}
   matches: REGISTER \rel PATTERN
\end{axdef}
The simplest pattern matching operation returns the set of registers
that match a submitted pattern:
\begin{schema}{InquireRegistersOk}
   \Xi\EG  \\
   CrateAccess  \\
   pattern?: PATTERN  \\
   rlist!: \power REGISTER
\where
   \forall r:REGISTER \mid r \in registers \spot  \\
\t1   r \in rlist! \iff (r,pattern?) \in matches
\end{schema}
Next, we submit a pattern and are returned a set of pairs of registers
and their corresponding values:
\begin{schema}{ReadRegistersOk}
   \Xi\EG  \\
   CrateAccess  \\
   pattern?: PATTERN  \\
   rvlist!: \power REGISTER \cross VALUE
\where
   \forall r:REGISTER; v:VALUE \mid r \in registers \spot  \\
\t1   (r,v) \in rvlist! \iff  \\
\t2     (r,pattern?) \in matches \land  \\
\t3        (LocateRegister \comp Read) [v/value!,r/register?]
\end{schema}
We can write a single value to a set of registers that match a pattern
and are type-compatible with the submitted value:
\begin{schema}{WriteRegistersOk}
   \Xi\EG  \\
   CrateAccess  \\
   pattern?: PATTERN  \\
   value?: VALUE  
\where
   \forall r:REGISTER \mid r \in registers \spot  \\
\t1    (r,pattern?) \in matches \land (value?, property(r)) \in compatible \implies  \\
\t2       (LocateRegister \comp Write) [r/register?]
\end{schema}
And we can load safe values into all registers matching a pattern:
\begin{schema}{InitialiseRegistersOk}
   \Xi\EG  \\
   CrateAccess  \\
   pattern?: PATTERN  \\
   value?: VALUE  
\where
   \forall r:REGISTER \mid r \in registers \spot  \\
\t1     (r,pattern?) \in matches \implies  \\
\t2        (LocateRegister \comp Write) [safe (r)/value?,r/register?]
\end{schema}
Operations specifying registers by name rather than by a pattern can fail
because the register submitted is unknown:
\begin{schema}{RegisterNotKnown}
   \Xi\EG  \\
   register?: REGISTER  \\
   status!: REPORT
\where
   register? \not\in registers  \\
   status! = register\_not\_known
\end{schema}
A specific write operation may fail because of a type incompatibility:
\begin{schema}{TypesIncompatible}
   \Xi\EG  \\
   register?: REGISTER  \\
   value? : VALUE  \\
   status!: REPORT
\where
   register? \in registers  \\
   (value?, property(register?)) \not\in compatible  \\
   status! = types\_incompatible
\end{schema}
Finally, we can describe robust register access functions:
\begin{zed}
   ReadRegister \defs (ReadRegisterOk \land EGOk) \lor CrateNotInUse 
       \lor CapabilityInvalid \\ \t1 \lor RegisterNotKnown   \\
   WriteRegister \defs (WriteRegisterOk \land EGOk) \lor CrateNotInUse 
       \lor CapabilityInvalid \\ \t1 \lor RegisterNotKnown \lor TypesIncompatible  \\
   InitialiseRegister \defs (InitialiseRegisterOk \land EGOk) \lor CrateNotInUse 
       \lor CapabilityInvalid \\ \t1 \lor RegisterNotKnown   \\
   ReadRegisters \defs (ReadRegistersOk \land EGOk) \lor CrateNotInUse 
       \lor CapabilityInvalid   \\
   WriteRegisters \defs (WriteRegistersOk \land EGOk) \lor CrateNotInUse 
       \lor CapabilityInvalid   \\
   InitialiseRegisters \defs (InitialiseRegistersOk \land EGOk) 
        \lor CrateNotInUse \lor CapabilityInvalid \\
\end{zed}
 
\section{Establishing a Configuration}     %-----------------------------
Each crate has to contain the data structures implied by the
$EuroGam$ schema in order to support register access as outlined
in the previous section.
A simple way of achieving this is to represent the sets and functions
in some sort of configuration description file. 
The frontend software is required to compile the description into
suitable data structures for implementing the $LocateRegister$ schema.
We would expect a \EG\ configuration to change infrequently---perhaps
at the start of an experiment or following replacement of a faulty module.
In these circumstances it is difficult to see how a partly established
set up of register values can be preserved, since crates are likely to
have been power-cycled and module and wiring configuration altered.
Hence we must accept that compiling a configuration from a description file 
will destroy all previously established information.
 
We will need a file in which to record diagnostics (such as syntax errors)
while compiling the description:
\begin{schema}{EuroGamLog}
   log: FILE
\end{schema}
We need not be very specific about the log file contents as long as 
it consists of readable text that helps pinpoint problems with the
configuration.
We would like to be able to read it back at any time though:
\begin{schema}{ReadEuroGamLog}
   \Xi EuroGamLog  \\
   file!: FILE
\where
   file! = log
\end{schema}
The $ConfigureEuroGam$ operation takes a description file, compiles a new
configuration, and updates the log:
\begin{schema}{ConfigureEuroGam}
   \Delta EuroGam  \\
   \Delta EuroGamLog  \\
   description? : FILE
\end{schema}
 
A suitable form for a description file follows quite naturally from the
signature of the $EuroGam$ schema.
\begin{syntax}
  \nt{EGspec}    & ::= & \nt{cratespec}\ldots\nt{cratespec}\;
                         \nt{detectorspec}\ldots\nt{detectorspec}  &\omit \\
  \nt{cratespec} & ::= & \T{crate}\; crate\; \T{host}\; host\;
                  \lb\nt{modulespec}\ldots \nt{modulespec}\rb &\omit \\
  \nt{modulespec} & ::= & \T{module}\; module\; \T{slot}\; slot\;
                  \lb\nt{socketspec}\ldots \nt{socketspec}\rb &\omit \\
  \nt{socketspec} & ::= & \T{socket}\; socket\; \T{wiredfrom}\; position &
                          data connection\\
                  & |   & \T{socket}\; socket\; \T{biases}\; position &
                          HV connection  \\
  \nt{detectorspec} & ::= & \T{detector}\; detector\; \T{position}\; position &\omit
\end{syntax}
For example:
\begin{quote}
\begin{verbatim}
crate VXI1 host NNVA
module G#003 slot 4
socket BNC1 wiredfrom G23
socket BNC2 wiredfrom G24
socket BNC3 wiredfrom G25
module B#007 slot 5
socket IDC1.1 wiredfrom S23a
socket IDC1.2 wiredfrom S23b
module T#002 slot 3
detector GUOC17 position G23
\end{verbatim}
\end{quote}
This describes a crate called VXI1 with network address NNVA.
It has a Ge module, serial \#003, in slot 4. 
BNC socket 1 of this module connects to array position G23,
socket 2 to position G24, and socket 3 to position G25.
In slot 5 of the crate is a BGO module, serial \#007. 
It has an IDC connector IDC1 with pin 1 connected to shield detector
position S23a and pin 2 to S23b.
Trigger unit serial \#002 occupies slot 3.
Germanium detector GUOC17 sits in array position G23.
We can exploit the expected regularity of the structure and cabling
with special pattern-matching syntax, using, say
\begin{quote}
\begin{verbatim}
socket BNC[1-3] wiredfrom G[23-25]
\end{verbatim}
\end{quote}
to abbreviate the first three {\tt socket} lines.
 
Note that we are using the natural structure of ``sockets are on modules 
which occupy slots in crates'' to save duplicating information.
The ``proper name'' of the slot occupied by module G\#003 is VXI1.N4 and 
that of its first socket is G\#003.BNC1.
The syntax of the description file guarantees that the proper names for
these objects can always be recovered.
 
Compiling a description is straightforward.
We start in an initial state in which we know nothing at all:
\begin{schema}{InitEuroGam}
   \Delta EuroGam
\where
   holes' = \empty \land  detectors' = \empty \land  crates' = \empty \\
   modules' = \empty \land  slots' = \empty \land   sockets' = \empty \\
   registers' = \empty \land   sitsin' = \empty \land   occupies' = \empty \\
   hostedby' = \empty \land  wiredto' = \empty \land   biasedby' = \empty
\end{schema}
The description file is trivially parsed and
the full configuration is built up piece by piece.
The following schema applies as soon as a $host$ has been read
while parsing a \nt{cratespec}:
\begin{schema}{InstallCrate}
   \Delta EuroGam \\
   crate? : CRATE  \\
   host? : NETADDRESS 
\where
   crates' = crates \cup \{crate?\}  \\
   hostedby' = hostedby \oplus \{crate? \mapsto host? \}
\end{schema}   
Similarly, $InstallModule$ applies once a $slot$ has been found
when parsing a \nt{modulespec}.
The $slot?$ input is constructed from $slot$ and its immediately
preceeding $crate$.
\begin{schema}{InstallModule}
   \Delta EuroGam  \\
   crate? : CRATE  \\
   module? : MODULE  \\
   slot? : SLOT 
\where
   incrate(slot?) = crate?  \\
   occupies' = occupies \oplus \{module? \mapsto slot? \}
\end{schema}
General modules (i.e. other than Ge and BGO types) introduce a set of
registers when they are installed, and they should be installed only once!
For example:
\begin{schema}{InstallTriggerModule}
   \Delta EuroGam  \\
   module? : MODULE 
\where
   mtype (module?) = \N{T}  \\
   triggers = \empty  \\
   triggers' = \{module?\}   \\
   registers' = registers \cup \\
\t1  \{r:REGISTER \mid supportedby \circ property (r) = mtype (module?)\}
\end{schema}
Detectors can be installed when a \nt{detectorspec} has been parsed:
\begin{schema}{InstallDetector}
   \Delta EuroGam  \\
   detector? : DETECTOR  \\
   position? : ARRAYPOSITION
\where
   detector? \not\in \dom sitsin  \\
   position? \not\in \ran sitsin  \\
   sitsin' = sitsin \oplus \{detector? \mapsto position?\}  \\
   detectors' = detectors \cup \{detector?\}  \\
   holes' = holes \cup \{position?\}  
\end{schema}
A socket can be installed once a complete \nt{socketspec} has been parsed.
Sockets can terminate data connections and bias supply connections:
\begin{schema}{InstallDataSocket}
   InstallSocket
\where
   wiredto' = wiredto \oplus \{ position? \mapsto socket? \} \\
\end{schema}   
\begin{schema}{InstallHVSocket}
   InstallSocket
\where
   biasedby' = biasedby \oplus \{ position? \mapsto socket? \} \\
\end{schema}   
where we have defined
\begin{schema}{InstallSocket}
   \Delta EuroGam  \\
   crate? : CRATE  \\
   module? : MODULE  \\
   socket? : SOCKET \\
   position? : ARRAYPOSITION  
\where
   incrate \circ occupies (module?) = crate?  \\
   onmodule (socket?) = module?  \\
   sockets' = sockets \cup \{ socket? \}  \\
   holes' = holes \cup \{ position? \}  \\
   registers' = registers \cup \\
\t1      \{r:REGISTER \mid atposition(r)=position? \land \\
\t2         supportedby \circ property (r) = mtype (module?) \}
\end{schema}   
Again, $socket?$ is constructed from $socket$ and its immediately
preceeding $module$.
Note how installing a socket extends the set of registers we know about by
just those registers associated with the array position connected up to the
socket.
 
These operations all maintain the predicate of the $EuroGam$ schema.
 
\section{XDR Bindings}             %----------------------------
 
This section details XDR type definitions and procedure bindings for
the operations specified in the previous section.
For background information on XDR see \cite{NP}.
 
First, a set of {\tt typedef}s for objects drawn from our given sets:
\begin{quote}
\begin{verbatim}
typedef string crate<255>;
typedef string register<255>;
typedef string pattern<255>;
typedef string filename<255>;
typedef string bytestring<255>;
typedef opaque capability[4];
typedef opaque cookie[4];
 
enum basictype {
   RV_INT = 1;
   RV_FLOAT = 2;
   RV_BYTESTRING = 3;
   RV_STRING = 4;
   RV_BOOL = 5;
   };
 
union registervalue switch (basictype rvtype) {
   case RV_INT:        int i;
   case RV_FLOAT:      float f;
   case RV_BYTESTRING: bytestring bs;
   case RV_STRING:     string s;
   case RV_BOOL:       bool b;
   };
 
enum report {
   EG_OK = 0;
   EG_CRATE_NOT_KNOWN = 1;
   EG_CRATE_ALREADY_IN_USE = 2;
   EG_CAPABILITY_INVALID = 3;
   EG_REGISTER_NOT_KNOWN = 4;
   EG_TYPES_INCOMPATIBLE = 5;
   }
\end{verbatim}
\end{quote}
All the operations we need return a report parameter indicating the
success of failure of the operation. 
Only if the operation succeeds will further parameters be returned.
Hence all operation outputs are coded in the form:
\begin{quote}
\begin{verbatim}
union reply switch (report r) {
   case EG_OK:   struct success;
   default: void;
   };
\end{verbatim}
\end{quote}
where the {\tt success} structure depends on the particular procedure
invoked.
To save space, in the XDR bindings that follow we will give just
the {\tt success} structures.
The syntax follows that of an earlier version of XDR which is a little
more compact and looks more like function declarations in the C language.
\begin{quote}
\begin{verbatim}
procedure ClaimCrate (c) returns (reply)
   crate c;
   struct success {capability cap;};
 
procedure FreeCrate (cap, c) returns (reply)
   capability cap;
   crate c;
   void success;
 
procedure ConfigureEuroGam (cap, c, f) returns (reply)
   capability cap;
   crate c;
   filename f;
   void success;
 
procedure ReadEuroGamLog (cap, c) returns (reply)
   capability cap;
   crate c;
   struct success {string file;};
 
procedure ReadRegister (cap, c, r) returns (reply)
   capability cap;
   crate c;
   register r;
   struct success {registervalue v;};
 
procedure WriteRegister (cap, c, r, v) returns (reply)
   capability cap;
   crate c;
   register r;
   registervalue v;
   void success;
 
procedure InitialiseRegister (cap, c, r) returns (reply)
   capability cap;
   crate c;
   register r;
   void success;
 
typedef struct {
   register r;
   cookie kk;
   reglist *rr;
   } reglist;
 
typedef struct {
   register r;
   registervalue v;
   cookie kk;
   regvallist *rr;
   } regvallist;
 
procedure InquireRegisters (cap, c, p, k, n) returns (reply)
   capability cap;
   crate c;
   pattern p;
   cookie k;
   int n;
   struct success {
      reglist *regs;
      boolean eol;
      };
 
procedure ReadRegisters (cap, c, p, k, n) returns (reply)
   capability cap;
   crate c;
   pattern p;
   cookie k;
   int n;
   struct success {
      regvallist *regvals;
      boolean eol;
      };
 
procedure WriteRegisters (cap, c, p, v) returns (reply)
   capability cap;
   crate c;
   pattern p;
   registervalue v;
   void success;
 
procedure InitialiseRegisters (cap, c, p) returns (reply)
   capability cap;
   crate c;
   pattern p;
   void success;
\end{verbatim}
\end{quote}
These are all straightforward XDR definitions apart from 
\verb+InquireRegisters+ and \verb+ReadRegisters+ which are potentially
capable of returning unbounded sets of parameters.
We use the technique outlined in \cite[page 179]{NP} to obtain the
full set of parameters in one or more chunks.
\verb+InquireRegisters+ returns a variable length list of register names, 
upto a maximum of \verb+n+ per call, each matching the pattern \verb+p+.
Each register is accompanied by a ``cookie'', \verb+kk+, which is an
opaque pointer to the next register in the list.
Any cookie can be used in a subsequent \verb+InquireRegisters+ call
to obtain further register names starting with the one identified by
the cookie.
To get the list started a special cookie value with all bits zero identifies 
the first entry in the list of matches.
Finally, the boolean \verb+eol+ takes the value \verb+TRUE+ when there are no
more matching registers in the list.
\verb+ReadRegisters+ is very similar, except that each matching register
name is also accompanied by a value.
The encodings for the procedures themselves are:
\begin{quote}
\begin{verbatim}
program FrontendCrateServer {
   version FCSversion {
      procedure ClaimCrate = 1;
      procedure FreeCrate = 2;
      procedure ConfigureEuroGam = 3;
      procedure ReadEuroGamLog = 4;
      procedure ReadRegister = 5;
      procedure WriteRegister = 6;
      procedure InitialiseRegister = 7;
      procedure InquireRegisters = 8;
      procedure ReadRegisters = 9;
      procedure WriteRegisters = 10;
      procedure InitialiseRegisters = 11;
      } = 1;
   } = 0x2000001;
\end{verbatim}
\end{quote}
 
 
\section{Implementation Recommendations}   %----------------------------
 
\subsection{Crate data structures}
The subset of a \EG\ configuration corresponding to
a single crate can be represented as a further constrained \EG\
configuration.
For example:
\begin{schema}{EuroGamCrate}
   EuroGam
\where
   crates = \{\N{VXI1}\}
\end{schema}
We can arrive at a model for the data structures needed in a particular
\EG\ crate by restricting the $\EG$ sets and functions to the given crate.
When compiling a description file, for example, 
all \nt{cratespec}s not referring to the given crate are simply ignored.
The set $registers$ ends up containing just those registers which ``live''
in the given crate.
 
\subsection{Representing sets and functions}
All the basic objects we need are essentially names or `symbols'. 
This suggests that an implementation should build a symbol table and
use fixed length (e.g. 32 bit) symbol table indexes or pointers to represent
basic objects.
A set of objects can then be represented by a list of such pointers,
and a function $f$ can be represented as a list of pairs of pointers $(x,y)$
such that $f(x)=y$.
Evaluating a function involves first finding the symbol table entry, $x$,
for the argument symbol, scanning the  list of pairs
representing the function for a pair whose first element equals $x$, and
then returning the corresponding $y$.
Finally the pointer $y$ can be used to probe the symbol table for
the result symbol.
Pattern matching a name against some set involves working down the list
of pointers representing the set, probing the symbol table for the
corresponding name and applying the pattern matching procedure.
Since we can expect to be dealing with some tens of thousands of basic
objects the symbol table should be organised as a balanced binary tree 
ordered lexicographically on the symbols. 
Functions and sets can also be represented by balanced binary trees, this
time ordered by the pointer values themselves
(the $x$ pointers in the case of functions).
This organisation is preferable to fixed sized arrays and tables,
being much more flexible and adaptable.
 
\subsection{Generating capabilities}
For this application we need to ensure against accidental rather
than malicious interference between distinct sets of clients.
Expensively encrypted capabilities are therefore waived in favour of
a cheap solution that guards against a client accidentally hitting
upon a valid capability value.
It is important that capability values  recycle slowly (periods of
several days are desirable) and do not recycle as a result of re-booting
crates.
A scheme based on a crate processor's real-time clock is recommended.
 
\subsection{Pattern matching on registers}
We will assume that register names are made from just the upper and lower case
letters, the digits, and the period.
The most useful patterns for this application are a wildcard pattern
which matches zero or more characters and numeric and
character range patterns that match any integer or character in
a sequence of consecutive integers or characters.
\begin{syntax}
  \nt{pattern}   & ::= & \nt{pat}\ldots\nt{pat}  &\omit \\
  \nt{pat}       & ::= & \nt{letter}             &\omit \\
                 &  |  & \T{.}                   &\omit \\
                 &  |  & \nt{digit}              &\omit \\
                 &  |  & \T{*}                   &\omit \\
                 &  |  & \T{[}\nt{range}\T{,}\ldots\T{,}\nt{range}\T{]}&\omit\\
  \nt{range}     & ::= & \nt{integer}            &\omit \\
                 &  |  & \nt{integer}\T{-}\nt{integer}        &\omit \\
                 &  |  & \nt{letter}                   &\omit \\
                 &  |  & \nt{letter}\T{-}\nt{letter}   &\omit \\
  \nt{integer}   & ::= & \nt{digit}\ldots\nt{digit}    &\omit 
\end{syntax}
where \nt{letter} denotes any of the upper and lower case letters and
\nt{digit} any of the digits 0 to 9.
For example, the pattern \T{[5,10-12,a-d,19]} matches any of the set
$\{5,10,11,12,a,b,c,d,19\}$, and the pattern \T{G[1-2].PoleZero} matches
G1.PoleZero and G2.PoleZero.
The wildcard pattern \T{G23.*} matches all names beginning G23. and 
followed by zero or more characters, i.e., all registers related to
array position G23.
 
\subsection{Calibration functions}
Many of the analogue properties of, for example, Ge modules are more
conveniently expressed in ``natural'' units such as microseconds and 
millivolts, rather than the integer representations (0 to 255, say)
necessarily required by the hardware in most cases.
This requires two functions:
\begin{axdef}
   writecalibration: REGISTER \p\fun VALUE \p\fun \num   \\
   readcalibration: REGISTER \p\fun \num \p\fun VALUE
\end{axdef}
which, given a register, return an output and an input calibration
function for that register, respectively.
At this stage of the hardware design it is not yet clear what level
of support for calibrations is required:
\begin{itemize}
\item do we need, for each analogue property, distinct calibrations
for each individual register, or for each module, or will a single fixed
function for all modules suffice?
\item to what extent should it be possible to alter these functions
dynamically?
\end{itemize}
If a single, immutable function (or pair of functions) for each
property is adequate then these can be built into the crate server
program as ``given'' functions.
This is the simplest solution, and devoutly to be desired.
More thought will be required if something more sophisticated is needed.
 
\section{Server Environment}    %----------------------------
 
\subsection{Loading the crate server}
In a production environment the server program must be started 
automatically following a crate power-up or re-boot, whereas 
when a crate is on the maintenance bench it is unlikely to be
of any use (and will probably be an encumbrance). 
Hence we will need to control what programs are loaded at crate
boot-time by means of different boot parameters and scripts---VxWorks
experts please advise.
 
In the case of VXI crates, we anticipate that before the server is started
the slot 0 Resource Manager software will have located all occupied
slots in the crate, identified the modules, performed some minimal
checks (e.g. modules powered up, configuration registers initialised)
and assigned the modules VME
addresses according to the VXI specification. 
The RM must provide the server (and other programs) with a ``crate map''
defining module type, serial number, and VME base address of each 
occupied slot. 
The server can check module types and serial numbers  against the
declarations in the configuration file.
The VME addresses provide the server with the $basedat$ function.
The RM software can  either  build a suitable globally accessible
data structure or export an inquiry function.
In the case of non-VXI crates, this information must be fixed by
convention (undesirable) or obtained from the configuration description
file.
 
\subsection{Diagnostic procedures}
This specification makes no mention of diagnostics for
modules since we regard this as outside the scope of the crate server program.
This is currently a topic under discussion but we anticipate that 
diagnostics will fall into three classes:
\begin{description}
\item [online] This class represents tests that can be set up by experimenters
by manipulating on-board registers using the facilities of the 
crate server.
These tests would be resorted to first should a problem be suspected
while preparing for or running an experiment.
They range from simple data integrity tests of individual registers
to (possibly) using the Ge card on-board pulse generator to produce
a singles histogram.
The latter test (if feasible) would exercise readout controller, DT32 bus, and
histogrammer functions.
At this stage of the design we do not anticipate incorporating extra functions
in the crate server to support diagnostic tests.
For example, we would exclude anything which required the crate server
to field interrupts from modules, this being a job for the next class
of diagnostics.
\item [standalone] This class of test can be met by running special
purpose diagnostic programs in the crate under suspicion.
This would require a remote login to the crate and some familiarity
with the VxWorks shell in order to load and execute the programs.
Such tests could involve only modules within the crate and could not
assume any of the functionality of the production data acquisition 
software.
In practice, it may be necessary to displace the standard crate server
program before running such a diagnostic
and such programs must rely on the crate map built by the Resource Manager
at boot-time to identify modules.
Tests in this class are candidates for running automatically 
at boot-time as confidence tests before invoking the crate server
program.
If written to a local file the results of such confidence tests could
be returned by an inquiry function supported by the crate server, 
analogous to the $ReadEuroGamLog$ operation.
 
\item [maintenance] Finally we have a class of diagnostic appropriate 
to the maintenance bench---cards on extenders, special test harnesses,
etc., which we will gratefully abandon to the design/commissioning
engineers.
\end{description}
 
\subsection{Server network port}
The server will always listen on a fixed UDP port number to be determined.
 
\subsection{Error recovery}
Lack of familiarity with the facilities offered by VxWorks prevents
us from recommending a specific fatal error recovery mechanism at
present.
Possibilities which should be investigated include:
\begin{itemize}
\item watchdog timers
\item remote boot facility
\end{itemize}
VxWorks experts please advise.
 
\subsection{Scope channels}
At this stage of the design it is not clear how the ``scope channel''
feature of the slot 0 card will work and how it might be used in
production.
However, we can envisage a set of registers on the card which control
the scope function and can be accessed via the crate server.
What to do with the data which is produced is an open problem.
One possibility is to have a client program polling the crate for
the scope data.
Another is to provide a pseudo register containing a network address
to which the crate calls back and transmits the data. 
 
\subsection{Configuration description file}
We have shown the configuration description file as an input parameter
to the $ConfigureEuroGam$ schema.
In practice, a client program  passes the crate server a file name and
the server accesses the file by means of the NFS capability of VxWorks.
We expect the description file(s) to reside on some file server system
where they are maintained by support staff using ordinary text editors.
Temporary  changes during an experiment---needed to 
configure around a hardware fault, for example---are accommodated
by modifying a copy of the basic description file.
Copies of description files can be taken away to aid post-experiment
analysis if need be.
 
\section{Client Programming Issues}       %----------------------------
 
\subsection{Addressing crates}
Client programs must learn the network addresses of crates 
comprising a \EG\ configuration by reading the appropriate
configuration description file, but in general they will not
know which crate supports a particular abstract register (though
there are exceptions).
Solutions to this problem include:
\begin{itemize}
\item RPC to all crates (preferably in parallel)---at most one
will respond affirmatively.
This is the only practical solution in the case of the pattern-matching
functions.
\item Build a register location map by polling the crates with
$InquireRegisters$ functions.
This may be a viable solution for certain long-running clients.
\item Compile the configuration description file---i.e., emulate
the crate servers themselves.
This is not recommended.
\end{itemize}
 
\subsection{RPC library}
Further work needs to be done in defining a package of routines that 
generate the above XDR bindings for linking with client programs.
This needs to take into account the issues raised in the preceeding
paragraph.
 
\subsection{Deadlock avoidance}
A classic deadlock can occur if client programs are careless of
the order in which they claim crates.
This possibility can be avoided if clients only acquire crates in the
order in which they appear in the configuration description file.
If a client fails to acquire one of the crates comprising a \EG\ configuration
it should release any it has succeeded in claiming.
 
\subsection{Detector database}
Experimenters have registered some interest in establishing some sort
of ``detector database.''
Such a database would be held on a file server system and maintained
by the local detector support staff.
In particular, users envisage setting up the LeCroy High Voltage
supplies by reference to ``preferred bias'' information held per
detector in such a database.
This can be realised by means of a client program that interrogates
the detector database for the appropriate voltage and invokes the
$WriteRegister$ function specifying a register name of the form
$detector${\tt.Bias}---the register access mechanism in the 
appropriate crate server does the rest.
The contents and format of such a database are outside the scope of this
document.
No further applications of a detector database which impact the
crate server software have been suggested.
 
In similar vein, the idea of an ``array database'' containing, 
for example, details of the array geometry has been mooted.
Again, this topic is outside the scope of the crate server software.
 
\begin{thebibliography}{99}
\bibitem{EGSS}{\em Eurogam Project: System Specification}, Pucknell et al,
Edition 1.0, May 1990.
\bibitem{Spivey}{\em The Z Notation---A Reference Manual}, J.M.Spivey, 
ISBN~0--13--983768--X
\bibitem{NP}{\em Network Programming}, Sun Microsystems,
part number~ 800--1779--10, May 1988.
\bibitem{CD}{\em Distributed Systems---Concepts and Design}, Coulouris and
Dollimore, ISBN~0--201--18059--6
\end{thebibliography}
\end{document}