bw_bakery

/*
me [] f1
#define f1 (mult == 31 || mult == 1)

ffs  [] ((c0 -> <>proc0) && (c1 -> <> proc1))

#define c0 (choosing[0] == true)
#define proc0 (proc[0]@crit)
#define c1 (choosing[1] == true)
#define proc1 (proc[1]@crit)


freedom for blocking
ffb [] []((c0 && c1 && !c2) -> <>(proc0 || proc1)) && []((c0 && c2 && !c1) -> <>(proc0 || proc2)) && []((c1 && c2 && !c0) -> <>(proc1 || proc2)) && []((c0 && c1 && c2) -> <>(proc0 || proc1 || proc2))

#define c0 (choosing[0] == true)
#define proc0 (proc[0]@crit)
#define c1 (choosing[1] == true)
#define proc1 (proc[1]@crit)
#define c2 (choosing[2] == true)
#define proc2 (proc[2]@crit)

*/

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

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, j, max_number) {

j = 0;
max_number = 0;
    do
        ::j < n_proc ->
            if
            ::color[j] == color[i] ->
                 if
                 ::TURN[j] > max_number ->
                    max_number = TURN[j];
	::else -> skip;
                 fi;
	::else -> skip;
            fi;
	j = j + 1;
          :: else -> break;
    od;

}

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

inline lock(i, j, max_number, pointer_j) {

	j = 0;
	choosing[i] = true;
	color[i] = cur_color;

	max(i, pointer_j, max_number);
	TURN[i] = 1 + max_number;
	choosing[i] = false;
	do
	    ::j < n ->
 		if
		:: j != i ->

            		(choosing[j] == false);
                			if
                				::color[i] == color[j] ->


                    					((TURN[j] == 0) || ((TURN[j] > TURN[i]) || (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;
    	::else -> break;
    od;

}

active[n] proctype proc() {

	int j = 0;
	int max_number = 0;
	int pointer_j = 0;
again:	lock(_pid, j, max_number, pointer_j);

crit: 	{ mult = mult * 31;
	assert(mult == 31);
	mult = mult / 31;
};
	unlock(_pid);
	goto again;

}