\documentstyle[zed,11pt,a4wide]{article}
\newcommand{\within}{\mathrel{\rm within}}
\newcommand{\precedes}{\mathrel{\rm precedes}}
\newcommand{\ordered}{\mathord{\rm ordered}}
\newcommand{\memfree}{\mathord{\rm memfree}}
\newcommand{\bitor}{\mathop{\rm bitor}}
\def \iseq	{\mathop{\rm iseq}}             % copied from fuzz.sty
\def\aside#1{\noindent {\it[#1]}\par}
\def\EG{EuroGam}
\def\signed#1#2{{\unskip\nobreak\hfil\penalty50
  \hskip2em\hbox{}\nobreak\hfil#1\quad#2
  \parfillskip=0pt \finalhyphendemerits=0 \par}}       % TeXBook, p106

\title{Eurogam Spectrum Servers\\Online Histogrammer}
\author{David Brightly}
\date{Edition 0.9\\December 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 on A4 paper
\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
EDOC060\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 Spectrum Servers:\\
Online Histogrammer\par
\vskip 20pt
\hrule height 2pt
\vskip 1in
\medium
Edition 0.9\par
\vskip 5pt
December 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 [As usual this document is not yet complete but is
published in its present form for comments.
More work needs to be done in defining  functions for returning
some form of compressed histogram data and for obtaining cuts and
slices from histograms of dimension $>1$.
XDR bindings for all the procedures also need to be worked out.
Author's remarks and asides are in square brackets.
\signed{D.B.}{Monday 10 December 1990]}


\section{Introduction}
This document is in two parts: 
the first part specifies the properties of spectra in general and defines
generic  operations on them;
the second part describes the \EG\ online histogrammer hardware and shows
how the operations defined in the first part can be mapped onto it.
Further documents in this series will describe similar specialisations
for online sorter spectra and saved disc spectra.


\section{Generic spectra}

\subsection{Shapes, tuples, and domains}
This section will describe the foundations which we will need to talk about 
histograms and spectra.

\begin{zed}
SHAPE == \seq_1 (\num \cross \num)  \\
TUPLE == \seq_1 \num  \\
DOMAIN == \power TUPLE 
\end{zed}
Histograms are essentially arrays of a certain {\sl shape\/}.
For example, a simple one dimensional histogram might have a shape given by 
$\langle (0,1024) \rangle$. 
This means it starts with channel $0$ and has $1024$ channels.
A two dimensional histogram with 64 channels in the first dimension and 4096 
in the second could have the shape $\langle (1,64),(0,4096) \rangle$.
In this example the channels in the first dimension are numbered $1$ to $64$.
A {\sl tuple\/} is a sequence of numbers labelling a channel in  a histogram.
The tuple $\langle 23 \rangle$ labels channel 23 of our first histogram
and the tuple $\langle 44, 2753 \rangle$ labels a channel in our two 
dimensional example.
A {\sl domain\/} is just a set of tuples. 
We will use domains to talk about subsets of all the channels in a histogram.
Both tuples and shapes have a {\sl dimension\/} defined in the obvious way:
\begin{axdef}
dimension : TUPLE \fun \nat_1  \\
shapedimension : SHAPE \fun \nat_1
\where
\forall t:TUPLE @ dimension (t) = \# t  \\
\forall s:SHAPE @ shapedimension (s) = \# s
\end{axdef}
We can count the total number of channels in a histogram of a certain shape.
Our first example has $1024$ channels and the second has $64*4096$ channels:
\begin{axdef}
size : SHAPE \fun \num
\where
\forall a,b : \num; s: SHAPE @ \\
\t1 size~\langle (a,b) \rangle = b \land  \\
\t1 size (s)  = size (\langle head~s \rangle) * size (tail~s)
\end{axdef}%
%%inrel \precedes
When reading or writing counts in channels we need to present them in some
fixed order.
In this ordering, the rightmost channel coordinate varies fastest, so we have
$\langle 100\rangle \precedes \langle 200 \rangle$ 
and $\langle 23, 3192 \rangle \precedes
\langle 44 , 1024 \rangle$.
\begin{axdef}
\_ \precedes \_ : TUPLE \rel TUPLE
\where
\forall a,b:\num; x,y:TUPLE | \#x = \#y @  \\
\t1 (\langle a \rangle \precedes \langle b \rangle \iff a < b) \land   \\
\t1 (x \precedes y \iff  (head~x < head~y
    \lor (head~x = head~y \land tail~x \precedes tail~y)))
\end{axdef}
%%prerel \ordered
We can say whether a given sequence of tuples is ordered or not:
\begin{axdef}
\ordered \_ : \power (\seq TUPLE)
\where
\forall s: \seq TUPLE @  \\
\t1 \ordered~s \iff (\forall i,j:\dom s @ (i < j) \iff s~i \precedes s~j)
\end{axdef}
and given a set of tuples we can order them:
\begin{axdef}
order : DOMAIN \fun \seq TUPLE
\where
\forall d:DOMAIN; s: \seq TUPLE @  \\
\t1 s = order (d) \iff \ran s = d \land \ordered~s
\end{axdef}
%%inrel \within
We can also say whether a given tuple lies within  a given shape.
For example, we have
$\langle 11, 999 \rangle \within  \langle (1,64), (0,4096) \rangle$ but
not $\langle 2048\rangle \within \langle (0,1024) \rangle$.
\begin{axdef}
\_ \within \_ : TUPLE \rel SHAPE
\where
\forall x,a,b:\num; t:TUPLE; s:SHAPE @  \\
\t1 (\langle x\rangle \within \langle(a,b)\rangle \iff 0 \leq x-a <b) \land \\
\t1 (t \within s \iff \langle head~t \rangle \within \langle head~s \rangle 
\land tail~t \within tail~s)
\end{axdef}
Given a shape we can now return the domain consisting of all the channels
that lie within that shape:
\begin{axdef}
rectdomain : SHAPE \fun DOMAIN
\where
\forall s:SHAPE @
rectdomain (s) = \{d: TUPLE | d \within s \}
\end{axdef}
Finally, if all the channels within a shape are ordered in this way 
we can calculate the offset of a given channel from the beginning of the
sequence.
\begin{axdef}
offset : TUPLE \cross SHAPE \fun \num
\where
\forall s:SHAPE; x,a,b:\num; t: TUPLE @ \\
\t1 offset (\langle x\rangle, \langle (a,b) \rangle) = x-a \land  \\
\t1 offset (t,s) = 
        offset (\langle head~t \rangle, \langle head~s \rangle) * size(tail~s)
      + offset(tail~t,tail~s)
\end{axdef}
For example, we have 
\[offset (\langle 23 \rangle, \langle (0, 1024)\rangle) = 23\] and
\[offset (\langle 11,999\rangle,\langle (1,64),(0,4096)\rangle)=10*4096+999.\]
The following relationships can be proved (by induction on the dimension
of the shape $s$):
\begin{argue}
\forall x,y:TUPLE; s:SHAPE | x \within s \land y \within s @  \\
\t1 0 \leq offset (x,s) < size~s  \land  \\
\t1 x \precedes y \iff offset (x,s) < offset (y,s)  \land  \\
\t1 order (rectdomain~s) (offset (x,s)+1) = x
\end{argue}
The last relation just says that the $offset$ function assigns to a tuple $x$
the ordinal number of its position in the ordered domain based on the shape 
$s$ (less one because sequences in Z start at one not zero, unfortunately).


\subsection{Histograms and Spectra}
We can now introduce histograms and spectra as data types.
A histogram consists of a function from some set of tuples, i.e., channels,
into the integers. 
This function is defined on all the channels within some shape.
It is also useful to hold with each histogram some indication of its
least and greatest count.
For example, 
an interactive spectrum display program can determine how to scale the
counts for display without first having to read them all.
However, we don't insist that the values always tell the truth---this
would be difficult to achieve within a hardware histogramming system,
for instance.
\begin{schema}{Histogram}
shape : SHAPE  \\
counts : TUPLE \pfun \num \\
mincount : \num  \\
maxcount : \num 
\where
\dom counts = rectdomain~shape
\end{schema}
A spectrum consists not only of counts but also of {\sl calibrations\/} 
and {\sl annotations\/}.
We don't need to specify at this stage what they look like---in fact they
will be opaque strings of characters associated with spectra---so we will
treat them for the time being as a given data type.
But we will need a reserved value from this type to denote the empty string, 
i.e., an undefined calibration or annotation.
We will also need to distinguish between histograms of different
{\sl precision\/}, i.e., the number of bits required to represent the
counts.
\aside{need to think out the semantics of precision further}

\begin{zed}
[STRING]  \\
PRECISION ::= bit16 | bit32
\end{zed}
\begin{axdef}
maxannotations  : \nat  \\
maxhistograms : \nat  \\
maxcalibrations : \nat  \\
NULL : STRING
\where
maxannotations = 16  \\
maxcalibrations = 16  \\
maxhistograms = 16
\end{axdef}
A spectrum is specified as follows:

\begin{schema}{Spectrum}
precision : PRECISION  \\
sshape : SHAPE  \\
arrays : 1 \upto maxhistograms \pfun Histogram  \\
calibrations : 1 \upto maxcalibrations \pfun STRING  \\
annotations : 1 \upto maxannotations \pfun STRING
\where
\forall i: \dom arrays @ (arrays~i) . shape = sshape  \\
\dom calibrations \subseteq 1 \upto shapedimension~sshape  \\
\end{schema}
A spectrum thus consists of zero or more histograms, calibrations,
annotations, all identified by small integers.
These will all have some conventional use---for example, the first
histogram would contain the principal counts of the spectrum and the
second (if it existed) might contain an ``error'' histogram if the
principal counts had been obtained (say) by some background
subtraction operation.
Similarly the first annotation might by convention be a descriptive
title for the spectrum included by application programs in formatted
output, and so on.
All we require at the moment is to establish an upper limit on the numbers
of such objects making up a spectrum, as this will guide implementation
decisions.
Note, however, that the histograms must all have a common shape, 
and each calibration (if it exists) is associated with a specific dimension.

We will need a data type for returning information about a spectrum:
\begin{schema}{Attributes}
s : SHAPE  \\
p : PRECISION
\end{schema}

\subsection{Spectrum store}
Users will want to reference spectra using meaningful names.
We can envisage at least three sources of spectra: online histogramming,
online EbyE sorting, and saved spectra on disc.
Each spectrum server manages a ``spectrum store'', i.e., a directory structure
which maps names to spectra.
In the case of online histogramming and sorting the store need offer no more
than a single level naming scheme, but in the case of saved spectra on disc
the store can be identified with (part of) the host system filestore and
will typically offer a multi-level directory structure.
Both online and saved spectrum directories can be integrated by adopting
a naming convention which reserves specific directory names for
histogrammers and sorters and which enables client programs to identify
which server supports a spectrum of any given name:
%%unchecked
\begin{syntax}
name & ::= & {\tt /histogrammer} n {\tt /} simplename \\
     &  |  & {\tt /sorter} n {\tt /} simplename \\
     &  |  & {\tt/} simplename {\tt /} \ldots {\tt /} simplename \\
simplename & ::= & {\rm any\ printable\ name\ without\ {\tt /}\ or\ blank}  \\
 n   & ::= & integer
\end{syntax}
\aside{in a multiple front end system should there be a leading
{\tt /eg1}, say, to identify the frontend, or should this be information
in the client context?}
However, for our current purposes we need not be too specific about
directories and stores and will just assume the following types:

\begin{zed}
[NAME, SIMPLENAME]  \\
DIRECTORY == SIMPLENAME \pfun Spectrum  \\
STORE == NAME \pfun Spectrum
\end{zed}
Each spectrum server will operate a single store of spectra and
in the case of online spectrum servers this will consist of a 
single directory.

\begin{schema}{SpectrumStore}
store : STORE  \\
\end{schema}
Given a directory within the store we must be able to obtain a list 
of the spectra within it (analogous to the unix {\tt ls} command):

\begin{schema}{ReadDirectory}
dir? : DIRECTORY \\
nn! : \iseq SIMPLENAME
\where
\ran nn! = \dom dir?
\end{schema}
and also a list of spectra together with their attributes 
(analogous to {\tt ls -l}):

\begin{schema}{ReadDirectoryWithAttributes}
dir? : DIRECTORY  \\
nana! : \iseq (SIMPLENAME \cross Attributes)
\where
\forall n:SIMPLENAME; s:Spectrum; a:Attributes @  \\
   (n,a) \in \ran nana! \iff s = dir? (n) \land a.s=s.sshape \land
a.p = s.precision
\end{schema}


\subsection{Generic operations on spectra}
This section will outline the operations that all spectrum servers
have to support. 
Later on we will specialise these operations for the \EG\ histogrammer.

\begin{schema}{CreateSpectrum}
\Delta SpectrumStore  \\
spectrum : Spectrum  \\
name? : NAME  \\
s? : SHAPE  \\
p? : PRECISION  \\
h : Histogram 
\where
name? \notin \dom store  \\
spectrum.precision = p?  \\
spectrum.sshape = s? \\
spectrum.calibrations = \empty \\
spectrum.annotations = \empty  \\
spectrum.arrays = \{ 1 \mapsto h \}  \\
h.shape = s?  \\
\ran h.counts = \{ 0 \} \\
h.mincount = h.maxcount = 0  \\
store' = store \oplus \{ name? \mapsto spectrum \}
\end{schema}

\begin{schema}{DeleteSpectrum}
\Delta SpectrumStore  \\
name? : NAME 
\where
name? \in \dom store  \\
store' = \{ name? \} \ndres store
\end{schema}
Note that a brand new spectrum comes with an already zeroed first
histogram. 
This is convenient for client programs of the online spectrum servers,
but in the case of large disc spectra it is probably desirable to
optimise out the writing of many zero channels---this happens
automatically with the unix file system, for example.

The following two schemas provide  convenient abbreviations to be
used in specifying operations on spectra: the first is used in
``read-only'' operations and the second in those that alter the
contents of the spectrum store.

\begin{schema}{AccessSpectrum}
\Xi SpectrumStore  \\
n? : NAME \\
s : Spectrum 
\where
n? \in \dom store  \\
s = store~n?
\end{schema}

\begin{schema}{ModifySpectrum}
\Delta SpectrumStore  \\
n? : NAME  \\
s,s' : Spectrum  
\where
n? \in \dom store  \\
s = store~n?  \\
s'.sshape = s.sshape  \\
store' = store \oplus \{ n? \mapsto s' \}
\end{schema}

