black_white_bakery_alg

#define n_proc 10 /* Число конкурирующих процессов */
#define n 9 /* Число для индексации массива */

mtype = { black, white };

bool choosing[n] = false;
mtype color[n] = black;
int TURN[n] = 0;
mtype cur_color = black;
int mult = 1;

inline max(i, temp, j, max_number) {
    do
        ::j < n_proc ->
            if
            ::color[j] == color[i] ->
                 if
                 ::TURN[j] > max_number ->
                    max_number = TURN[j];

                 fi;
            fi
    od;
    temp = 1 + max_number;
}

inline unlock(i) {
    if
    ::color[i] == black ->
        cur_color = white;
    ::else ->
        cur_color = black;
    fi;
}

inline lock(i, temp, j, max_number, pointer_j) {
	choosing[i] = true;
	color[i] = cur_color;

	max(i, temp, pointer_j, max_number);
	TURN[i] = 1 + temp;
	choosing[i] = false;
	do
	    ::j < n ->
            if
            ::choosing[j] == false ->
                if
                ::color[i] == color[j] ->
                    ((TURN[j] != 0) && ((TURN[j] < TURN[i]) && (j < i)) &&  (color[j] == color[i]));
                ::else ->
                    (TURN[j] != 0 && (color[i] == cur_color) && color[j] != color[i]);
                fi;
            ::else -> skip;
            fi;

          j = j + 1;
    od;

}

active[n] proctype proc() {
	int temp = 0;
	int j = 0;
	int max_number = -1;
	int pointer_j = 0;
	lock(_pid, temp, j, max_number, pointer_j);

	mult = mult * 31;
	assert(mult == 31);
	mult = mult / 31;
	unlock(_pid);

}