Version 0.1 1
1 Introduction
The primitives in this description are Channel s and items of Work.
It is assumed that work is a message transfer or acknowledgement of
some kind. It is not important. What is important is that a series of
items of Work needs to be done for a Channel and we cannot allow
two items of work to be processed for the same Channel at the same
time. So we introduce the primitive sets:
[Channel, Work]
and with these we can describe the general state.
2 The general state of things
The basic state of the system is a collection of Channels with a se-
quence of items of work associated with each:
Pool
pool : Channel 7→ seq Work
The pool of known channels (dom pool) is partitioned into those
which are dormant, those ready for work to be done, and those which
are currently being processed (inprogress).
We define a convenience schema for each partition. This is to name
them for use in explicitly stating preservation later.
The dormant ones have no work (but we cannot impose this con-
straint without the pool – we do it later):
Dormant
dormant : P Channel
the ready ones are ordered:
Ready
ready : iseq Channel
and the rest are ‘in progress’:
InProgress
inprogress : P Channel
- 1
- 2
前往页