module KO (TYPES, CHANNELS) is

process MAIN [RECEIVE_BLOCK_PROPOSAL: BLOCK, COMMIT_PROPOSED_BLOCK: COMMIT,
              COMMIT_EMPTY_BLOCK: COMMIT] is
   loop
      alt
         RECEIVE_BLOCK_PROPOSAL (0 of BIT);
         alt
            i;
            COMMIT_PROPOSED_BLOCK
         []
            i;
            COMMIT_EMPTY_BLOCK
         end alt
      []
         RECEIVE_BLOCK_PROPOSAL (1 of BIT);
         COMMIT_EMPTY_BLOCK
      end alt
   end loop
end process

end module