*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.