The following operation returns the attributes of a spectrum---its
shape and precision:
\begin{schema}{InquireAttributes}
AccessSpectrum  \\
n? : NAME  \\
a! : Attributes
\where
a!.s = s.sshape \land a!.p = s.precision
\end{schema}

We can now give schemas describing the operations of reading and writing
the component parts of a spectrum.

\begin{schema}{ReadHistogram}
\Xi SpectrumStore  \\
AccessSpectrum \\
i? : \nat \\
s? : SHAPE  \\
h : Histogram  \\
z! : \seq \num
\where
i? \in \dom s.arrays  \\
h = s.arrays~i?  \\
rectdomain~s? \subseteq rectdomain~h.shape  \\
z! =  h.counts \circ (order ( rectdomain~s?))
\end{schema}

\begin{schema}{WriteHistogram}
\Delta SpectrumStore  \\
ModifySpectrum  \\
i? : \nat  \\
s?: SHAPE  \\
z? : \seq \num  \\
h,h': Histogram 
\where
i? \in \dom s.arrays  \\
h = s.arrays~i?  \\
rectdomain~s? \subseteq rectdomain~h.shape  \\
h'.counts = h.counts \oplus 
   \{ j:\dom z? @  order (rectdomain~s?) j  \mapsto z?~j \}   \\
