.Open Flows and Flow Diagrams
. Introduction
This document tries to show that the kind of flow diagrams used informally
by Systems Analysts and (more formally) by electrical engineers and others
have a formal model that accounts for the way they are used. The overall
structure is that DFDs (
.See Data Flow Diagrams
) are explained in terms of general hierarchical flow
diagrams
.See Hierarchical FFDs
and these, in turn are defined in terms of
.See Formal Flow Diagrams
and (in turn) these depend on a novel kind of algebraic poset(Partially Ordered
sets
.See http://www/dick/maths/math_21_Order.html#poset
) that I call a
.See Flosets
.Open Flosets
. Introduction to Flosets
Here are some examples of the kinds of situations that the '$FLOW' model is intended to cover:
. Examples of Flows
Numbers of objects in a part of system per unit time.
Data Types being used in each part of a system.
Frequencies with which something is done.
Number of derivations of a string in a particular grammar.
Types of objects flowing between classes in some software.
. Theory of Flows
FLOW::=Net{
Flows can be combined, and the order in which this is done does not effect the result. There is also a null or zero flow - which has no effect when combined with any other flow. This set of assumptions is describes an `Abelian Monoid`
.See http://www/dick/maths/math_33_Monoids.html#Abelian_monoid
|-(F1): Abelian_monoid(Set=>Flows, op=>+, u=>0).
(F1)|-(F1.1): for all f:Flows ( f+0 = 0 = 0 +f ),
(F1)|-(F1.2): for all f1,f2:Flows(f1+f2=f2+f1).
(F1)|-(F1.3): for all f1,f2,f3:Flows((f1+f2)+f3= f1+(f2+f3)).
We require that there is at least one non-zero flow - ie. at least two:
|-(F2): |Flows|>1.
We can recognize when one flow contains another. This can be modeled as
a partially ordered set
.See http://www/dick/maths/math_21_Order.html#poset
|-(F3): poset(Set=>Flows, order=>(<=), inverse=>(>=), strict=>(<), strict_inverse=>(>)).
The above incorporates definitions of the usual relations: `<`, `<=`, `>`, and
`>=` plus rules like the transitivity and strictness of `<`:
(F3)|-(trans <): for all x,y,z, if x=f1,f2 ).
One flow is greater than another if and only if the first results by adding a flow to the second one:
|-(F5): for all f1,f2 ( f10 and f1+f3=f2) ).
(F2,F1.1)|-(F6): for some f(f<>0) and for all f(0+f=f),
(F6)|-(F7): for some f(f<>0 and 0+f=f),
(F7,F4,F5)|-(F8): for some f(0(0).
Adding a flow to two flows preserves their order:
|-(F10):for all f1,f2,f3, if f1f2.
()|-(F12): 0<=0.
Consider{0+0=0}
()|-(F13): for all f:Flows (0<=f).
Consider{f, |-0+f=f}
()|-(F14): for all f, f<>0(f>0).
()|-(F15): for all f1,f2:Flows, if f1<>0 then f1+f2<>0,
()|-(F16): for all f1,f2, if f1+f2=0 then f1=0=f2.
()|-(F17): for no f (f<0),
. Proof of F15
.Let
|-(F15.1): f1,f2:Flows,
|-(F15.2): f1<>0,
|-(F15.3): f1+f2=0,
(F15.2)|-(F15.4): f1>0,
(F15.3,F15.4,>)|-(F15.5): f1+f2>0,
()|-(F15.6): f1+f2>f2,
(F15.6,F15.3)|-(F15.7): 0>f2,
()|-(F15.8): 0=f2.
.Close.Let
. Proof of F17
po{
|-(F17.1): f<0,
(F17.1)|-(F17.2): f<>0,
(Monoid)|-(F17.3): 0+f=f,
(<)|-(F17.4): 00,
}
}=::FLOW.
floset::=$ $FLOW.
(def)|- for all POSITIVE_SEMIRING(Set,+.0,.,1,...) ($FLOW(Set,+,0))
[MATHS.41 Two Operators.semiring]
. Example Flows
(def)|- ({0,1}, {(0,1)+>1, (1,1)+>1,...},0,{(0,0),(0,1),(1,1)}) in floset.
The above is half of a Boolean algebra.
(def)|- (Nat0,+,0) in floset.
(def)|- ([0..),+,0) in floset.
These are quantitative flows.
(def)|- For all S:Sets, (@S,|,{},==>) in floset.
This is a qualitive flow.
(def)|- (0.0..1.0, max,0) in floset
A Fuzzy flow.
(def)|- For all S:Sets, (F,+,0,<=) :floset, (S->F, + , [s]0,<=) in floset.
In this case (+)=[x,y:S->F]([s](x(s)+y(s))).
For S:Sets, Bag(S) ::=$ $FLOW(S->Nat0,+, 0).
For S, FuzzySet(S) ::=$ $FLOW(S->[0..1], max, 0).
. Applications
The following could be used in Data Flow Diagrams. First a qualitive data flow diagram where data is either present of absent on each arc:
|- For Data={Customer, Invoice, Invoice_item, Order, Order_item, ...},
((@Data, |, {}) in $ $FLOW ).
Or equivalently the following model forms a qualitative flow:
(Data->@,|,{},==>) in floset.
However:
(def)|- For all Data:Finite_set, (Data->Nat0,+,0,<=) in floset.
So we can also have a quantitive data flow:
for all a,b:@Nat0^Data(a < b ::= for all i:Data (a[i] < b[i]) ).
If these two models describe the same system then there is a homomorphism from the quantitive model to the qualitive, based on the map
qualify::(Data->Nat0)->(@Data)=map[S]0./S,
()|- qualify(S)={d:Data||S(d)>0}.
The following example, could be part of a model of Ozone depletion:
|- For Parts:={Ground, Lower_atmosphere, Upper_atmosphere, ...},
Chemicals:={H2O, CO2, O2, O3, NOn, SOn, C, S, N, ...},
((Real^Chemicals,+,0) in $ $FLOW), ((Real^Chemicals)^Parts,+,0) in $ $FLOW).
The following would be used in parts of D. Knuth's analysis of algorithms:
|- For Frequencies:=Nat0, ((Frequencies, +, 0) in $ $FLOW ).
In general:
squash(n) ::(S->Nat0)->(S->0..n) with addition redefined so that
a*b=min{a+b,n}.
is a homomorphism from a complex model to a simpler one.
. Exercise on Category of Flosets
Investigate the category of all flosets with homomorphisms that preserve 0, monoids and order. Are there free flosets (initial obejects) which can be mapped onto any other floset? Do products and co-products make sense? (Hint - monoids have a similar category - but in what sense?)
. Project - Petrie Nets and Flosets
Use a floset to model for the numbers of tokens in a Petrie Net, or marked directed graph. What are the simplest expressions of the firing rules?
.Close Flosets
.Open Formal Flow Diagrams
Informally a flow diagram is a collection of parts that have flows connecting them.
. Example Flow Diagram
Simple assembler program reads lines of source code lines and produces words of object code.
.DFD
Sample::=( Parts=>{Source, SASS, Object}, External_entities=>{Source,Object}, Flow=>{0,lines,words,lines+words}, lines+lines=lines, words+words=words,)
. Theory of Formal Flow Diagrams(FFDs)
FFD::=Net{
Parts::Sets.
|-(D0): $FLOW.
flows::Flow^(Parts>(Parts^2)= map p:Parts({(i,p) :Parts^2||flows(i,p)<>0}).
out_arc::Parts->(Parts^2)= map p({(p,o)||flows(p,o)<>0}).
effects::@(Parts,Parts)= {(o,i) :Parts^2||flow(o,i)<>0)}.
effected_by::= /effects.
|-$DIGRAPH(Nodes=>Parts, Arcs=>effects),
DIGRAPH::=http://www/dick/maths/math_22_graphs.html#DIGRAPH.
Now we have defined the directed graph associated with the flow
we can make a simplifying postulate.
|-(acyclic): loops=0.
The absence of loops is assumed without loss of generality, because if there is a need for a flow to return to a node then a new node with a single input and output is introduced to provide the feedback. In a hierarchical flow diagram a loop is placed within the refinement of the part.
sources::@Parts= {p:Parts||for no i:Parts(i effects p)}.
sinks::@Parts= {p:Parts||for no o:Parts(p effects o)}.
Again in realistic situations all the parts a connected up.
There shouldn't be any completely isolated Parts.
|-(no_isolates): no (sources & sinks).
The following are used to show the aggregate flow out of a part or set
of parts.
output::Parts->Flow= map [p](+{flow(a)||a:outarc(p)}),
output=(Parts->Flow);outarc;flow;+.
total_output::@Parts->Flow= map[P](+(output(P)).
The following are used to show the aggregate flow in to a part or set
of parts.
input::Parts->Flow= map [p](+{flow(a)||a:inarc(p)}),
total_input::@Parts->Flow= map [P](+(input(P)).
There is a way to document that some of the nodes are `outside the system`.
external_entities::@Parts.
An external entity can both send and receive flows.
entities::= source | sinks.
All sources and sinks should be external entities.
|-(ent0): entities ==> external_entities.
A `store` is a part that doesn't produces `more` than it is given.
stores::= {p:Parts~ external_entities || output(p) <= input(p)}.
Processes are nodes where `more`(>) comes out than comes in.
Thus they must change that which is flowing in the network.
processes::= Parts~ (stores | external_entities).
A `passive flow` is arc that has no process attached to it.
passive_flows::= {(p,q) :Parts^2||p effects q not (p in processes or q in processes)}.
(def)|-(pass0): passive_flows= effects~(Parts>stores,
However a store can absorb things and never output them.
Certain kinds of flow diagrams have the property that all their parts are conservative, this law (when it holds) is named in honor of Kirchoff.
Kirchoff_s_Law::@= (Parts=conservative_parts).
}=::FFD.
.Open N_Squared Charts
This is a particularly neat and simple way to display FFD's.
. Example of A Simple Assembler(SASS)
.As_is Table of parts
.As_is --------------
.As_is Source line
.As_is SASS word
.As_is Object
. Theory of N_Squared Charts
Uses FFD.
N::= |Parts|,
n::Parts---1..N,
table::1..N><1..N ->(Parts|Flows).
for p:Parts( table [ n(p),n(p) ] =p),
for p1,p2:Parts, f=flow(p1,p2) ( if n(p1) < n(p2) then table [ n(p1), n(p2) ] =f or if n(p1) > n(p2) then table [ n(p2), n(p1) ] =f)
.Close N_Squared
.Open Hierarchical FFDs
. Example Refined SASS
.As_is Context DFD
.As_is -----------
.As_is Source line
.As_is SASS word
.As_is Object
.As_is
.As_is SASS
.As_is -----------
.As_is Source lines lines
.As_is Pass1 label+address
.As_is Symbol address
.As_is label Pass2 word
.As_is Object
.Close Refinement
. Theory of Refinement
HIFFD::=Net{
Use FFD.
elements::@processes.
refined::= processes~ elements.
|- processes>=={refined, elements}.
The following uses recursion.
refinement::refined->$ $HIFFD.
|- refinement:processes(0..)-(1)$ $HIFFD.
for all p:refined (refinement(p) fits p).
For r:$ $FFD, p:Parts, (r fits p) ::@=
( r.external_entities=(r.Parts & Parts) and r.external_entities=(effects(p) |effected_by(p)) and for all i:effects(p)(r.output(i)=flows(i,p)) and for all o:effected_by(p)(r.input(o)=flows(p,o)))
}=::HIFFD.
.Close Formal Flow Diagrams
. Data Flow Diagrams
DFD::=Net{
Process,Entity,Store,Flow,Identifier::Finite_Sets.
Processes::= Process^PId, -- Parts of system which transform data.
Entities::= Entity^EId, -- Source or destination for data outside this system.
Stores::= Store^SId, -- parts of system which preserve data unchanged.
Flows::= Data^Fid.
Identifier::@#Char.
Identifier>=={NId, Fid}. Identifiers identify nodes or flows.
NId>=={PId, EId, SId}. Nodes are processes, entities, or stores.
DIGRAPH,
Nodes>=={ Processes, Entities, Stores }.
Arc_label::Arcs->Data.
for all (x,y) :Arcs(x in Processes or y in Processes ).
Either Gane_and_Sarson, SSADM, ... or Shlaer_and_Mellor.
if Gane_and_Sarson then PId=number #("." number) and Eid=lower_case_letter and SId="D" number #("." number) and Fid=NId "-" NId.
}=::DFD.