EDOC060

EUROGAM PROJECT

NSF DATA ACQUISITION SYSTEM

Eurogam Spectrum Servers: Online Histogrammer

Edition 0.9 December 1990

NSF Software Systems Group UK Science and Engineering Research Council Daresbury Laboratory Eurogam Spectrum Servers Online Histogrammer

David Brightly

Edition 0.9 December 1990

[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. D.B. Monday 10 December 1990]

1 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 EuroGam 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.

2 Generic spectra

2.1 Shapes, tuples, and domains

This section will describe the foundations which we will need to talk about histograms and spectra.

SHAPE == seq_{1}( × ) TUPLE == seq_{1} DOMAIN == TUPLE

Histograms are essentially arrays of a certain shape. For example, a simple one dimensional histogram might have a shape given by ⟨(0, 1024)⟩. 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 ⟨(1, 64), (0, 4096)⟩. In this example the channels in the first dimension are numbered 1 to 64. A tuple is a sequence of numbers labelling a channel in a histogram. The tuple ⟨23⟩ labels channel 23 of our first histogram and the tuple ⟨44, 2753⟩ labels a channel in our two dimensional example. A 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 dimension defined in the obvious way: dimension : TUPLE → _{1} shapedimension : SHAPE → _{1}

∀ t : TUPLE • dimension(t) = #t ∀ s : SHAPE • shapedimension(s) = #s

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:

size : SHAPE →

∀ a, b : ; s : SHAPE • size ⟨(a, b)⟩ = b ∧ size(s) = size(⟨head s⟩) ∗ size(tail s)

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 ⟨100⟩ precedes ⟨200⟩ and ⟨23, 3192⟩ precedes ⟨44, 1024⟩.

precedes : TUPLE ↔ TUPLE

∀ a, b : ; x, y : TUPLE | #x = #y • (⟨a⟩ precedes ⟨b⟩ ⇔ a < b) ∧ (x precedes y ⇔ (head x < head y ∨ (head x = head y ∧ tail x precedes tail y)))

We can say whether a given sequence of tuples is ordered or not:

ordered : (seq TUPLE)

∀ s : seq TUPLE • ordered s ⇔ (∀ i, j : dom s • (i < j ) ⇔ s i precedes s j )

and given a set of tuples we can order them:

order : DOMAIN → seq TUPLE

∀ d : DOMAIN ; s : seq TUPLE • s = order(d) ⇔ ran s = d ∧ ordered s

We can also say whether a given tuple lies within a given shape. For example, we have ⟨11, 999⟩ within ⟨(1, 64), (0, 4096)⟩ but not ⟨2048⟩ within ⟨(0, 1024)⟩.

within : TUPLE ↔ SHAPE

∀ x, a, b : ; t : TUPLE; s : SHAPE • (⟨x⟩ within ⟨(a, b)⟩ ⇔ 0 ≤ x − a < b) ∧ (t within s ⇔ ⟨head t⟩ within ⟨head s⟩ ∧ tail t within tail s)

Given a shape we can now return the domain consisting of all the channels that lie within that shape:

rectdomain : SHAPE → DOMAIN

∀ s : SHAPE • rectdomain(s) = {d : TUPLE | d within s} 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.

offset : TUPLE × SHAPE →

∀ s : SHAPE; x, a, b : ; t : TUPLE • offset(⟨x⟩, ⟨(a, b)⟩) = x − a ∧ offset(t, s) = offset(⟨head t⟩, ⟨head s⟩) ∗ size(tail s) + offset(tail t, tail s)

For example, we have

offset(⟨23⟩, ⟨(0, 1024)⟩) = 23

and

offset(⟨11, 999⟩, ⟨(1, 64), (0, 4096)⟩) = 10 ∗ 4096 + 999.

The following relationships can be proved (by induction on the dimension of the shape s):

∀ x, y : TUPLE; s : SHAPE | x within s ∧ y within s • 0 ≤ offset(x, s) < size s ∧ x precedes y ⇔ offset(x, s) < offset(y, s) ∧ order(rectdomain s)(offset(x, s) + 1) = x

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).

2.2 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.

Histogram shape : SHAPE counts : TUPLE \underrightarrow{} mincount : maxcount :

dom counts = rectdomain shape

A spectrum consists not only of counts but also of calibrations and 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 precision, i.e., the number of bits required to represent the counts. [need to think out the semantics of precision further]

[STRING] PRECISION ::= bit16 | bit32

maxannotations : maxhistograms : maxcalibrations : NULL : STRING

maxannotations = 16 maxcalibrations = 16 maxhistograms = 16

A spectrum is specified as follows:

Spectrum precision : PRECISION sshape : SHAPE arrays : 1 . . maxhistograms \underrightarrow{}Histogram calibrations : 1 . . maxcalibrations \underrightarrow{}STRING annotations : 1 . . maxannotations \underrightarrow{}STRING

∀ i : dom arrays • (arrays i).shape = sshape dom calibrations ⊆ 1 . . shapedimension sshape

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:

Attributes s : SHAPE p : PRECISION

2.3 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:

name  ::= /histogrammern/simplename
| /sortern/simplename
| /simplename/ … /simplename
simplename ::= any printable name without / or blank
n  ::= integer

[in a multiple front end system should there be a leading /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:

[NAME, SIMPLENAME]

DIRECTORY == SIMPLENAME \underrightarrow{}Spectrum STORE == NAME \underrightarrow{}Spectrum

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.

SpectrumStore store : STORE

Given a directory within the store we must be able to obtain a list of the spectra within it (analogous to the unix ls command):

ReadDirectory

dir? : DIRECTORY nn! : iseq SIMPLENAME

ran nn! = dom dir?

and also a list of spectra together with their attributes (analogous to ls -l):

ReadDirectoryWithAttributes

dir? : DIRECTORY

nana! : iseq(SIMPLENAME × Attributes)

∀ n : SIMPLENAME; s : Spectrum; a : Attributes •

(n, a) ∈ ran nana! ⇔ s = dir?(n) ∧ a.s = s.sshape ∧ a.p = s.precision

2.4 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 EuroGam histogrammer.

CreateSpectrum ΔSpectrumStore spectrum : Spectrum name? : NAME s? : SHAPE p? : PRECISION h : Histogram

name? ∉ dom store spectrum.precision = p? spectrum.sshape = s? spectrum.calibrations = spectrum.annotations = spectrum.arrays = {1 ↦ h} h.shape = s? ran h.counts = {0} h.mincount = h.maxcount = 0 store′ = store ⊕ {name? ↦ spectrum}

DeleteSpectrum ΔSpectrumStore name? : NAME

name? ∈ dom store store′ = {name?} − store

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.

AccessSpectrum ΞSpectrumStore n? : NAME s : Spectrum

n? ∈ dom store s = store n?

ModifySpectrum ΔSpectrumStore n? : NAME s, s′ : Spectrum

n? ∈ dom store s = store n? s′.sshape = s.sshape store′ = store ⊕ {n? ↦ s′}

The following operation returns the attributes of a spectrum—its shape and precision:

InquireAttributes AccessSpectrum n? : NAME a! : Attributes

a!.s = s.sshape ∧ a!.p = s.precision

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

ReadHistogram ΞSpectrumStore AccessSpectrum i? : s? : SHAPE h : Histogram z! : seq

i? ∈ dom s.arrays h = s.arrays i? rectdomain s? ⊆ rectdomain h.shape z! = h.counts ∘ (order(rectdomain s?))

WriteHistogram ΔSpectrumStore ModifySpectrum i? : s? : SHAPE z? : seq h, h′ : Histogram

i? ∈ dom s.arrays h = s.arrays i? rectdomain s? ⊆ rectdomain h.shape h′.counts = h.counts ⊕ {j : dom z? • order(rectdomain s?)j ↦ z? j } h′.shape = h.shape s′.arrays = s.arrays ⊕ {i? ↦ h′} s′.annotations = s.annotations s′.calibrations = s.calibrations

ZeroHistogram ΔSpectrumStore ModifySpectrum i? : s? : SHAPE h, h′ : Histogram

i? ∈ dom s.arrays rectdomain s? ⊆ rectdomain h.shape h′.counts = h.counts ⊕ {t : rectdomain s? • t ↦ 0} h′.shape = h.shape h′.mincount = h′.maxcount = 0 s′.arrays = s.arrays ⊕ {i? ↦ h′} s′.annotations = s.annotations s′.calibrations = s.calibrations

ReadExtrema ΞSpectrumStore AccessSpectrum i? : h : Histogram min!, max! :

i? ∈ dom s.arrays h = s.arrays i? min! = h.mincount max! = h.maxcount WriteExtrema ΔSpectrumStore ModifySpectrum i? : min?, max? : h, h′ : Histogram

i? ∈ dom s.arrays h′.shape = h.shape h′.counts = h.counts h′.mincount = min? h′.maxcount = max? s′.arrays = s.arrays ⊕ {i? ↦ h′} s′.annotations = s.annotations s′.calibrations = s.calibrations

ReadCalibration ΞSpectrumStore AccessSpectrum c! : STRING i? :

i? ∈ dom s.calibrations c! = s.calibrations i?

WriteCalibration ΔSpectrumStore ModifySpectrum c? : STRING i? :

i? ∈ dom s.calibrations s′.sshape = s.sshape s′.arrays = s.arrays s′.annotations = s.annotations s′.calibrations = s.calibrations ⊕ {i? ↦ c?}

ReadAnnotation ΞSpectrumStore AccessSpectrum a! : STRING i? :

i? ∈ 1 . . maxannotations a! = s.annotations i?

WriteAnnotation ΔSpectrumStore ModifySpectrum a? : STRING i? :

i? ∈ 1 . . maxannotations s′.sshape = s.sshape s′.arrays = s.arrays s′.annotations = s.annotations ⊕ {i? ↦ a?} s′.calibrations = s.calibrations

3 EuroGam online histogrammer

3.1 Histogrammer memory

The previous sections have described spectra in general. We now come to specific properties of the EuroGam 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.

VMElimit : RMbase : RMrange :

VMElimit = 1024 ∗ 1024 ∗ 1024 0 ≤ RMbase ∧ RMbase + RMrange ≤ VMElimit

We can model the actual histogramming memory with a function which returns the contents of a memory word, given its address.

RealMemory memory : →

dom memory = RMbase . . RMbase + RMrange − 1

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.

HistogramMemory membase : Histogram \underrightarrow{} memrange : Histogram \underrightarrow{} memused : Histogram \underrightarrow{} memfree : ( × )

dom membase = dom memrange

∀ h : Histogram • h ∉ dom membase ⇒ memused(h) = ∧ h ∈ dom membase ⇒ memused(h) = membase(h) . . membase(h) + memrange(h) − 1

∀ m, r : •

memfree(m, r) ⇔ (∀ h : dom membase • (m . . m + r − 1) ∩ memused h = ) ∧ 0 ≤ m < m + r ≤ RMrange

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.

3.2 Histogrammer card

In this section we describe the EuroGam histogrammer card as outlined in [1]. We need to talk about enabling and disabling aspects of the card’s function:

STATE ::= enabled | disabled

We need to refer to the data acquisition channel “addresses” which label conversions received by the histogrammer. We will call these tags in order to distinguish them from histogramming memory addresses.

[TAG]

We can now describe the histogrammer card itself:

HistogrammerCard state : STATE tagstate : TAG → STATE tagbase : TAG \underrightarrow{} baseaddress :

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 [1]. 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 we can specify the operation of the histogrammer card when presented with a tag t? and a data word d? [1, section 3.3].

Increment ΞHistogrammerCard ΔRealMemory t? : TAG d? :

state = enabled ∧ tagstate t? = enabled ⇔

(∃ a : • a = baseaddress bitor(tagbase t? ∗ 1024) bitor d? ∧ memory′ = memory ⊕ {a ↦ memory(a) + 1})

3.3 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:

Histogrammer HistogrammerCard HistogramMemory RealMemory address : Histogram × TUPLE → SpectrumStore

∀ t : TAG • tagstate t = enabled ⇒ (∃ h : Histogram • membase h = tagbase t ∗ 1024)

∀ s : ran store • shapedimension s.sshape = 1 ∧ first(head s.sshape) = 0

∀ h : dom membase; t : TUPLE | t within h.shape • address(h, t) = RMbase + membase(h) + offset(t, h.shape) ∧ h.counts(t) = memory(address(h, t))

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 [1, section 3.6]; 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 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

∃ n • ∀ h • RMbase mod 2^{n} = 0 ∧ 2^{n} > membase(h) + c and that,

∀ h • ∃ m • membase(h) mod 2^{m} = 0 ∧ 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 RMbasemodRMrange = 0.

validranges :

validranges = {1024, 2048, 4096, 8192} RMbase mod RMrange = 0

[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.

InitHistogrammer Histogrammer

state = enabled ∀ t : TAG • tagstate t = disabled membase = memrange = baseaddress = RMbase store =

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 map a certain tag onto that histogram.

MapTag ΔHistogrammerCard ΞHistogramMemory h? : Histogram t? : TAG

state = disabled = state′ tagstate t? = disabled tagstate′ = tagstate ⊕ {t? ↦ enabled} tagbase′ = tagbase ⊕ {t? ↦ membase h? div 1024} baseaddress′ = baseaddress 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.

UnMapTag ΔHistogrammerCard ΞHistogramMemory t? : TAG

state = disabled = state′ tagstate t? = enabled tagstate′ = tagstate ⊕ {t? ↦ disabled} tagbase′ = {t?} − tagbase baseaddress′ = baseaddress

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.

Go ΔHistogrammerCard ΞHistogramMemory

state = enabled

Stop ΔHistogrammerCard ΞHistogramMemory

state′ = disabled

We can now promote these operations to the spectrum level:

StopMapTagGo ˆ= Stop ^{o}_{9} MapTag ^{o}_{9} Go StopUnMapTagGo ˆ= Stop ^{o}_{9} UnMapTag ^{o}_{9} Go

AssociateTag AccessSpectrum StopMapTagGo i? :

h? = s.arrays i?

DissociateTag AccessSpectrum StopUnMapTagGo i? : h : Histogram

h = s.arrays i? t? = (μ t : TAG | tagbase t ∗ 1024 = membase h)

We can now completely define the operations of creating a new histogrammer spectrum and of deleting one:

CreateHistogrammerSpectrum ΔHistogrammer ΞHistogrammerCard CreateSpectrum m, r :

shapedimension spectrum.sshape = 1 ∧ first(head spectrum.sshape) = 0 r = size s? ∧ r ∈ validranges m mod r = 0 memfree(m, r)

membase′ = membase ⊕ {h ↦ m} memrange′ = memrange ⊕ {h ↦ r}

DeleteHistogrammerSpectrum ΔHistogrammer t? : TAG DeleteSpectrum h : Histogram

h = (store name?).arrays 1 (∃ t? : TAG | tagbase t? ∗ 1024 = membase h • StopUnMapTagGo) ∨ (¬ (∃ t? : TAG | tagbase t? ∗ 1024 = membase h • ΞHistogrammerCard)) membase′ = {h} − membase memrange = {h} − memrange

3.4 Error conditions

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

Ok r! : REPORT

r! = ok BadShape r! : REPORT s? : SHAPE h : Histogram

¬ rectdomain s? ⊆ rectdomain h.shape r! = domain outside spectrum

BadCalibration r! : REPORT s : Spectrum i? :

¬ i? ∈ 1 . . shapedimension s.sshape r! = invalid calibration number

BadAnnotation r! : REPORT i? :

¬ i? ∈ 1 . . maxannotations r! = invalid annotation number

BadCounts r! : REPORT i? : s? : SHAPE z? : seq

#z? ≠ size s? r! = counts dont fill shape

BadHistogram r! : REPORT i? : s : Spectrum

¬ i? ∈ dom s.arrays r! = invalid annotation number

UnknownSpectrum ΞHistogrammer r! : REPORT n? : NAME

¬ n? ∈ dom store r! = spectrum not known AlreadyExists ΞHistogrammer r! : REPORT n? : NAME

n? ∈ dom store r! = spectrum already exists

UnsuitableShape s? : SHAPE r! : REPORT

¬ (shapedimension s? = 1 ∧ first(head s?) = 0 ∧ second(head s?) ∈ validranges) r! = shape unsuitable for histogrammer

NoMemory ΞHistogrammer s? : SHAPE r! : REPORT

¬ (∃ m, r : • r = size s? ∧ m mod r = 0 ∧ memfree(m, r)) r! = insufficient histogramming memory

TagInUse ΞHistogrammerCard t? : TAG r! : REPORT

tagstate t? = enabled r! = tag already being histogrammed

NotAssociated ΞHistogrammerCard ΞHistogramMemory t? : TAG r! : REPORT h : Histogram

¬ (∃ t : TAG • tagbase t ∗ 1024 = membase h) r! = histogram not associated with tag

3.5 Total operations

We can now specify total versions of our earlier operations:

CreateSpectrumOp ˆ= (CreateHistogrammerSpectrum ∧ Ok) ∨ AlreadyExists

∨ BadShape ∨ NoMemory DeleteSpectrumOp ˆ= (DeleteHistogrammerSpectrum ∧ Ok) ∨ UnknownSpectrum ReadHistogramOp ˆ= (ReadHistogram ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram

∨ BadShape WriteHistogramOp ˆ= (WriteHistogram ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram ∨ BadShape

∨ BadCounts ZeroHistogramOp ˆ= (ZeroHistogram ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram ∨ BadShape

∨ BadCounts ReadExtremaOp ˆ= (ReadExtrema ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram WriteExtremaOp ˆ= (WriteExtrema ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram ReadAnnotationOp ˆ= (ReadAnnotation ∧ Ok) ∨ UnknownSpectrum ∨ BadAnnotation WriteAnnotationOp ˆ= (WriteAnnotation ∧ Ok) ∨ UnknownSpectrum ∨ BadAnnotation ReadCalibrationOp ˆ= (ReadCalibration ∧ Ok) ∨ UnknownSpectrum ∨ BadCalibration WriteCalibrationOp ˆ= (WriteCalibration ∧ Ok) ∨ UnknownSpectrum ∨ BadCalibration AssociateTagOp ˆ= (AssociateTag ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram ∨ TagInUse DissociateTagOp ˆ= (DissociateTag ∧ Ok) ∨ UnknownSpectrum ∨ BadHistogram ∨ NotAssociated

References

[1] Eurogam Project: Specification of Histogrammer, John Alexander, October 1990, EDOC???.