module co4_4_1 (CO4_DATATYPES, CO4_PROCESSES) is

process MAIN [user: UserActionChannel,
            up1, down1, up2, down2, up3, down3: MessageChannel,
            signal: SignalValChannel,
            OK: none] is
   par user in
      disrupt
         UserInput [user]
      by
         null
      end disrupt
   ||
      KBHierarchy [user, up1, down1, up2, down2, up3, down3, signal]
   end par;
   i;
   Ring [OK]
end process

process KBHierarchy [user: UserActionChannel,
            up1, down1, up2, down2, up3, down3: MessageChannel,
            signal: SignalValChannel] is
   par
      up2, down2 ->
      par
        up1, down1 ->
        par user, up1, down1 in
           par
              InitIndividualKB [user, down1, up1, signal] (1 of BaseId)
           ||
              InitIndividualKB [user, down1, up1, signal] (2 of BaseId)
           end par
        ||
           SerializeIndividualKB [user, down1, up1]
        end par
     ||
        up1, down1 ->
        hide up: MessageChannel in
           par up in
              InitQueue [up1, up]
           ||
              InitGroupKB [up, down1, down2, up2, signal] (3 of BaseId)
           end par
        end hide
     ||
        InitIndividualKB [user, down2, up2, signal] (4 of BaseId)
        end par
   ||
      up2, down2, up3, down3 ->
      hide up: MessageChannel in
         par up in
            InitQueue [up2, up]
         ||
            InitGroupKB [up, down2, down3, up3, signal] (5 of BaseId)
         end par
      end hide
      (* 5 of BaseId has no parent *)
   ||
      up3, down3 -> access up3, down3 -- i.e., null
   end par
end process

process UserInput [user: UserActionChannel] is
   par
      user (1 of BaseId, doregister, 3 of BaseId);
      user (2 of BaseId, doregister, 3 of BaseId);
      user (4 of BaseId, doregister, 5 of BaseId);
      user (1 of BaseId, doforward, reqregister (5 of BaseId));
      user (1 of BaseId, doforward, reqachieve ({Assert (white)} of Proposal));
      stop
   ||
      AllUserReply [user]
   end par
end process

end module