module CMM (TYPES, CHANNELS, BUS) is

-------------------------------------------------------------------------------

process CMM [gInfo: InfoChannel, gUpDown: UpDownChannel,
             gBusReset: BusResetChannel] (Id: Nat3) is
   CMMDown [gInfo, gUpDown, gBusReset] (Id)
end process

-------------------------------------------------------------------------------

process CMMDown [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gBusReset: BusResetChannel] (Id: Nat3) is
   disrupt
      FlushBusReset [gBusReset]
   by
      gUpDown (Id, power_change);
      var net: Network in
         net := any Network;
         gBusReset (bus_reset_end, net);
         CMMUp [gInfo, gUpDown, gBusReset] (Id, net)
      end var
   end disrupt
end process

-------------------------------------------------------------------------------

process CMMUp [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gBusReset: BusResetChannel] (Id: Nat3, net: Network) is
   disrupt
      CMMReady [gInfo, gBusReset] (Id, net)
   by
      gUpDown (Id, power_change);
      CMMDown [gInfo, gUpDown, gBusReset] (Id)
   end disrupt
end process

-------------------------------------------------------------------------------

process CMMReady [gInfo: InfoChannel, gBusReset: BusResetChannel]
        (Id: Nat3, net: Network) is
   alt
      gInfo (Id, GUID_list, net);
      CMMReady [gInfo, gBusReset] (Id, net)
   []
      gBusReset (bus_reset_start);
      CMMDeliver [gInfo, gBusReset] (Id)
   end alt
end process

-------------------------------------------------------------------------------

process CMMDeliver [gInfo: InfoChannel, gBusReset: BusResetChannel]
        (Id: Nat3) is
   var net: Network in
      alt
         gInfo (Id, bus_reset_event);
         net := any Network;
         gBusReset (bus_reset_end, net);
         CMMReady [gInfo, gBusReset] (Id, net)
      [] 
         net := any Network;
         gBusReset (bus_reset_end, net);
         CMMDeliver2 [gInfo, gBusReset] (Id, net) 
      end alt
   end var
end process

-------------------------------------------------------------------------------

process CMMDeliver2 [gInfo: InfoChannel, gBusReset: BusResetChannel]
        (Id: Nat3, net: Network) is
    alt
       gInfo (Id, GUID_list, net);
       CMMDeliver2 [gInfo, gBusReset] (Id, net)
    []
       gInfo (Id, bus_reset_event);
       CMMReady [gInfo, gBusReset] (Id, net)
    []
       gBusReset (bus_reset_start);
       CMMDeliver [gInfo, gBusReset] (Id)
    end alt
end process

-------------------------------------------------------------------------------

end module