1. (10 points) Consider the two mutual exclusion algorithms below. Use the translation function in Section 2.2.2 to translate the program to a first-order logic representation. You only need to translate the lock() methods. Be sure to do a translation for each version: mutex one and mutex two.
2. (10 points) Create the Kripke structure for Mutex One from the first-order representation in the first problem. Express the first 10 states of the Kripke as a dotty graph (see below). Use a depth first search to generate the 10 states always preferring the first thread in the transition.

Below are two different algorithms for mutual exclusion. That are called in the following way from two threads:

cobegin run() || run() coend

The global variable initialization and code for run follows:

int turn = 0;
int signal[2] = {0, 0};
 
void run() {
   int i = getpid();  //Only returns 0 or 1
   while(1) {
      lock(i);
      CriticalSection();
      unlock(i);
   }
}

void lock (int i) {
      int j = 1 - i;
      signal[i] = 1;
      while (turn != i) {
         while (signal[j]);
         turn = i;
      }
 }
 
void unlock(int i) {
   signal[i] = 0;
}

void lock (int i) {
      int j = 1 - i;
      signal[i] = 1;
      turn = j;
      while (signal[j] && turn != i);
 }
 
void unlock(int i) {
   signal[i] = 0;
}

Graphviz is a tool set for graph layout and manipulation. We will use the tool set from time to time to visualize different Kripke structures and graphs. Below is a an example input file for a Kripke:

 digraph massive_output {
 0 -> 1;
 0 -> 2;
 1 -> 4;
 2 -> 0;
 2 -> 5;
 3 -> 3;
 3 -> 2;
 3 -> 0;
 4 -> 1;
 4 -> 2;
 5 -> 6;
 6 -> 3;
 0 [label="0\n"+"~Start\n"+"~Close\n"+"~Heat\n" + "~Error\n"];
 1 [label="1\n"+"Start\n"+"~Close\n"+"~Heat\n" + "Error\n"];
 2 [label="2\n"+"~Start\n"+"Close\n"+"~Heat\n" + "~Error\n"];
 3 [label="3\n"+"~Start\n"+"Close\n"+"Heat\n" + "~Error\n"];
 4 [label="4\n"+"Start\n"+"Close\n"+"~Heat\n" + "Error\n"];
 5 [label="5\n"+"Start\n"+"Close\n"+"~Heat\n" + "~Error\n"];
 6 [label="6\n"+"Start\n"+"Close\n"+"Heat\n" + "~Error\n"];
  }

Notice that the description language is simple: edge list followed by labels. To render the file as a PDF graph, use the following command:

dot -Tpdf -o .pdf .dot

or

dot -Tpdf .dot -o .pdf 

Many more details and documentation at Graphviz.