h'.shape = h.shape  \\
s'.arrays = s.arrays \oplus \{ i? \mapsto h' \}  \\
s'.annotations = s.annotations  \\
s'.calibrations = s.calibrations
\end{schema}

\begin{schema}{ZeroHistogram}
\Delta SpectrumStore  \\
ModifySpectrum  \\
i? : \nat  \\
s? : SHAPE  \\
h,h': Histogram
\where
i? \in \dom s.arrays  \\
rectdomain~s? \subseteq rectdomain~h.shape  \\
h'.counts = h.counts \oplus  \{ t:rectdomain~s? @ t \mapsto 0 \}   \\
h'.shape = h.shape  \\
h'.mincount = h'.maxcount = 0  \\
s'.arrays = s.arrays \oplus \{ i? \mapsto h' \}  \\
s'.annotations = s.annotations  \\
s'.calibrations = s.calibrations
\end{schema}

\begin{schema}{ReadExtrema}
\Xi SpectrumStore  \\
AccessSpectrum \\
i? : \nat \\
h : Histogram  \\
min!, max! : \num
\where
i? \in \dom s.arrays  \\
h = s.arrays~i?  \\
min! = h.mincount \\
max! = h.maxcount 
\end{schema}

\begin{schema}{WriteExtrema}
\Delta SpectrumStore  \\
ModifySpectrum  \\
i? : \nat  \\
min?, max? : \num  \\
h,h': Histogram 
\where
i? \in \dom s.arrays  \\
h'.shape = h.shape  \\
h'.counts = h.counts  \\
h'.mincount = min?  \\
h'.maxcount = max?  \\
s'.arrays = s.arrays \oplus \{ i? \mapsto h' \}  \\
s'.annotations = s.annotations  \\
s'.calibrations = s.calibrations
\end{schema}

