[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci Dept] / [R J Botting] / [ MATHS ] / math_23_Flow_Diagrams
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Sep 18 15:18:19 PDT 2007

Contents

    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 ( [ Data Flow Diagrams ] ) are explained in terms of general hierarchical flow diagrams [ Hierarchical FFDs ] and these, in turn are defined in terms of [ Formal Flow Diagrams ] and (in turn) these depend on a novel kind of algebraic poset(Partially Ordered sets [ poset in math_21_Order ] ) that I call a [ Flosets ]

      Flosets

        Introduction to Flosets

         Here are some examples of the kinds of situations that the 'FLOW' model is intended to cover:

        Examples of Flows
      1. Numbers of objects in a part of system per unit time.
      2. Data Types being used in each part of a system.
      3. Frequencies with which something is done.
      4. Number of derivations of a string in a particular grammar.
      5. Types of objects flowing between classes in some software.

        Theory of Flows

      6. 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 [ Abelian_monoid in math_33_Monoids ]
        1. |- (F1): Abelian_monoid(Set=>Flows, op=>+, u=>0).
        2. (F1)|- (F1.1): for all f:Flows ( f+0 = 0 = 0 +f ),
        3. (F1)|- (F1.2): for all f1,f2:Flows(f1+f2=f2+f1).
        4. (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:

        5. |- (F2): |Flows|>1.

          We can recognize when one flow contains another. This can be modeled as a partially ordered set [ poset in math_21_Order ]

        6. |- (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 <:

        7. (F3)|- (trans <): for all x,y,z, if x<y<z then x<y.
        8. (F3)|- (strict <): for no x, x < x.

          A combined flow is greater than or equal to its parts:

        9. |- (F4): for all f1,f2:Flows( f1+f2>=f1,f2 ).

          One flow is greater than another if and only if the first results by adding a flow to the second one:

        10. |- (F5): for all f1,f2 ( f1<f2 iff for some f3:Flows( f3<>0 and f1+f3=f2) ).


        11. (F2, F1.1)|- (F6): for some f(f<>0) and for all f(0+f=f),
        12. (F6)|- (F7): for some f(f<>0 and 0+f=f),
        13. (F7, F4, F5)|- (F8): for some f(0<f),
        14. (F8)|- (F9): some Flows & />(0).

          Adding a flow to two flows preserves their order:

        15. |- (F10): for all f1,f2,f3, if f1<f2 then f1+f3<=f2+f3.
        16. In other words (+) is monotonic.


        17. (above)|- (F11): for f1,f2, if f1<f2 then f1<>f2.
        18. (above)|- (F12): 0<=0.
        19. Consider{0+0=0}
        20. (above)|- (F13): for all f:Flows (0<=f).
          Consider{f,|-0+f=f}
        21. (above)|- (F14): for all f, f<>0(f>0).


        22. (above)|- (F15): for all f1,f2:Flows, if f1<>0 then f1+f2<>0,
        23. (above)|- (F16): for all f1,f2, if f1+f2=0 then f1=0=f2.
        24. (above)|- (F17): for no f (f<0),

          Proof of F15
          Let

          1. |- (F15.1): f1,f2:Flows,
          2. |- (F15.2): f1<>0,
          3. |- (F15.3): f1+f2=0,
          4. (F15.2)|- (F15.4): f1>0,
          5. (F15.3, F15.4, >)|- (F15.5): f1+f2>0,
          6. (above)|- (F15.6): f1+f2>f2,
          7. (F15.6, F15.3)|- (F15.7): 0>f2,
          8. (above)|- (F15.8): 0=f2.

          (Close Let )

          Proof of F17
        25. Po{

          1. |- (F17.1): f<0,
          2. (F17.1)|- (F17.2): f<>0,
          3. (Monoid)|- (F17.3): 0+f=f,
          4. (<)|- (F17.4): 0<f,
          5. (trans <)|- (F17.5): 0<0,
          6. (strict <)|- (F17.6): 0<>0,
            }


        }=::FLOW.

      7. floset::=$ FLOW.
      8. (def)|-for all POSITIVE_SEMIRING(Set,+.0,.,1,...) (FLOW(Set,+,0))
      9. [MATHS.41 Two Operators.semiring]

        Example Flows


      10. (def)|-({0,1}, {(0,1)+>1, (1,1)+>1,...},0,{(0,0),(0,1),(1,1)}) in floset.
      11. The above is half of a Boolean algebra.
      12. (def)|-(Nat0,+,0) in floset.
      13. (def)|-([0..),+,0) in floset.
      14. These are quantitative flows.
      15. (def)|-For all S:Sets, (@S,|,{},==>) in floset.
      16. This is a qualitive flow.
      17. (def)|-(0.0..1.0, max,0) in floset
      18. A Fuzzy flow.
      19. (def)|-For all S:Sets, (F,+,0,<=) :floset, (S->F, + , [s]0,<=) in floset.
      20. In this case (+)=[x,y:S->F]([s](x(s)+y(s))).

      21. For S:Sets, Bag(S)::=$ FLOW(S->Nat0,+, 0).
      22. 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:
      23. |-For Data={Customer, Invoice, Invoice_item, Order, Order_item, ...}, ((@Data, |, {}) in $ FLOW ). Or equivalently the following model forms a qualitative flow:
      24. (Data->@,|,{},==>) in floset.

        However:

      25. (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

      26. qualify::(Data->Nat0)->(@Data)=map[S]0./S,
      27. (above)|-qualify(S)={d:Data||S(d)>0}.

        The following example, could be part of a model of Ozone depletion:


      28. |-For Parts:={Ground, Lower_atmosphere, Upper_atmosphere, ...},
      29. 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:

      30. |-For Frequencies:=Nat0, ((Frequencies, +, 0) in $ FLOW ).

        In general:

      31. squash(n)::(S->Nat0)->(S->0..n) with addition redefined so that
      32. 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?

      . . . . . . . . . ( end of section Flosets) <<Contents | End>>

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

      2. FFD::=
        Net{
        1. Parts::Sets.
        2. |- (D0): FLOW.
        3. flows::Flow^(Parts><Parts).

        4. For f:Flows, p1,p2:Parts, (f=flows(p1, p2)) ::= f flows from p1 to p2.
        5. |-For f, p1,p2, (f=flows(p1,p2))= p1 sends f to p2 = p2 gets f from p1 = p1 gives f to p2 = p2 takes f from p1.

          A set of flows between pairs of objects defines a directed graph where each arc indicates a non-zero flow.

        6. in_arc:: Parts->(Parts^2)= map p:Parts({(i,p) :Parts^2||flows(i,p)<>0}).
        7. out_arc::Parts->(Parts^2)= map p({(p,o)||flows(p,o)<>0}).
        8. effects::@(Parts,Parts)= {(o,i) :Parts^2||flow(o,i)<>0)}.
        9. effected_by::= /effects.


        10. |-DIGRAPH(Nodes=>Parts, Arcs=>effects),
        11. DIGRAPH::= See http://csci.csusb.edu/dick/maths/math_22_graphs.html#DIGRAPH.

          Now we have defined the directed graph associated with the flow we can make a simplifying postulate.

        12. |- (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.

        13. sources::@Parts= {p:Parts||for no i:Parts(i effects p)}.
        14. 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.

        15. |- (no_isolates): no (sources & sinks).

          The following are used to show the aggregate flow out of a part or set of parts.

        16. output::Parts->Flow= map [p](+{flow(a)||a:outarc(p)}), output=(Parts->Flow);outarc;flow;+.
        17. 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.

        18. input::Parts->Flow= map [p](+{flow(a)||a:inarc(p)}),
        19. total_input::@Parts->Flow= map [P](+(input(P)).

          There is a way to document that some of the nodes are outside the system.

        20. external_entities::@Parts.

          An external entity can both send and receive flows.

        21. entities::= source | sinks.

          All sources and sinks should be external entities.

        22. |- (ent0): entities ==> external_entities.

          A store is a part that doesn't produces more than it is given.

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

        24. processes::= Parts~ (stores | external_entities).

          A passive flow is arc that has no process attached to it.

        25. passive_flows::= {(p,q) :Parts^2||p effects q not (p in processes or q in processes)}.
        26. (def)|- (pass0): passive_flows= effects~(Parts><processes | processes><Parts),
        27. In several structured analysis and design methods passive flows are not permitted because if something flows then there needs to be a process that moves it.
        28. no_passive_flows::@=(passive_flows={}).

          A filter is a common kind of process with a single input and a single output.

        29. filters::= {p:parts|| one(in_arc(p)) and one(out_arc(p))}.

          A conservative part outputs no more or less than what it inputs.

        30. conservative_parts::@Parts= {p||p.output=p.input},
        31. (def)|- (stores_conserve): conservative_parts==>stores,
        32. 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.

        33. Kirchoff_s_Law::@= (Parts=conservative_parts).


        }=::FFD.

        N_Squared Charts

          This is a particularly neat and simple way to display FFD's.

          Example of A Simple Assembler(SASS)

           
           Table of parts
           --------------
           Source	line
           		SASS	word
           				Object

          Theory of N_Squared Charts
        1. Uses FFD.
        2. N::= |Parts|,
        3. n::Parts---1..N,
        4. table::1..N><1..N ->(Parts|Flows).

        5. for p:Parts( table [ n(p),n(p) ] =p),
        6. 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)

        . . . . . . . . . ( end of section N_Squared) <<Contents | End>>

        Hierarchical FFDs

          Example Refined SASS

           
           Context DFD
           -----------
           Source	line
           		SASS	word
           				Object
          

           SASS
          

           -----------
          

           Source	lines				lines
          

           		Pass1	label+address
          

           				Symbol		address
          

           				label		Pass2	word
          

           							Object
          

        . . . . . . . . . ( end of section Refinement)  <<Contents | End>>

        Theory of Refinement
        

      3. HIFFD::= 
        Net{
          

        1. Use FFD.

        2. elements::@processes.

        3. refined::=  processes~ elements.

        4. |-processes>=={refined, elements}.

          
The following uses recursion.

        5. refinement::refined->$ HIFFD.

          

        6. |-refinement:processes(0..)-(1)$ HIFFD.

        7. for all p:refined (refinement(p) fits p).

          

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

        

      . . . . . . . . . ( end of section Formal Flow Diagrams)  <<Contents | End>>

      Data Flow Diagrams
      

      

    1. DFD::= 
      Net{
        
Process,Entity,Store,Flow,Identifier::Finite_Sets.

      1. Processes::=  Process^PId,  -- Parts of system which transform data.

      2. Entities::=  Entity^EId,  -- Source or destination for data outside this system.

      3. Stores::=  Store^SId,  -- parts of system which preserve data unchanged.

      4. Flows::=  Data^Fid.

        

      5. Identifier::@#Char.

      6. Identifier>=={NId, Fid}.  Identifiers identify nodes or flows.

      7. NId>=={PId, EId, SId}.    Nodes are processes, entities, or stores.

        

      8. DIGRAPH,

      9. Nodes>=={ Processes, Entities, Stores }.

      10. Arc_label::Arcs->Data.

      11. for all (x,y) :Arcs(x in Processes  or y in Processes ).

        

      12. Either Gane_and_Sarson, SSADM, ... or Shlaer_and_Mellor.

        

      13. if  Gane_and_Sarson then PId=number #("." number) and Eid=lower_case_letter and SId="D" number #("." number) and Fid=NId "-" NId.


      }=::DFD.
      

      

      Notes on MATHS Notation
      
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.

      
Proofs follow a natural deduction style that start with
assumptions ("Let") and continue to a consequence ("Close Let")
and then discard the assumptions and deduce a conclusion. Look
here
[ Block Structure in logic_25_Proofs ]
for more on the structure and rules.

      
The notation also allows you to create a new network of variables
and constraints. A "Net" has a number  of variables (including none) and
a number of properties (including none) that connect variables.
You can give them a name and then reuse them.  The schema, formal system,
or an elementary piece of documentation starts with "Net" and finishes "End of Net".
For more, see
[ notn_13_Docn_Syntax.html ]
for these ways of defining and reusing pieces of logic and algebra
in your documents.  A quick example: a circle = Net{radius:Positive Real, center:Point}.

      
For a complete listing of pages in  this part of my site by topic see
[ home.html ]

      

      Notes on the Underlying Logic of MATHS
      
The notation used here is a formal language with syntax
and a semantics described using traditional formal logic
[ logic_0_Intro.html ]
plus sets, functions, relations, and other mathematical extensions.

      
For a more rigorous description of the standard notations
see

    2. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

      Glossary
      

    3. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements.
The previous and previous but one statments are shown as (-1) and (-2).

    4. given::reason="I've been told that...", used to describe a problem.

    5. given::variable="I'll be given a value or object like this...", used to describe a problem.

    6. goal::theorem="The result I'm trying to prove right now".

    7. goal::variable="The value or object I'm trying to find or construct".

    8. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.

    9. hyp::reason="I assumed this in my last Let/Case/Po/...".

    10. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

    11. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

    12. RAA::conclusion="Reducto Ad Absurdum".  This allows you to discard the last
assumption (let) that you introduced.

      

    

    End