Problemas con codigo PROMELA ayudaa plis

[fhernandoecheverria]

Tngo un problema con codigo de PROMELA, este tipo de codigo es para programar las simulaciones de los protocolos de red. Todo esta programado con el C++. Alguno me podria decir si alguno de uds. conoce del tema para Q puede ayudarme a resolver esto

mtype = {MSG, ACK}

chan canal = [3] of {mtype, int, int}

proctype Usuario(int user) {
int dato;
int usuario = user;
int acuse_user;

do
:: canal ! MSG, 1105, usuario ->
printf("mensaje enviado");
//if
canal ? ACK, dato, acuse_user;
//if
//:: usuario == acuse_user ->
//printf ("vamos bien xD ");
//:: else ->
//skip;
//fi
//:: timeout -> skip;
//fi
od
}

proctype Servidor() {
int dato;
int acuse_user;
do
:: canal ? MSG, dato, acuse_user ->
printf("mensaje recibido: %d", dato);
canal ! ACK, dato, acuse_user;
od
}


init {

run Usuario(1200);
run Usuario(2100);
run Servidor();
}


Estoy programando el protocolo ALOHA, el cual dice que siempre habra un canal llamado servidor escuchando cualquier mensaje emitido por todos los clientes, sin embargo cuando dos o mas clientes envian mensage al mismo tiempo se crea una colision y ambos clientes esperan un tiempo aleatorio (time out aleatorio) para poder reenviar su paquete y es ahi donde tngo problemas en no saber como crear la colision y como crear el tiempo aleatorio. Desde ya muchas GRACIAS por su ayuda y su tiempo. Saludos a todos.