I am modeling a system in PROMELA that has a central controller and N workers. There is a lot of broadcasting (e.g. sending a message from the controller to all workers, or receiving messages from all workers) and I find myself repeating the same line of code with an index incremented. For example, the following do block checks if a process has received data and if not it sends data to it.

    do
    :: (has_data[0]==0) -> atomic{
        channels[0].env!1;
        has_data[0]=1;
    }
    :: (has_data[1]==0) -> atomic{
        channels[1].env!1;
        has_data[1]=1;
    }
    :: (has_data[2]==0) -> atomic{
        channels[2].env!1;
        has_data[2]=1;
    }
    :: timeout -> goto end;
    od

Similarly, there are if constructs to read messages from at least one of the workers, for example this is an if construct to read data from a unique worker.

        if
        :: (has_written[0]==0) && ((channels[0].write?[DT,good]))-> atomic{
            channels[0].write?DT,write_data;
            has_written[0]=1;
        }
        :: (has_written[1]==0) && ((channels[1].write?[DT,good]))-> atomic{
            channels[1].write?DT,write_data;
            has_written[1]=1;
        }
        :: (has_written[2]==0) && ((channels[2].write?[DT,good]))-> atomic{
            channels[2].write?DT,write_data;
            has_written[2]=1;
        }
        :: timeout -> goto voting_increment;
        fi

These examples are for 3 worker processes, but I would like to parameterize them to n workers, is there a way to abstract-away the repetition of code by denoting a range of indices to the do and if loops?