state = RES_GRANTING;
reqResId = id;
}
+ else if (reqResId == id) {
+ return SUCCESS;
+ }
else return call Queue.enqueue(id);
}
signal ResourceDefaultOwner.requested();
if(state == RES_BUSY && resId == id) {
if(call Queue.isEmpty() == FALSE) {
reqResId = call Queue.dequeue();
+ resId = NO_RES;
state = RES_GRANTING;
post grantedTask();
call ResourceConfigure.unconfigure[id]();