Part III Proper Conceptualisation
Definition 38: Mereology
6.3.2 Behaviours
Behaviours can be simple, sequential, and behaviours can be highly composite. To define be-haviours we need notions of states and actions: By adomain statewe mean any collection of simple entities — so designated by the domain engineer. By a domain actionwe mean the invocation of
an operation which “changes” the state.6 s296
Definition 39 –Behaviours: (i) By abehaviourwe shall understand either a simple, sequential behaviour, or a simple parallel (or concurrent) behaviour, or a communicating behaviour. (ii) By a simple, sequential behaviour we shall understand a sequence of actions and events (the latter to be defined shortly). (iii) By a simple parallel (or concurrent) behaviour we shall understand a set of simple, sequential behaviours. (iv) By acommunicating behaviour we shall understand a set of simple parallel behaviours which in addition (to being simple parallel behaviours) communicate messages between one-another.
s297
We shall base our formal specification of behaviours on the use of CSP(Hoare’s Communicating Sequential Processes [81,82,130,134]). Other concurrency formalisms can, of course, be used: Petri nets [91,115,123–125], Message Sequence Charts (MSCs) [86–88], Statecharts [71–74,76], or other.
Communication, between two behaviours (CSPprocesses),PandQis inCSPexpressed by the CSPoutput and input clauses: ch ! e, respectivelych ?wherech designates aCSP channel. s298
type
wherea, a′ andb, b′ designate processP, respectively processQstate values provided to process invocations (witha′andb′ resulting from “calculations” not shown in the bodies of the definitions of PandQ.avandbvare initial entities.S is the overall system behaviour of two communicating behaviours operating in parallel (k).Mdesignates the type of the messages sent over channelch.
We shall now show a duality between entities and behaviours. The background for this duality is the following: In everyday parlance we speak of some domain phenomena both as being entities
and as embodying behaviours. s300
Example 43 –Entities and Behaviours: A train is the composite entity of one or more engines (i.e., locomotives) and one or more passenger and/or freight cars.
6Since we shall be expressing our formalisations in a pure, functional language, state changes are expressed by functions whose signature include state entity types both as arguments and as results.
type
Train, Engine, PassCar, FreightCar Car =PassCar|FreightCar
value
obs Engine: Train→Engine obs Carl: Train →Car∗ axiom
∀ tr:Train•cardobs Carl(tr)>0
s301 A train is also the behaviour whose state include the time dependent train location and the states of these engines and cars and whose sequence of actions comprise the arrival and stop of the train at stations, the unloading and loading of passengers and freight at stations, the start-up and departure of trains from stations and the continuous movement, initially at accelerated speeds, then constant speed, finally at decelerating speeds along the rail track between stations — occasionally allowing for stops at track segment blocking signals. A train behaviour event could be that a cow presence of the track causes interrupt of scheduled train behaviour. Et cetera.
s302
type T, Loc,
TrainBehaviour=T →m Train channel
net channel (is at station|Bool) value
obs Loc: Train→Loc
train: Train→T→out,innet channel→Unit train(tr)(t)≡
if is at Station(obs Loc(tr)) then
let (tr′,t′)=stop train(tr)(t);
let (tr′′,t′′)=load unload passengers and freight(tr′)(t′)in let (tr′′′,t′′′)=move train(tr′′)(t′′)in
[ assert: ∼is at Station(obs Loc(tr′′′)) ] train(eσ′′,(el′,pfl′),loc′)(t′)end end end
else
let (tr′,t′)=move train(tr)(t) intrain(tr′)(t′)end end
s303 Here we leave undefined a number of auxiliary functions:
value
is at Station: Loc →out,innet channel Bool stop train: Train→T→Train×T
load unload passengers and freight: Train→T→Train×T move train: Train →T →Train×T
The above “model” of a train behaviour is really not of the kind (of models) that we shall eventually seek. The predicate is at Station communicates with the net behaviour (not shown). The function load unload passengers and freight communicates with the net behaviour (platforms, marshalling yards, etc., not shown). It is a rough sketch meant only to illustrate the process behaviour.
s304
Example 42 illustrated a very general class of mereologies. The next example, Example 44 will show how the duality between entities and behaviours can be “drawn” to an ultimate conclusion !
s305
Example 44 –Mereology: Parts and Wholes (2): The model of mereology presented in Exam-ple 42 on page 60 (Pages 60–62) focused on the following simExam-ple entities
6.3 Simple Entities and Behaviours 65
• the assemblies,
• the units and
• the connectors.
To assemblies and units we associate CSP processes, and to connectors we associate CSPchannels,
one-by-one [81, 82, 130, 134]. s306
The connectors form the mereological attributes of the model.
To each connection we associate aCSPchannel, it is “anchored” in two parts: if a part is a unit then in “its corresponding” unit process, and if a part is an assembly then in “its corresponding” assembly process.
From a system assembly we can extract all connector identifiers. They become indexes into an array of channels. Each of the connector channel identifiers is mentioned in exactly one unit or one assembly
process. s307
From a system which is an assembly, we can extract all the connector identifiers as well as all the internal connector identifiers. They become indexes into an array of channels. Each of the external connector channels is mentioned in exactly one unit or one assembly process; and each of these internal connection channels is a mentioned in exactly two unit or assembly processes. The xtr∀KIs(s) below
was defined in Example 42 (Page 62). s308
value s:S
kis:KI-set=xtr∀KIs(s) type
ChMap=AUI →m KI-set value
cm:ChMap= [obs AUI(p)7→obs KIs(p)|p:P•p∈xtr Ps(s)] channel
ch[i|i:KI•i∈kis]MSG value
system: S→Process system(s)≡assembly(s)
s309
value
assembly: a:A→in,out{ch[cm(i)]|i:KI•i∈cm(obs AUI(a))}process assembly(a)≡
MA(a)(obs AΣ(a))k
k {assembly(a′)|a′:A•a′∈obs Ps(a)} k k {unit(u)|u:U•u∈obs Ps(a)}
obs AΣ: A →AΣ
MA: a:A→AΣ→in,out{ch[cm(i)]|i:KI•i∈cm(obs AUI(a))} process MA(a)(aσ)≡ MA(a)(AF(a)(aσ))
AF: a:A→AΣ→in,out{ch[em(i)]|i:KI•i∈cm(obs AUI(a))}×AΣ
s310
The unit process is defined in terms of the recursive meaning functionMU function which requires access to all the same channels as the unit process.
value
unit: u:U→in,out{ch[cm(i)]|i:KI•i∈cm(obs UI(u))}process unit(u)≡ MU(u)(obs UΣ(u))
obs UΣ: U→UΣ
MU: u:U→UΣ→in,out{ch[cm(i)]|i:KI•i∈cm(obs UI(u))} process
MU(u)(uσ)≡ MU(u)(UF(u)(uσ))
UF: U→UΣ →in,out{ch[em(i)]|i:KI• i∈cm(obs AUI(u))} UΣ
s311
The meaning processesMUandMAare generic. Their sˆole purpose is to provide a never ending recur-sions. “In-between” they “makes use” of assembly, respectively unit specific functions here symbolised byAF andUF.
s312
The assembly function “first” “functions” as a compiler. The ‘compiler’ translates an assembly structure into three process expressions: the MA(a)(aσ, aρ) invocation, the parallel composition of assembly processes,a′, one for each sub-assembly ofa, and the parallel composition of unit processes, one for each unit of assemblya — with these three process expressions “being put in parallel”. The recursion in assembly ends when a sub-. . . -assembly consists of no sub-sub-. . . -assemblies. Then the compiling task ends and the many generatedMA(a)(aσ, aρ)andMU(u)(uσ, uρ)process expressions are invoked.
s313
We can refine the meaning of connectors. Each connector, so far, was modelled by aCSPchannel.
CSPchannels serve both as a synchronisation and as a communication medium. We now suggest to model it by a process. A channel process can be thought of as having four channels and a buffering process. Connector,κ:K, may connect parts πi, πj. The four channels could be thought of as indexed by (κ, πi),(πi, κ),(κ, πj) and(πj, κ). The process buffer could, depending on parts pi, pj, be either
queues, sets, bags, stacks, or other. This ends Example 44
s314
The duality between simple entities and behaviours has the attributes of atomic as well as of composite entities become the state in which the entity behaviours evolve.
Whereas — in principle — the mereology of how sub-entities compose into entities are modelled as in Example 42, namely in terms of sorts, observer functions and axioms over unique identifiers of simple entities, their attributes are usually modelled in a more model-oriented way, in terms of mathematical sets, Cartesians, sequences and maps.