\begin{schema}{ReadCalibration}
\Xi SpectrumStore  \\
AccessSpectrum  \\
c! : STRING  \\
i? : \nat
\where
i? \in \dom s.calibrations  \\
c! = s.calibrations~i?
\end{schema}

\begin{schema}{WriteCalibration}
\Delta SpectrumStore  \\
ModifySpectrum  \\
c? : STRING  \\
i? : \nat
\where
i? \in \dom s.calibrations  \\
s'.sshape = s.sshape  \\
s'.arrays = s.arrays  \\
s'.annotations = s.annotations  \\
s'.calibrations = s.calibrations \oplus \{ i? \mapsto c? \}
\end{schema}

\begin{schema}{ReadAnnotation}
\Xi SpectrumStore  \\
AccessSpectrum  \\
a! : STRING  \\
i? : \nat
\where
i? \in 1 \upto maxannotations  \\
a! = s.annotations~i?
\end{schema}

\begin{schema}{WriteAnnotation}
\Delta SpectrumStore  \\
ModifySpectrum  \\
a? : STRING  \\
i? : \nat
\where
i? \in 1 \upto maxannotations  \\
s'.sshape = s.sshape  \\
s'.arrays = s.arrays  \\
s'.annotations = s.annotations \oplus \{ i? \mapsto a? \}  \\
s'.calibrations = s.calibrations 
\end{schema}

