process CMM[ gInfo, gUpDown, gBusReset ]
        ( Id: Nat ) 
  : noexit :=

  CMMDown[gInfo,gUpDown,gBusReset](Id)

where

  process CMMDown[ gInfo, gUpDown, gBusReset ]
          ( Id: Nat ) 
    : noexit :=

    FlushBusReset[gBusReset]
    [> ( gUpDown ! Id ! power_change
         ; ( choice b1,b2:Bool
             [] gBusReset ! bus_reset_end ! consnet(consn(b1),consn(b2))
             ; CMMUp[gInfo,gUpDown,gBusReset]
               (Id,consnet(consn(b1),consn(b2))) ) )
  endproc (* CMMDown *)

  process CMMUp[ gInfo, gUpDown, gBusReset ]
          ( Id: Nat , net: Network ) 
    : noexit :=

    CMMReady[gInfo,gUpDown,gBusReset](Id,net)
    [> ( gUpDown ! Id ! power_change
         ; CMMDown[gInfo,gUpDown,gBusReset](Id) )

  where
    process CMMReady[ gInfo, gUpDown, gBusReset ]
          ( Id: Nat , net: Network )
    : noexit :=

    ( gInfo ! Id ! GUID_list ! net
      ; CMMReady[gInfo,gUpDown,gBusReset](Id,net) )
    []
    ( gBusReset ! bus_reset_start
      ; CMMDeliver[gInfo,gUpDown,gBusReset](Id) )

    endproc (* CMMReady *)

    process CMMDeliver[ gInfo, gUpDown, gBusReset ]
          ( Id: Nat )
    : noexit :=

    ( gInfo ! Id ! bus_reset_event
      ; ( choice b1,b2:Bool
          [] (gBusReset ! bus_reset_end ! consnet(consn(b1),consn(b2))
              ; CMMReady[gInfo,gUpDown,gBusReset]
                (Id,consnet(consn(b1),consn(b2))))))
    []
    ( choice b1,b2:Bool
             [] (gBusReset ! bus_reset_end ! consnet(consn(b1),consn(b2))
                 ; CMMDeliver2 [gInfo,gUpDown,gBusReset]
                   (Id,consnet(consn(b1),consn(b2))) 
                )
    )
    endproc (* CMMDeliver *)

    process CMMDeliver2[ gInfo, gUpDown, gBusReset ]
          ( Id: Nat , net: Network )
    : noexit :=

    ( gInfo ! Id ! GUID_list ! net
      ; CMMDeliver2[gInfo,gUpDown,gBusReset] (Id,net) )
    []
    ( gInfo ! Id ! bus_reset_event
      ; CMMReady[gInfo,gUpDown,gBusReset] (Id,net) )
    []
    ( gBusReset ! bus_reset_start
      ; CMMDeliver[gInfo,gUpDown,gBusReset](Id) )
    endproc (* CMMDeliver2 *)

  endproc (* CMMUp *)

endproc (* CMM *)