process DCM_Manager[ ginfo, gUpDown, gDMin, gDMout, gEvent ]
        ( Id: Nat , UrlCapable: Bool ) 

  : noexit :=

  downDM[ginfo,gUpDown,gDMin,gDMout,gEvent](Id,UrlCapable)

  where

    process downDM[ ginfo, gUpDown, gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool )
      : noexit :=

      stop
      [> (gUpDown! Id ! power_change		(* Disrupt !! *)
          ; leDM[ginfo,gUpDown,gDMin,gDMout,gEvent]
            (Id,UrlCapable) )

    endproc (* downDM *)

    process leDM[ ginfo, gUpDown, gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool )
      : noexit :=

      ( choice b1,b2:Bool 
        [] gInfo ! Id ! GUID_list ! consnet(consn(b1),consn(b2))
           ; ( [i_leader(consnet(consn(b1),consn(b2)))==Id]
                 -> gEvent ! init_leader ! Id
                    ; ilDM[gDMin,gDMout,gEvent]
                      (Id,UrlCapable,consnet(consn(b1),consn(b2)))
               []
               [i_leader(consnet(consn(b1),consn(b2)))<>Id]
                 -> ifDM[gDMin,gDMout,gEvent]
                    (Id,UrlCapable,consnet(consn(b1),consn(b2)),
                     i_leader(consnet(consn(b1),consn(b2))))
           )
      )
      [> ( ( gInfo ! Id ! bus_reset_event		(* Disrupt !! *)
             ; ( gDMout ! Id ! empty
                 ; leDM[ginfo,gUpDown,gDMin,gDMout,gEvent](Id,UrlCapable))
               []
               ( gUpDown ! Id ! power_change
                 ; downDM[ginfo,gUpDown,gDMin,gDMout,gEvent](Id,UrlCapable))
           )
           []
           ( gUpDown ! Id ! power_change
             ; downDM[ginfo,gUpDown,gDMin,gDMout,gEvent](Id,UrlCapable))
         )
    endproc (* leDM *)

    process ifDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network , leader: Nat )
      : noexit :=

      DeclareCapability[ gDMin, gDMout, gEvent](Id,UrlCapable,leader)

      [> ( choice j:Nat, b:Bool
           [] gDMin ! Id ! consm(DMInitReply,j,b)
              ; ( [j==Id]
                    -> gEvent ! final_leader ! Id ! UrlCapable
                       ; flDM[gDMin,gDMout,gEvent]
                          (Id,UrlCapable,net)
                  []
                  [j<>Id]
                    -> ffDM[gDMin,gDMout,gEvent]
                           (Id,UrlCapable,net,j)
             )
          )

      where
        process DeclareCapability[ gDMin, gDMout, gEvent ]
                ( Id:Nat , UrlCapable: Bool , leader: Nat )
        : noexit :=
          (gDMout ! leader ! consm(DMInitRequest,Id,UrlCapable)
           ; DeclareCapability[gDMin,gDMout,gEvent](Id,UrlCapable,leader))
          []
          (choice j:Nat, b:Bool
           [] gDMin ! Id ! consm(DMInitRequest,j,b)
              ; DeclareCapability[gDMin,gDMout,gEvent](Id,UrlCapable,leader))
        
        endproc (* DeclareCapability *)
    endproc (* ifDM *)

    process ilDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network )
      : noexit :=

      Elect[gDMin,gDMout,gEvent]
           (Id,UrlCapable,net,init_hosts(net),nr_uphosts(net))

      where
        process Elect[ gDMin, gDMout, gEvent ]
                ( Id: Nat , UrlCapable: Bool , net: Network ,
                  hosts: Hosts, nr: Nat)
          : noexit :=
            ([nr==1]
              -> DeclareLeader[gDMin,gDMout,gEvent]
                 (Id,UrlCapable,net,hosts,f_leader(Id,chge_rec(Id,UrlCapable,hosts))))
            []
            ([nr>1]
              -> ( choice m:Message2,j:Nat,b:Bool
                   [] gDMin ! Id ! consm(m,j,b)
                   ; ( ([m==DMInitRequest and not(rec(j,hosts))]
                       -> Elect[gDMin,gDMout,gEvent]
                          (Id,UrlCapable,net,chge_rec(j,b,hosts),nr-1))
                       []
                       ([m<>DMInitRequest or rec(j,hosts)]
                       -> Elect[gDMin,gDMout,gEvent]
                          (Id,UrlCapable,net,hosts,nr))
                     )
                 ))
        endproc (* Elect *)

        process DeclareLeader[ gDMin, gDMout, gEvent ]
                ( Id: Nat , UrlCapable: Bool , net: Network ,
                  hosts: hosts , leader: Nat )
          : noexit :=
            ([hosts==emptyh]
              -> ( [leader==Id]
                     -> (gEvent ! final_leader ! Id ! UrlCapable
                         ; fliDM[gDMin,gDMout,gEvent]
                           (Id,UrlCapable,net))
                   []
                   [leader<>Id]
                     -> (gDMout ! leader ! consm(DMInitReply,leader,false)
                         ; ffiDM[gDMin,gDMout,gEvent]
                           (Id,UrlCapable,net,leader))
                 ))
            []
            ([hosts<>emptyh] -> [(id(headh(hosts))==Id)or(id(headh(hosts))==leader)]
              -> DeclareLeader[gDMin,gDMout,gEvent]
                 (Id,UrlCapable,net,tailh(hosts),leader))
            []
            ([hosts<>emptyh] -> [(id(headh(hosts))<>Id)and(id(headh(hosts))<>leader)]
              -> (gDMout ! id(headh(hosts)) ! consm(DMInitReply,leader,false)
                 ; DeclareLeader[gDMin,gDMout,gEvent]
                   (Id,UrlCapable,net,tailh(hosts),leader)))
        endproc (* DeclareLeader *)

    endproc (* ilDM *)

    process ffDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network , leader: Nat )
      : noexit :=

        choice m:Message2,j:Nat,b:Bool
        [] gDMin ! Id ! consm(m,j,b)
           ; ffDM[gDMin,gDMout,gEvent] (Id,UrlCapable,net,leader)

    endproc (* flDM *)

    process ffiDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network , leader: Nat )
      : noexit :=

      ( choice m:Message2,j:Nat,b:Bool
        [] gDMin ! Id ! consm(m,j,b)
           ; ( ([m==DMInitRequest]
                -> (gDMout ! j ! consm(DMInitReply,leader,false)
                    ; ffiDM[gDMin,gDMout,gEvent]
                      (Id,UrlCapable,net,leader)))
             []
               ([m<>DMInitRequest]
                -> ffiDM[gDMin,gDMout,gEvent]
                   (Id,UrlCapable,net,leader))
             )
      )

    endproc (* ffiDM *)

    process flDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network )
      : noexit :=

        choice m:Message2,j:Nat,b:Bool
        [] gDMin ! Id ! consm(m,j,b)
           ; flDM[gDMin,gDMout,gEvent] (Id,UrlCapable,net)

    endproc (* flDM *)

    process fliDM[ gDMin, gDMout, gEvent ]
            ( Id: Nat , UrlCapable: Bool , net: Network )
      : noexit :=

      ( choice m:Message2,j:Nat,b:Bool
        [] gDMin ! Id ! consm(m,j,b)
           ; ( ([m==DMInitRequest]
                -> (gDMout ! j ! consm(DMInitReply,Id,false)
                    ; fliDM[gDMin,gDMout,gEvent]
                      (Id,UrlCapable,net)))
             []
               ([m<>DMInitRequest]
                -> fliDM[gDMin,gDMout,gEvent]
                   (Id,UrlCapable,net))
             )
      )

    endproc (* fliDM *)

endproc (* DCM_Manager *)

process DCM [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id : Nat) : noexit :=
   DCM_Manager [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, true)
   []
   DCM_Manager [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, false)
endproc (* DCM *)