\section{EuroGam online histogrammer}
\subsection{Histogrammer memory}
The previous sections have described spectra in general.
We now come to specific properties of the \EG\ online histogrammer.
Let us assume that the histogramming memory occupies a contiguous
block of 32 bit words in the VME address space between word address
$RMbase$ and $RMbase+RMrange-1$ inclusive.
It turns out to be easier to model the memory as a sequence of words
rather than bytes, so all our ``addresses'' have to be multiplied by
four to get actual VME addresses.
\begin{axdef}
VMElimit : \nat  \\
RMbase : \nat  \\
RMrange : \nat 
\where
VMElimit = 1024*1024*1024  \\
0 \leq RMbase \land RMbase+RMrange \leq VMElimit
\end{axdef}
We can model the actual histogramming memory with a function which
returns the contents of a memory word, given its address.

\begin{schema}{RealMemory}
memory : \nat \fun \num
\where
\dom memory = RMbase \upto RMbase+RMrange-1
\end{schema}
All our histograms will occupy real memory so we need a way of managing
the space.
We will do this with a pair of functions which record the base address
(relative to $RMbase$) and number of words occupied of each histogram.
%%prerel \memfree
\begin{schema}{HistogramMemory}
membase : Histogram \pfun \num  \\
memrange : Histogram \pfun \num  \\
memused : Histogram \pfun \power \num  \\
\memfree \_ : \power (\num \cross \num) 
\where
\dom membase = \dom memrange  
\also
\forall h: Histogram @  \\
\t1 h \notin \dom membase \implies memused (h) = \empty  \land  \\
\t1 h \in \dom membase \implies memused (h) = membase (h) \upto membase (h) +
   memrange (h) - 1 
\also
\forall m,r:\num @  \\
\t1 \memfree (m,r) \iff (\forall h: \dom membase @  \\
\t2 (m \upto m+r-1) \cap memused~h = \empty) \land 0 \leq m < m+r \leq RMrange
\end{schema}
To simplify discussion of memory management $memused$ returns the
set of memory addresses occupied by a histogram, and $\memfree(m,r)$ tells
us whether there is a block of $r$ unused words starting at address $m$.


\subsection{Histogrammer card}
In this section we describe the \EG\ histogrammer card as outlined
in \cite{JRA}.
We need to talk about enabling and disabling aspects of the card's
function:
\begin{zed}
STATE ::= enabled | disabled
\end{zed}
We need to refer to the data acquisition channel ``addresses'' which
label conversions received by the histogrammer.
We will call these {\sl tags\/} in order to distinguish them from
histogramming memory addresses.
\begin{zed}
[TAG]
\end{zed}
We can now describe the histogrammer card itself:
\begin{schema}{HistogrammerCard}
state : STATE  \\
tagstate : TAG \fun STATE  \\
tagbase : TAG \pfun \num  \\
baseaddress : \nat
\end{schema}
We have an overall $state$ which determines whether words are
histogrammed or not and
a function $tagstate$ which tells us whether a given tag is to be 
histogrammed or not.
Note that $tagstate$ is a total function---it must be defined
for all possible tags.
The function $tagbase$ and the constant $baseaddress$ determine (indirectly)
the base address in memory of the histogram generated by each tag, 
These objects directly model the hardware features described in \cite{JRA}.
In particular, $tagstate$ and $tagbase$ correspond to the histogrammer's
``look-up table''.

