[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> math_23
[Contents] || [Source] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Apr 22 09:17:50 PDT 2005

Contents


    Flows and Flow Diagrams

      Flosets

        Introduction

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

        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.

        Theory

      1. 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(Set=>Flows, op=>+, u=>0).

          We require that there is at least one non-zero flow - ie at least two:

        1. |Flows|>1.

          We can recognise when one flow contains another. This can be modelled as a partially ordered set:

          poset(Set=>Flows, order=>(<=), inverse=>(>=), strict=>(<), strict_inverse=>(>)).

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

        2. 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: for all f1,f2 ( f1<f2 iff for some f3:Flows( f3<>0 and f1+f3=f2) ).


        3. |-for some f(f<>0) and for all f(0+f=f),
        4. |-for some f(f<>0 and 0+f=f),
        5. |-for some f(0<f),
        6. |-some Flows & />(0).

          Adding a flow to two flows preserves their order:

          for all f1,f2,f3, if f1<f2 then f1+f3<=f2+f3.


        7. |-for f1,f2, if f1<f2 then f1<>f2.
        8. |-0<=0. Consider{0+0=0}
        9. |-for all f:Flows (0<=f). Consider{f, |-0+f=f}


        10. |-for all f, f<>0(f>0).


        11. |-for all f1,f2:Flows, if f1<>0 then f1+f2<>0,
        12. Po{
          1. (1): f1,f2:Flows,
          2. (2): f1<>0,
          3. (3): f1+f2=0,
          4. (2) |- (4): f1>0,
          5. (3, 4, >) |- (5): f1+f2>0,
          6. |- (6): f1+f2>f2,
          7. (6, 3) |- (7): 0>f2,
          8. |- (8): 0=f2.
            }

        13. |-for all f1,f2, if f1+f2=0 then f1=0=f2.


        14. |-for no f (f<0),
        15. Po{
          1. (1): f<0,
          2. (1) |- (2): f<>0,
          3. (Monoid) |- (3): 0+f=f,
          4. (<) |- (4): 0<f,
          5. (trans <) |- (5): 0<0,
          6. (strict <) |- (6): 0<>0,
            }


        }=::FLOW.

      2. floset::=FLOW.
      3. |-for all POSITIVE_SEMIRING(Set,+.0,.,1,...) (FLOW(Set,+,0))
      4. [MATHS.41 Two Operators.semiring]

        Example Flows


      5. |-({0,1}, {(0,1)+>1, (1,1)+>1,...},0,{(0,0),(0,1),(1,1)})
      6. The above is half of a Boolean algebra.
      7. |-(Nat0,+,0) in floset.


      8. |-([0..),+,0) in floset.
      9. These are quantitative flows.
      10. |-For all S:Sets, (@S,|,{},==>) in floset.
      11. This is a qualitive flow.
      12. |-([0..1],max,0) in floset
      13. A Fuzzy flow.
      14. |-For all S:Sets, (F,+,0,<=):floset, (S->F, + , [s]0,<=) in floset.
      15. in this case (+)=[x,y:S->F]([s](x(s)+y(s))).

        For S:Sets,

      16. Bag(S)::=FLOW(S->Nat0,+, 0).
      17. FuzzySet(S)::=FLOW(S->[0..1], max, 0).

        Applications

        The following could be used in qualitative and quantitative Data Flow Diagrams


      18. |-For Data={Customer, Invoice, Invoice_item, Order, Order_item, ...}, ((@Data, |, {}) in FLOW ).


      19. |-For all Data:Finite_set,

      20. (Data->Nat0,+,0,<=) in floset. for all a,b:@Nat0^Data(a < b ::= for all i:Data (a[i] < b[i]) ).
      21. This is a quantitive model.

      22. (Data->@,|,{},==>) in floset.
      23. This is a qualitive model.

        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,

      24. |-qualify(S)={d:Data||S(d)>0}.

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


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

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

        In general:

      28. squash(n)::(S->Nat0)->(S->0..n) with addition redefined so that
      29. a*b=min{a+b,n}. is a homomorphism from a complex model to a simpler one.

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

        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 Diagram

          Informally a flow diagram is a collection of parts that have flows connecting them.

          .Example Simple assembler program reads lines of source code lines and produces words of object code.

        1. .DFD Sample::=( Parts=>{Source, SASS, Object},

        2. External_entities=>{Source,Object},
        3. Flow=>{0,lines,words,lines+words},
        4. lines+lines=lines,
        5. words+words=words, )

          .Theory

        6. FFD::=
          Net{
          1. Parts::Sets. FLOW.
          2. flows::Flow^(Parts><Parts).

          3. For f:Flows, p1,p2:Parts, f=flows(p1,p2)::= f flows from p1 to p2or`p1 sends f to p2 or p2 gets f from p1 or p1 gives f to p2 or p2 takes f from p1`.

          4. in_arc:: Parts->(Parts^2)= map p:Parts({(i,p) : Parts^2||flows(i,p)<>0}).
          5. out_arc::Parts->(Parts^2)= map p({(p,o)||flows(p,o)<>0}).

          6. effects::@(Parts,Parts)= {(o,i) : Parts^2||flow(o,i)<>0)}.
          7. effected_by::= /effects.

            DIGRAPH(Nodes=>Parts, Arcs=>effects). [ DIGRAPH in math_22_graphs ]

          8. (acyclic): loops=0.

            The abscence of loops is assumed without loss of generallity, 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 hierachical floww diagram a loop is placed within the refinement of the part.

          9. sources::@Parts= {p:Parts||for no i:Parts(i effects p)}.
          10. sinks::@Parts= {p:Parts||for no o:Parts(p effects o)}. There shouldn't be any completely isolated Parts.
          11. (no_isolates): no (sources & sinks).

          12. output::Parts->Flow= map p(+{flow(a)||a:outarc(p)}), output=(Parts->Flow);outarc;flow;+.
          13. total_output::@Parts->Flow= map[P](+(output(P)).

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

          16. external_entities::@Parts. There is a way to document that some of the nodes are outside the system.
          17. entities::= source | sinks.

          18. (ent0): entities ==> external_entities. An external entity can both send and receive flows. All sources and sinks should be external entities.

          19. stores::= {p:Parts~ external_entities || output(p) <= input(p)}. A store is a part that doesn't produces more than it is given.

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

            Processes are nodes where more(>) comes out than comes in. Thus they must change that which is flowing in the network.

          21. passive_flows::= {(p,q) : Parts^2||p effects q not (p in processes or q in processes)}
          22. |- (pass0): passive_flows=effects~ (Parts><processes | processes><Parts), In several methods passive flows are not permitted. If something flows then there is a process that moves it.

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

          24. conservative_parts::@Parts= {p||p.output=p.input},


          25. |- (stores_conserve): conservative_parts==>stores,
          26. Kirchoff_s_Law::@= (Parts=conservative_parts).


          }=::FFD.

          N_Squared

        7. Uses FFD.
        8. N::= |Parts|,
        9. n::Parts---1..N,

        10. table::1..N><1..N ->(Parts|Flows).

        11. for p:Parts( table [ n(p),n(p) ] =p),
        12. for p1,p2:Parts, f=flow(p1,p2) (
        13. if n(p1) < n(p2) then table [ n(p1), n(p2) ] =f
        14. or if n(p1) > n(p2) then table [ n(p2), n(p1) ] =f
        15. )

          Example of A Simple Assembler(SASS)

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

          Hierarchical FFDs

        16. HIFFD::=
          Net{

          1. Use FFD.
          2. elements::@processes.
          3. refined::= processes~ elements.
          4. |-processes>=={refined, elements}.

          5. refinement::refined->HIFFD.


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

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

          Example Refined SASS as N-squared

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

          
          
           SASS
           -----------
           Source   lines                   lines
                    Pass1   label+address
                                    Symbol  address
                                    label   Pass2   word
                                                    Object

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

        Data Flow Diagrams

      30. 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}. Identifers 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
        14. PId=number #("." number)
        15. and Eid=lower_case_letter
        16. and SId="D" number #("." number)

        17. 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_2_Proofs ] for more on the structure and rules.

        The notation also allows you to create a new network of variables and constraints, and give them a name. 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.

        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 complete listing of pages by topic see [ home.html ]

        End