6.4.1 The Mereology Entities ≡ Processes
The model of mereology presented in Sect. 6.2 (Pages 21–28) focused on the following simple entities (i) the assemblies, (ii) the units and (iii) the connectors. To assemblies and units we associateCSPprocesses, and to connectors we associate aCSPchannels, one-by-one [26]. The connectors form the mereological attributes of the model.
6.4.2 Channels 136
The CSP channels, are each “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 two unit or assembly processes.
137
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
138
Process Definitions value
system: S → Process system(s) ≡ assembly(s)
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Σ
139
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Σ
The meaning processesMA and MU are generic. Their sˆole purpose is to provide a never ending recursion. “In-between” they “make use” of assembly, respectively unit specific
functions here symbolised by UA, respectively UF. 140
Mereology, Part III A little more meaning has been added to the notions of parts and connections. The within and adjacent to relations between parts (assemblies and units) reflect a phenomenological world of geometry, and the connected relation between parts (assemblies and units) reflect both physical and conceptual world understandings: physical world in that, for example, radio waves cross geometric “boundaries”, and conceptual world in that ontological classifications typically reflect lattice orderings where overlaps likewise
cross geometric “boundaries”. 141
Discussion
Partial Evaluation Theassembly function “first” “functions” as a compiler. The ‘com-piler’ translates an assembly structure into three process expressions: the MA(a)(aσ) invocation, the parallel composition of assembly processes,a′, one for each sub-assembly of a, and the parallel composition of unit processes, one for each unit of assembly a — 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σ) andMU(u)(uσ) process expressions are invoked.
6.4.3 Generalised Channel Processes 142
We can refine the meaning of connectors. Each connector, so far, was modelled by a CSP channel. CSP channels 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.
That completes our ‘contribution’: A mereology of systems has been given a syntactic explanation, Sect. 2, a semantic explanation, Sect. 5 and their relationship to classical mereologies.
6.5 “Connectability” cum “Overlap” in Other Computing Models
143
In this section we investigate the concept of “connectability” cum “overlap” in other com-puting models. The “other” comcom-puting models are:
• Petri nets [32],
• Message Sequence Charts (MSC)[27] and
• Statecharts [25].
7 Laws of Descriptions
1448 Laws of Domain Facets
1458.1 Intrinsics
1468.2 Support Technologies
1478.2.1 A Generic Example
Traffic (tf:TF), intrinsically, is a total function over some time interval, from time (t:T) to continuously positioned (p:P) vehicles (v:V).
Conventional optical sensors sample, at regular intervals, the intrinsic traffic. The result is a sampled traffic (stf:sTF). Hence the collection of all optical sensors, for any given net, is a partial function from intrinsic (itf) to sampled train traffics (stf).
We need to express quality criteria that any optical sensor technology should satisfy — relative to a necessary and sufficient description of a closeness predicate.
148
For all intrinsic traffics,itf,and for all optical sensor technologies,ost,the following must hold: Let stf be the traffic sampled by the optical sensor technology. For all time points, t,in the sampled traffic, those time points must also be in the intrinsic traffic, and, for all vehicles, v,in the intrinsic traffic at that time, the train must be observed by the optical sensor technology, and the actual (i.e., intrinsice) position of a[ny] vehicle and the sampled position must somehow be checkable to beclose, including identical to one another.
Since hubs change state with time, n:N, the net needs to be part of any model of traffic.
149
type T, TN P
NetTraffic :: net:N × trf:(V →m P) iTF = T → NetTraffic
sTF = T →m NetTraffic OST = iTF →∼ sTF value
close: NetTraffic × V ×NetTraffic →∼ Bool axiom
∀ itf:iTF, ost:OST • letstf = ost(itf) in
∀ t:T • t ∈dom stf •
t ∈ DOM itf ∧ ∀v:V • v ∈ dom trf(itf(t))
⇒v ∈dom trf(stf(t)) ∧ close(itf(t),v,stf(t)) end
DOM is not an RSLoperator. It is a mathematical way of expressing the definition set of a general function. Hence it is not a computable function.
Checkability is an issue of testing the optical sensors when delivered for conformance to the closeness predicate, i.e., to the axiom.
8.2.2 General 150
The formal requirements can be narrated:Let Θi and Θa designate the spaces of intrinsic and actual-world configurations (contexts and states). For each intrinsic configuration model — that we know is support technology assisted — there exists a support technology solution, that is, a total function from all intrinsic configurations to corresponding actual configurations. If we are not convinced that there is such a function then there is little hope that we can trust this technology
type Θi, Θa
ST = Θi →Θa
axiom
∀ sts:ST-set, st:ST • st ∈sts ⇒ ∀θi:Θi,∃ θa:Θa • st(θi) = θa
8.3 Rules and Regulations
151There are, abstractly speaking, usually three kinds of languages involved wrt. (i.e., when expressing) rules and regulations (respectively when invoking actions that are subject to rules and regulations). Two languages, Rules and Reg, exist for describing rules, respec-tively regulations; and one, Stimulus, exists for describing the form of the [always current]
domain action stimuli. 152
A syntactic stimulus, sy sti, denotes a function,se sti:STI: Θ→ Θ, from any configura-tion to a next configuraconfigura-tion, where configuraconfigura-tions are those of the system being subjected to stimulations. A syntactic rule,sy rul:Rule,stands for, i.e., has as its semantics, its meaning, rul:RUL, a predicate over current and next configurations, (Θ× Θ) → Bool,where these next configurations have been brought about, i.e., caused, by the stimuli. These stimuli express: If the predicate holds then the stimulus will result in a valid next configuration. 153
type
Stimulus, Rule, Θ STI = Θ → Θ
RUL = (Θ × Θ)→ Bool value
meaning: Stimulus → STI meaning: Rule → RUL
valid: Stimulus × Rule → Θ→ Bool
valid(sy sti,sy rul)(θ) ≡meaning(sy rul)(θ,(meaning(sy sti))(θ)) valid: Stimulus × RUL→ Θ →Bool
valid(sy sti,se rul)(θ) ≡ se rul(θ,(meaning(sy sti))(θ))
154
A syntactic regulation, sy reg:Reg (related to a specific rule), stands for, i.e., has as its semantics, its meaning, a semantic regulation, se reg:REG, which is a pair. This pair consists of a predicate,pre reg:Pre REG,wherePre REG = (Θ×Θ)→Bool,and a domain configuration-changing function, act reg:Act REG,where Act REG =Θ→ Θ, that is, both involving current and next domain configurations. 155The two kinds of functions express: If the predicate holds, then the action can be applied.
The predicate is almost the inverse of the rules functions. The action function serves to undo the stimulus function.
156
type Reg
Rul and Reg = Rule × Reg REG = Pre REG ×Act REG Pre REG = Θ ×Θ → Bool Act REG = Θ → Θ
value
interpret: Reg → REG
157
The idea is now the following: Any action of the system, i.e., the application of any stimulus, may be an action in accordance with the rules, or it may not. Rules therefore express whether stimuli are valid or not in the current configuration. And regulations therefore express whether they should be applied, and, if so, with what effort.
158
More specifically, there is usually, in any current system configuration, given a set of pairs of rules and regulations. Let(sy rul,sy reg)be any such pair. Letsy stibe any possible stimulus. And let θ be the current configuration. Let the stimulus, sy sti, applied in that configuration result in a next configuration, θ′, where θ′ = (meaning(sy sti))(θ). Let θ′ violate the rule,∼valid(sy sti,sy rul)(θ),then if predicate part,pre reg,of the meaning of the regulation,sy reg,holds in that violating next configuration,pre reg(θ,(meaning(sy sti))(θ)), then the action part, act reg, of the meaning of the regulation, sy reg, must be applied, act reg(θ),to remedy the situation.
159
axiom
∀ (sy rul,sy reg):Rul and Regs • let se rul = meaning(sy rul),
(pre reg,act reg) = meaning(sy reg) in
∀ sy sti:Stimulus, θ:Θ •
∼valid(sy sti,se rul)(θ)
⇒ pre reg(θ,(meaning(sy sti))(θ))
⇒ ∃ nθ:Θ• act reg(θ)=nθ ∧ se rul(θ,nθ) end
160
It may be that the regulation predicate fails to detect applicability of regulations actions.
That is, the interpretation of a rule differs, in that respect, from the interpretation of a regulation. Such is life in the domain, i.e., in actual reality