module co4_2a_1 (CO4_DATATYPES, CO4_PROCESSES) is

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

process KBHierarchy [user: UserActionChannel,
            up1, down1, up2, down2: MessageChannel,
            signal: SignalValChannel] is
   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, up2, down2 ->
      hide down: MessageChannel in
         par down in
            InitQueue [down, down1]
         ||
            InitGroupKB [up1, down, down2, up2, signal] (3 of BaseId)
         end par
      end hide
      (* group has no parent *)
   ||
      up2, down2 -> access up2, down2 -- 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 (1 of BaseId, doachieve, {Assert (square)} of Proposal);
      stop
   ||
      AllUserReply [user]
   end par
end process

end module