atomicInc increments a variable and returns the old value of the variable atomically. Its definition can be written as follows:

int atomicInt(int *x) {
  /* do the following atomically */
  int t = *x;
  *x = *x + 1;
  return t;
}

We can use atomicInc to write a program that allows at most one process to enter the critical section at the same time. In the program, three variables are used as follows:

int ticket = 0;
int served = 0;
int check[N];  /* N is the number of processes. */

The program executed by process i can be written as follows:

l1: check[i] = atomicInc(&ticket);
l2: if (check[i] != served) goto l2;
cs:Critical Section
l3: served = served + 1;

Each process repeatedly executes this program.

1. Make a formal model of this program as a transition system and describe it in CafeOBJ.
2. Write proof scores in CafeOBJ showing that at most one process is at cs at the same time.