module DCM_asyn (TYPES, CHANNELS, MS) is

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

process DCM [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gDMin, gDMout: IOChannel, gEvent: EventChannel] (Id: Nat3) is
   alt
      DCM_Manager [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, true)
   []
      DCM_Manager [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, false)
   end alt
end process

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

process DCM_Manager [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gDMin, gDMout: IOChannel, gEvent: EventChannel]
        (Id: Nat3, UrlCapable: bool) is
   downDM [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, UrlCapable)
end process

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

process downDM [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gDMin, gDMout: IOChannel, gEvent: EventChannel]
        (Id: Nat3, UrlCapable: bool) is
   gUpDown (Id, power_change);
   leDM [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, UrlCapable)
end process

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

process leDM [gInfo: InfoChannel, gUpDown: UpDownChannel,
        gDMin, gDMout: IOChannel, gEvent: EventChannel]
        (Id: Nat3, UrlCapable: bool) is
   disrupt
      var net: Network in
         net := any Network;
         gInfo (Id, GUID_list, net);
         if i_leader (net) == Id then
            gEvent (init_leader, Id);
            ilDM [gDMin, gDMout, gEvent] (Id, UrlCapable,
                                          init_hosts (net), nr_uphosts (net))
         else
            ifDM [gDMin, gDMout, gEvent] (Id, UrlCapable, i_leader (net))
         end if
      end var
   by
      alt
         gInfo (Id, bus_reset_event);
         gDMout (Id, empty);
         leDM [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, UrlCapable)
      []
         gUpDown (Id, power_change);
         downDM [gInfo, gUpDown, gDMin, gDMout, gEvent] (Id, UrlCapable)
      end alt
   end disrupt
end process

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

process ifDM [gDMin, gDMout: IOChannel, gEvent: EventChannel] (Id: Nat3,
        UrlCapable: bool, leader: Nat3) is
   var j: Nat3, b: bool in
      disrupt
         -- process DeclareCapability in the LOTOS specification
         loop
            alt
               gDMout (leader, consm (DMInitRequest, Id, UrlCapable))
            []
               j := any Nat3;
               b := any bool;
               gDMin (Id, consm (DMInitRequest, j, b))
            end alt
         end loop
      by
         j := any Nat3;
         b := any bool;
         gDMin (Id, consm (DMInitReply, j, b));
         if j == Id then
            gEvent (final_leader, Id, UrlCapable)
         end if;
         -- processes ffDM and flDM in the LOTOS specification
         loop
            gDMin (Id, ?any MesFrame)
         end loop
      end disrupt
   end var
end process

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

process ilDM [gDMin, gDMout: IOChannel, gEvent: EventChannel] (Id: Nat3,
        UrlCapable: bool, in var hosts: Hosts, in var nr: Nat3) is
   assert nr > 0;
   if nr == 1 then
      nr := f_leader (Id, chge_rec (Id, UrlCapable, hosts));
      DeclareLeader [gDMin, gDMout, gEvent] (Id, UrlCapable, hosts, nr)
   else
      -- assert nr > 1
      var m: Message2, j: Nat3, b: bool in
         m := any Message2;
         j := any Nat3;
         b := any bool;
         gDMin (Id, consm (m, j, b));
         if (m == DMInitRequest) and (not (rec (j, hosts))) then
            hosts := chge_rec (j, b, hosts);
            nr := nr - 1
         end if;
         ilDM [gDMin, gDMout, gEvent] (Id, UrlCapable, hosts, nr)
      end var
   end if
end process

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

process DeclareLeader [gDMin, gDMout: IOChannel, gEvent: EventChannel]
        (Id: Nat3, UrlCapable: bool, hosts: hosts, leader: Nat3) is
   if hosts == nil then
      if leader == Id then
         gEvent (final_leader, Id, UrlCapable)
      else
         gDMout (leader, consm (DMInitReply, leader, false))
      end if;
      -- processes ffiDM and fliDM in the LOTOS specification
      var m: Message2, j: Nat3, b: bool in
         loop
            m := any Message2;
            j := any Nat3;
            b := any bool;
            gDMin (Id, consm (m, j, b));
            if m == DMInitRequest then
               gDMout (j, consm (DMInitReply, leader, false))
            end if
         end loop
      end var
   else
      if (head (hosts).Id <> Id) and (head (hosts).Id <> leader) then
         gDMout (head (hosts).Id, consm (DMInitReply, leader, false))
      end if;
      DeclareLeader [gDMin, gDMout, gEvent] (Id, UrlCapable,
                                             tail (hosts), leader)
   end if
end process

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

end module