module COUNTER (TYPES, CONSTANTS, CHANNELS) is

process COUNTER [PROPAGATE: PROPAGATE, SELF_PROPAGATE: SELF_PROPAGATE,
                 TALLY: TALLY] (ID: PID) is
   var B: BIT, J: PID, K0, K1: NAT in
      K0 := 0;
      K1 := 0;
      loop
         alt
            only if K0 + K1 < N then
               alt
                  -- propagation events go from other nodes to this counter
                  PROPAGATE (?J, ?B) where J <> ID
               []
                  -- self-propagation events go from each node to its counter
                  SELF_PROPAGATE (ID, ?B)
               end alt;
               if B == 0 then
                  K0 += 1
               else
                  K1 += 1
               end if
            end if
         []
            TALLY (ID, K0, K1);
            K0 := 0;
            K1 := 0
         end alt
      end loop
   end var
end process

end module