module DCM_sync (TYPES, CHANNELS) is

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

channel DMChannel is
   (Id1: Nat3, Id2: Nat3, m: Message2, b: bool),
   (Id1: Nat3, Id2: Nat3, m: Message2, n: Nat3)
end channel

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

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

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

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

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

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

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

process leDM [gInfo: InfoChannel, gUpDown: UpDownChannel, gDM: DMChannel,
        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 [gDM, gEvent] (Id, UrlCapable, init_hosts (net),
                                nr_uphosts (net))
         else
            ifDM [gDM, gEvent] (Id, UrlCapable, i_leader (net))
         end if
      end var
   by
      alt
         gInfo (Id, bus_reset_event);
         leDM [gInfo, gUpDown, gDM, gEvent] (Id, UrlCapable)
      []
         gUpDown (Id, power_change);
         downDM [gInfo, gUpDown, gDM, gEvent] (Id, UrlCapable)
      end alt
   end disrupt
end process

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

process ifDM [gDM: DMChannel, gEvent: EventChannel] (Id: Nat3,
        UrlCapable: bool, leader: Nat3) is
   var j: Nat3 in
      disrupt
         -- process DeclareCapability in the LOTOS specification
         loop
            alt
               gDM (leader, Id, DMInitRequest, UrlCapable)
            []
               gDM (Id, ?j, DMInitRequest, ?any bool)
                  where (j <> Id) and (j <> 0)
            end alt
         end loop
      by
         gDM (Id, leader, DMInitReply, ?j) where j <> 0;
         if j == Id then
            gEvent (final_leader, Id, UrlCapable)
         end if;
         -- processes ffDM and flDM in the LOTOS specification
         var k, l: Nat3 in
            loop
               alt
                  gDM (Id, ?k, DMInitRequest, ?any bool)
                     where (k <> Id) and (k <> 0)
               []
                  gDM (Id, ?k, DMInitReply, ?l)
                     where (k <> Id) and (k <> 0) and (l <> 0)
               end alt
            end loop
         end var
      end disrupt
   end var
end process

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

process ilDM [gDM: DMChannel, gEvent: EventChannel] (Id: Nat3,
        UrlCapable: bool, in var hosts: Hosts, in var nr: Nat3) is
   assert nr > 0;
   var j, k, l: Nat3, b: bool in
      alt
         if nr == 1 then
            nr := f_leader (Id, chge_rec (Id, UrlCapable, hosts));
            DeclareLeader [gDM, gEvent] (Id, UrlCapable, hosts, nr)
         else
            -- assert nr > 1
            gDM (Id, ?j, DMInitRequest, ?b) where (j <> Id) and (j <> 0);
            if not (rec (j, hosts)) then
               hosts := chge_rec (j, b, hosts);
               nr := nr - 1
            end if;
            ilDM [gDM, gEvent] (Id, UrlCapable, hosts, nr)
         end if
      []
         gDM (Id, ?k, DMInitReply, ?l)
            where (k <> Id) and (k <> 0) and (l <> 0);
         ilDM [gDM, gEvent] (Id, UrlCapable, hosts, nr)
      end alt
   end var
end process

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

process DeclareLeader [gDM: DMChannel, 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
         gDM (leader, Id, DMInitReply, leader)
      end if;
      -- processes ffiDM and fliDM in the LOTOS specification
      var j, k, l: Nat3 in
         loop
            alt
               gDM (Id, ?j, DMInitRequest, ?any bool)
                  where (j <> Id) and (j <> 0);
               gDM (j, Id, DMInitReply, leader)
            []
               gDM (Id, ?k, DMInitReply, ?l)
                  where (k <> Id) and (k <> 0) and (l <> 0)
            end alt
         end loop
      end var
   else
      if ((head (hosts).Id <> Id) and (head (hosts).Id <> leader)) then
         gDM (head (hosts).Id, Id, DMInitReply, leader)
      end if;
      DeclareLeader [gDM, gEvent] (Id, UrlCapable, tail (hosts), leader)
   end if
end process

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

end module