process DCM_Manager[ gInfo, gUpDown, gDM, gEvent ]
        ( Id: Nat , UrlCapable: Bool ) 
  : noexit :=

  downDM[gInfo,gUpDown,gDM,gEvent](Id,UrlCapable)

  where

    process downDM[ gInfo, gUpDown, gDM, gEvent ]
            ( Id: Nat , UrlCapable: Bool )
      : noexit :=

      stop
      [> (gUpDown! Id ! power_change		(* Disrupt !! *)
          ; leDM[gInfo,gUpDown,gDM,gEvent]
            (Id,UrlCapable) )

    endproc (* downDM *)

    process leDM[ gInfo, gUpDown, gDM, gEvent ]
            ( Id: Nat , UrlCapable: Bool )
      : noexit :=

      ( choice b1,b2:Bool
        [] let net:Network=consnet(consn(b1),consn(b2))
           in ( gInfo ! Id ! GUID_list ! net
                ; ( [i_leader(net)==Id]
                      -> gEvent ! init_leader ! Id
                         ; ilDM[gDM,gEvent](Id,UrlCapable,net)
                   []
                    [i_leader(net)<>Id]
                      -> ifDM[gDM,gEvent]
                         (Id,UrlCapable,net,i_leader(net))
                  )
              )
      )
      [> ( ( gInfo ! Id ! bus_reset_event		(* Disrupt !! *)
             ; leDM[gInfo,gUpDown,gDM,gEvent](Id,UrlCapable))
           []
           ( gUpDown ! Id ! power_change
             ; downDM[gInfo,gUpDown,gDM,gEvent](Id,UrlCapable))
         )
    endproc (* leDM *)

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

      DeclareCapability[ gDM, gEvent](Id,UrlCapable,leader)

      [> ( gDM ! Id ! leader ! DMInitReply ? j:Nat[j<>0]
           ; ( [j==Id]
                 -> ( gEvent ! final_leader ! Id ! UrlCapable
                      ; flDM[gDM,gEvent](Id,UrlCapable,net) )
               []
               [j<>Id]
                 -> ffDM[gDM,gEvent](Id,UrlCapable,net,j)
             )
         )

      where
        process DeclareCapability[ gDM, gEvent ]
                ( Id:Nat , UrlCapable: Bool , leader: Nat )
        : noexit :=

          ( gDM ! leader ! Id ! DMInitRequest ! UrlCapable
            ; DeclareCapability[gDM,gEvent](Id,UrlCapable,leader))
          []
          ( gDM ! Id ? k:Nat ! DMInitRequest ? b:Bool
            [(k<>Id) and (k<>0)]
            ; DeclareCapability[gDM,gEvent](Id,UrlCapable,leader))

        endproc (* DeclareCapability *)
    endproc (* ifDM *)

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

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

      where
        process Elect[ gDM, gEvent ]
                ( Id: Nat , UrlCapable: Bool , net: Network ,
                  hosts: Hosts, nr: Nat)
          : noexit :=
            ([nr==1]
              -> DeclareLeader[gDM,gEvent]
                 (Id,UrlCapable,net,hosts,f_leader(Id,chge_rec(Id,UrlCapable,hosts))))
            []
            ([nr>1]
              -> ( gDM ! Id ? j:Nat ! DMInitRequest ? b:Bool
                   [(j<>Id) and (j<>0)]
                   ; ( [not(rec(j,hosts))]
                         -> Elect[gDM,gEvent]
                            (Id,UrlCapable,net,chge_rec(j,b,hosts),nr-1)
                     []
                       [rec(j,hosts)]
                         -> Elect[gDM,gEvent]
                            (Id,UrlCapable,net,hosts,nr)
                     )
                 )
            )
            []
            ( gDM ! Id ? k:Nat ! DMInitReply ? l:Nat 
              [(k<>Id) and (k<>0) and (l<>0)]
              ; Elect[gDM,gEvent] (Id,UrlCapable,net,hosts,nr))
        endproc (* Elect *)

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

    endproc (* ilDM *)

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

        ( gDM ! Id ? k:Nat ! DMInitRequest ? b:Bool
          [(k<>Id) and (k<>0)]
          ; ffDM[gDM,gEvent] (Id,UrlCapable,net,leader))
        []
        ( gDM ! Id ? k:Nat ! DMInitReply ? l:Nat 
          [(k<>Id) and (k<>0) and (l<>0)]
          ; ffDM[gDM,gEvent] (Id,UrlCapable,net,leader))

    endproc (* flDM *)

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

        ( gDM ! Id ? j:Nat ! DMInitRequest ? b:Bool
          [j<>Id and (j<>0)]
          ; ( gDM ! j ! Id ! DMInitReply ! leader
              ; ffiDM[gDM,gEvent] (Id,UrlCapable,net,leader)))
        []
        ( gDM ! Id ? k:Nat ! DMInitReply ? l:Nat 
          [(k<>Id) and (k<>0) and (l<>0)]
          ; ffiDM[gDM,gEvent] (Id,UrlCapable,net,leader))

    endproc (* ffiDM *)

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

        ( gDM ! Id ? k:Nat ! DMInitRequest ? b:Bool
          [(k<>Id) and (k<>0)]
          ; flDM[gDM,gEvent] (Id,UrlCapable,net))
        []
        ( gDM ! Id ? k:Nat ! DMInitReply ? l:Nat 
          [(k<>Id) and (k<>0) and (l<>0)]
          ; flDM[gDM,gEvent] (Id,UrlCapable,net))

    endproc (* flDM *)

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

        ( gDM ! Id ? j:Nat ! DMInitRequest ? b:Bool
          [j<>Id and(j<>0)]
           ; ( gDM ! j !Id ! DMInitReply ! Id
               ; fliDM[gDM,gEvent] (Id,UrlCapable,net)))
        []
        ( gDM ! Id ? k:Nat ! DMInitReply ? l:Nat 
          [(k<>Id) and (k<>0) and (l<>0)]
          ; fliDM[gDM,gEvent] (Id,UrlCapable,net))

    endproc (* fliDM *)

endproc (* DCM_Manager *)

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