module main : int)
{
    type process_id_t = [n] int;
    type message_t = int;

    var id : process_id_t; // Process identifiers
    var m : message_t; // Message received

    init {
        // Initialize process identifiers
        forall i: [n] {
            id[i] := i + 1; // Assign unique identifier to each process
        }
    }

    process electionProcess(i : int)
    {
        var next : int;
        var prev : int;

        if (i == 0) {
            prev := n - 1;
        } else {
            prev := i - 1;
        }

        if (i == n - 1) {
            next := 0;
        } else {
            next := i + 1;
        }

        send(id[i], next); // Send own id to next process

        while (true) {
            receive(m, prev); // Receive message from previous process

            if (m == id[i]) {
                stop;
            }

            if (m > id[i]) {
                send(m, next);
            }
        }
    }

    // Create n instances of electionProcess
    forall i: [n] {
        electionProcess(i);
    }
}
