module co4_6_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
      up1, down1 -> InitIndividualKB [user, down1, up1, signal] (1 of BaseId)
   ||
      up1, down1, up2, down2 ->
      hide up: MessageChannel in
         par up in
            InitQueue [up1, up]
         ||
            InitGroupKB [up, down1, down2, up2, signal] (3 of BaseId)
         end par
      end hide
   ||
      up2, down2, up3, down3 ->
      hide up: MessageChannel in
         par up in
            InitQueue [up2, up]
         ||
            par
               InitGroupKB [up, down2, down3, up3, signal] (5 of BaseId)
            ||
               InitGroupKB [up, down2, down3, up3, signal] (6 of BaseId)
            end par
         end par
      end hide
      (* 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 (1 of BaseId, doforward, reqregister (5 of BaseId));
      user (1 of BaseId, doforward, reqregister (6 of BaseId));
      stop
   ||
      AllUserAccept [user]
   end par
end process

end module