module main int)
{
    type id_t = 1..n;
    type message_t = struct {
        m: id_t;
    };

    var channel ch: message_t;

    procedure process(id: id_t)
    {
        var m: id_t;
        send(ch, {m: id});
        while (true) {
            var msg: message_t;
            receive(ch, msg);
            m := msg.m;
            if (m == id) {
                break;
            }
            if (m > id) {
                send(ch, {m: m});
            }
        }
    }

    var processes: array[id_t] of process_id;

    init {
        for (var i: id_t) {
            processes[i] := create_process(process(i));
        }
    }
}
