/*   mutex [] f1

   sf ([] (flag0_true -> <> proc0)) && ([] (flag1_true -> <> proc1)) && ([] (flag2_true -> <> proc2))

   deadlock ([]((c0 && c1) -> <>(proc0 || proc1)) && []((c0 && c2) -> <>(proc0 || proc2)) && []((c1 && c2) -> <>(proc1 || proc2)))
  []((c0 && c1 && !c2) -> <>(proc0 || proc1)) && []((c0 && c2 && !c1) -> <>(proc0 || proc2)) && []((c1 && c2 && !c0) -> <>(proc1 || proc2)) && []((c0 && c1 && c2) -> <>(proc0 || proc1 || proc2))

#define f1 (ncrit == 0 || ncrit == 1)

#define flag0_true (FLAG[0] == true)
#define proc0 (proc[0]@crit)
#define flag1_true (FLAG[1] == true)
#define proc1 (proc[1]@crit)
#define flag2_true (FLAG[2] == true)
#define proc2 (proc[2]@crit)

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

#define N_PROC 3

int M = N_PROC;
bool FLAG[N_PROC] = false;
int TURN[N_PROC] = 0;

byte ncrit = 0;

inline max(max_buf, temp_j_max) {
    max_buf = 0; temp_j_max = 0;

  do
  :: temp_j_max < N_PROC ->
        if
        :: TURN[temp_j_max] > max_buf ->
            max_buf = TURN[temp_j_max];
        :: TURN[temp_j_max] <= max_buf;
        fi;
    temp_j_max++;
  :: temp_j_max == N_PROC -> break;
  od;
}

inline acquire_mutex(i, MAX_TURN, j, j_max, j_waiting) {
    MAX_TURN = 0; j = 0; j_max = 0; j_waiting = 0;
L1: atomic {
        j = 0;
        do
        :: j < N_PROC ->
            (TURN[j] < M);
            j++;
        :: j == N_PROC -> break;
        od; j = 0;
    };

    FLAG[i] = true;
    max(MAX_TURN, j_max); TURN[i] = MAX_TURN;

    if
    :: TURN[i] >= M ->
        TURN[i] = 0; FLAG[i] = false;goto L1;
    :: TURN[i] < M -> TURN[i] = TURN[i] + 1;
    fi;

    FLAG[i] = false;

    do
    :: j_waiting < N_PROC ->
        if
        :: j_waiting != i ->
            !(FLAG[j_waiting] != false);
            !(TURN[j_waiting] != 0 && (TURN[j_waiting] < TURN[i] || (TURN[j_waiting] == TURN[i] && j_waiting < i)));
        :: j_waiting == i;
        fi;
        j_waiting++;
    :: j_waiting == N_PROC -> break;
    od;
}

inline release_mutex(i) {
   TURN[i] = 0;
}

active [N_PROC] proctype proc() {
  int MAX_TURN, j, j_max, j_waiting = 0;
again:
  acquire_mutex(_pid, MAX_TURN, j, j_max, j_waiting);
crit: {
  ncrit++;
  assert(ncrit == 1);
  ncrit--;
};
  release_mutex(_pid);
  goto again;
}