The histogrammer card generates addresses to be incremented by shifting
and ``or''-ing.
If we use the infix function $\_\bitor\_$ to denote bitwise ``or''
on two's complement integers
%%inop \bitor 4
%%\begin{axdef}
%%\_ \bitor \_ : \nat \cross \nat \fun \nat
%%\end{axdef}
we can specify the operation of the histogrammer card when 
presented with a tag $t?$ and a data word $d?$ \cite[section 3.3]{JRA}.
\begin{schema}{Increment}
\Xi HistogrammerCard  \\
\Delta RealMemory   \\
t? : TAG  \\
d? : \nat
\where
state = enabled \land tagstate~t? = enabled \iff  \\
\t1 (\exists a:\nat @ \\
\t2   a = baseaddress \bitor (tagbase~t? * 1024) \bitor d?  \land  \\
\t2   memory' = memory \oplus \{ a \mapsto memory(a)+1 \})
\end{schema}

\subsection{Putting it all together}
We can now combine the definitions in the preceding sections to
specify the state space of the whole histogrammer hardware/software
combination:
 
\begin{schema}{Histogrammer}
HistogrammerCard  \\
HistogramMemory  \\
RealMemory  \\
address : Histogram \cross TUPLE \fun \num  \\
SpectrumStore
\where
\forall t: TAG @ tagstate~t = enabled \implies \\
\t1 (\exists h:Histogram @ membase~h = tagbase~t * 1024)
\also
\forall s: \ran store @ shapedimension~s.sshape = 1 \land 
   first (head~s.sshape) = 0
\also
\forall h: \dom membase; t:TUPLE | t \within h.shape @ \\
\t1 address (h,t) = RMbase + membase(h) + offset (t,h.shape) \land \\
\t1 h.counts (t) = memory (address (h,t))
\end{schema}
Note the constraints in the $Histogrammer$ schema:
firstly, every enabled entry in the look-up table must point to
a piece of memory associated with a histogram \cite[section 3.6]{JRA};
secondly, all spectra are one dimensional and start in channel zero;
thirdly, the function $address (h,t)$ gives the address in histogramming
memory of the channel $t$ of histogram $h$;
finally, we {\em identify\/} the count in channel $t$ of histogram $h$
with the contents of memory location $address(h,t)$.

Note also the implications of the histogrammer's use of $\bitor$ rather
than addition.
When presented with tag $t$ and data $d$ the histogrammer increments
memory address 
\[baseaddress \bitor (tagbase~t * 1024) \bitor d.\]
We want this to be $address (h,c)$ where $h$ is the histogram
corresponding to tag $t$ and $c=d$.
Since all our histograms are one dimensional and start in channel zero 
this is just the address
\[RMbase + membase(h) + c. \]
To ensure that $\bitor$ gives the same result as addition we can insist
that
\[\exists n @ \forall h @ RMbase \mod 2^n = 0 \land 2^n > membase(h)+c\]
and that,
\[\forall h @ \exists m @ membase (h) \mod 2^m = 0 \land 2^m > c.\]
These conditions are readily met by demanding that all histograms 
have power of two size and be aligned on their size
and that  $RMrange$ also be a power of two with
$RMbase \mod RMrange = 0$.

\begin{axdef}
validranges : \power \nat
\where 
validranges = \{1024,2048,4096,8192\}  \\
RMbase \mod RMrange = 0
\end{axdef}


\aside{Finally, note that $d=c$ and $c \within h.shape$ 
implies $d \within h.shape$
also. 
If the data presented to the histogrammer does not meet this condition,
e.g., through some external hardware or programming fault, then
spurious counts may appear in some spectra.
It may be worthwhile widening the histogrammer's lookup table 
with per-tag mask fields to prevent this}

 
The next schema describes how the histogrammer system starts---basically
nothing is known and all tags are disabled, but overall operation
of the card is enabled.
This avoids the need for explicit ``halt'' and ``go'' operations
on the histogrammer hardware.
It is not essential to zero the real memory at this point, though
clearly some sort of memory self-test is desirable. 
\begin{schema}{InitHistogrammer}
Histogrammer
\where
state = enabled  \\
\forall t:TAG @ tagstate ~t = disabled  \\
membase = \empty  \\
memrange = \empty  \\
baseaddress = RMbase \\
store = \empty 
\end{schema}

In the foregoing we have tried to keep separate operations on abstract
histograms from hardware descriptions.
We now have to say how a histogram gets associated with a particular tag.
First we reserve space for a histogram in the memory and then we {\sl map\/}
a certain tag onto that histogram.

\begin{schema}{MapTag}
\Delta HistogrammerCard  \\
\Xi HistogramMemory  \\
h? : Histogram  \\
t? : TAG 
\where
state = disabled = state'  \\
tagstate~t? =  disabled  \\
tagstate' = tagstate \oplus \{ t? \mapsto enabled \}  \\
tagbase' = tagbase \oplus \{ t? \mapsto membase~h? \div 1024 \}  \\
baseaddress' = baseaddress
\end{schema}
When we no longer require a histogram we must unmap the associated
tag (if any) before we can free the memory belonging to the
histogram.

\begin{schema}{UnMapTag}
\Delta HistogrammerCard  \\
\Xi HistogramMemory  \\
t? : TAG 
\where
state = disabled = state'  \\
tagstate~t? = enabled  \\
tagstate' = tagstate \oplus \{ t? \mapsto disabled \}  \\
tagbase' = \{t?\} \ndres tagbase \\
baseaddress' = baseaddress
\end{schema}
Both these operations require that the histogrammer hardware be
in the disabled state, so let us give ourselves operations
for enabling and disabling the histogrammer card.

\begin{schema}{Go}
\Delta HistogrammerCard  \\
\Xi HistogramMemory
\where
state = enabled
\end{schema}

\begin{schema}{Stop}
\Delta HistogrammerCard \\
\Xi HistogramMemory
\where
state' = disabled
\end{schema}
We can now promote these operations to the spectrum level:

\begin{zed}
StopMapTagGo \defs Stop \semi MapTag \semi Go  \\
StopUnMapTagGo \defs Stop \semi UnMapTag \semi Go
\end{zed}

\begin{schema}{AssociateTag}
AccessSpectrum  \\
StopMapTagGo  \\
i? : \nat
\where
h?=s.arrays~i?
\end{schema}

\begin{schema}{DissociateTag}
AccessSpectrum  \\
StopUnMapTagGo  \\
i? : \nat  \\
h : Histogram
\where
h = s.arrays~i?  \\
t? = (\mu t:TAG | tagbase~t * 1024 = membase~h)
\end{schema}



We can now completely define the operations of creating a new
histogrammer spectrum and of deleting one:
\begin{schema}{CreateHistogrammerSpectrum}
\Delta Histogrammer  \\
\Xi HistogrammerCard  \\
CreateSpectrum  \\
m,r : \num  
\where
shapedimension~spectrum.sshape = 1 \land first (head~spectrum.sshape) = 0  \\
r = size~s? \land r \in validranges  \\
m \mod r = 0 \\
\memfree (m,r)  
\also
membase' = membase \oplus \{ h \mapsto m \}  \\
memrange' = memrange \oplus \{ h \mapsto r \} 
\end{schema}

\begin{schema}{DeleteHistogrammerSpectrum}
\Delta Histogrammer  \\
t? : TAG  \\
DeleteSpectrum  \\
h : Histogram
\where
h = (store~name?).arrays~1 \\
(\exists t?:TAG | tagbase~t? * 1024 = membase~h @ StopUnMapTagGo) \lor  \\
(\lnot (\exists t?:TAG | tagbase~t? * 1024 = membase~h @ \Xi HistogrammerCard))\\
membase' = \{ h \} \ndres membase  \\
memrange = \{ h \} \ndres memrange
\end{schema}

\subsection{Error conditions}

\begin{syntax}
REPORT & ::=  & ok  \\
       & |    & domain\_outside\_spectrum  \\
       & |    & invalid\_calibration\_number \\
       & |    & invalid\_annotation\_number  \\
       & |    & invalid\_histogram\_number  \\
       & |    & counts\_dont\_fill\_shape  \\
       & |    & spectrum\_not\_known  \\
       & |    & spectrum\_already\_exists  \\
       & |    & shape\_unsuitable\_for\_histogrammer  \\
       & |    & insufficient\_histogramming\_memory  \\
       & |    & tag\_already\_being\_histogrammed  \\
       & |    & histogram\_not\_associated\_with\_tag 
\end{syntax}

\begin{schema}{Ok}
r! : REPORT
\where
r! = ok
\end{schema}

\begin{schema}{BadShape}
r! : REPORT  \\
s?:SHAPE  \\
h: Histogram
\where
\lnot rectdomain~s? \subseteq rectdomain~h.shape  \\
r! = domain\_outside\_spectrum
\end{schema}

\begin{schema}{BadCalibration}
r! : REPORT  \\
s: Spectrum  \\
i?: \nat
\where
\lnot i? \in 1 \upto shapedimension~s.sshape  \\
r! = invalid\_calibration\_number
\end{schema}

\begin{schema}{BadAnnotation}
r! : REPORT  \\
i?: \nat
\where
\lnot i? \in 1 \upto maxannotations  \\
r! = invalid\_annotation\_number
\end{schema}

\begin{schema}{BadCounts}
r! : REPORT  \\
i?: \nat  \\
s? : SHAPE  \\
z? : \seq \num
\where
\# z? \neq size~s?  \\
r! = counts\_dont\_fill\_shape
\end{schema}

\begin{schema}{BadHistogram}
r! : REPORT  \\
i?: \nat  \\
s : Spectrum
\where
\lnot i? \in \dom s.arrays  \\
r! = invalid\_annotation\_number
\end{schema}

\begin{schema}{UnknownSpectrum}
\Xi Histogrammer \\
r! : REPORT  \\
n? : NAME
\where
\lnot n? \in \dom store  \\
r! = spectrum\_not\_known
\end{schema}

\begin{schema}{AlreadyExists}
\Xi Histogrammer \\
r! : REPORT  \\
n?: NAME
\where
n? \in \dom store  \\
r! = spectrum\_already\_exists
\end{schema}

\begin{schema}{UnsuitableShape}
s? : SHAPE  \\
r! : REPORT
\where
\lnot (shapedimension~s? = 1 \land first (head~s?) = 0 \land
   second (head~s?) \in validranges)  \\
r! = shape\_unsuitable\_for\_histogrammer
\end{schema}

\begin{schema}{NoMemory}
\Xi Histogrammer  \\
s? : SHAPE  \\
r! : REPORT
\where
\lnot (\exists m,r: \nat @ r = size~s? \land m \mod r = 0 \land
   \memfree (m,r))  \\
r! = insufficient\_histogramming\_memory
\end{schema}

\begin{schema}{TagInUse}
\Xi HistogrammerCard  \\
t? : TAG  \\
r! : REPORT
\where
tagstate~t? = enabled  \\
r! = tag\_already\_being\_histogrammed
\end{schema}

\begin{schema}{NotAssociated}
\Xi HistogrammerCard  \\
\Xi HistogramMemory  \\
t? : TAG  \\
r! : REPORT  \\
h : Histogram 
\where
\lnot (\exists t:TAG @ tagbase~t * 1024 = membase~h)  \\
r! = histogram\_not\_associated\_with\_tag 
\end{schema}

\subsection{Total operations}
We can now specify total versions of our earlier operations:

\begin{zed}
CreateSpectrumOp \defs (CreateHistogrammerSpectrum \land Ok) \lor AlreadyExists
  \\ \t1 \lor BadShape \lor NoMemory \\
DeleteSpectrumOp \defs (DeleteHistogrammerSpectrum \land Ok) \lor UnknownSpectrum \\
ReadHistogramOp \defs (ReadHistogram \land Ok) \lor UnknownSpectrum \lor
  BadHistogram \\ \t1 \lor BadShape  \\
WriteHistogramOp \defs (WriteHistogram \land Ok) \lor UnknownSpectrum \lor
  BadHistogram \lor BadShape \\ \t1 \lor BadCounts  \\
ZeroHistogramOp \defs (ZeroHistogram \land Ok) \lor UnknownSpectrum \lor
  BadHistogram \lor BadShape \\ \t1 \lor BadCounts  \\
ReadExtremaOp \defs (ReadExtrema \land Ok) \lor UnknownSpectrum \lor
  BadHistogram  \\
WriteExtremaOp \defs (WriteExtrema \land Ok) \lor UnknownSpectrum \lor
  BadHistogram  \\
ReadAnnotationOp \defs (ReadAnnotation \land Ok) \lor UnknownSpectrum \lor
  BadAnnotation  \\
WriteAnnotationOp \defs (WriteAnnotation \land Ok) \lor UnknownSpectrum \lor
  BadAnnotation  \\
ReadCalibrationOp \defs (ReadCalibration \land Ok) \lor UnknownSpectrum \lor
  BadCalibration  \\
WriteCalibrationOp \defs (WriteCalibration \land Ok) \lor UnknownSpectrum \lor
  BadCalibration  \\
AssociateTagOp \defs (AssociateTag \land Ok) \lor UnknownSpectrum \lor
  BadHistogram \lor TagInUse  \\
DissociateTagOp \defs (DissociateTag \land Ok) \lor UnknownSpectrum \lor
  BadHistogram \lor NotAssociated
\end{zed}

\begin{thebibliography}{99}
\bibitem{JRA}{\em Eurogam Project: Specification of Histogrammer},
John Alexander, October 1990, EDOC???.
\end{thebibliography}

\end{document}