function isHighestProcess(int id) returns boolean {
	int i;
	boolean b;
	loc loc0: 
		do {
			i := 0;
		}
		goto loc1;
	loc loc1:
		when (i == CONST.N) do { 
			b := true;
		}
		goto loc2;
		when (i < CONST.N && (i == id)) do {
			i := i+1;
		}
		goto loc1;
		when (i < CONST.N && (i != id) && (inL[i] < inL[id])) do {
			i := i+1;
		}
		goto loc1; 
		when (i < CONST.N && (i != id) && (inL[i] >= inL[id])) do {
			 b := false;
		}
		goto loc2;
	loc loc2:
		do {}
		return b;
		// note that assignments to b must all be in the same location
}