Chapter 9 of the course text.

Consider the below solution to the dining philosopher for just two participants. Each active thread describes the state of the philosopher. Both start in the the first location, loc0. For example, in the first location of Philosopher1, when fork1 is available, then Philosopher1 sets fork1 to true and jumps to loc1 (goto loc1). The description details a transition system from which it is possible to derive a Kripke structure.

system TwoDiningPhilosophers {
	boolean fork1 = false;
	boolean fork2 = false;
 
	active thread Philosopher1() {
		loc loc0:  // take first fork
		   when !fork1 do  { 
                      fork1 := true; 
                   }
      		   goto loc1;
 
    		loc loc1:  // take second fork 
      		   when !fork2 do { 
                      fork2 := true; 
                   }
      		   goto loc2;
 
                   when fork2 do {
                      fork1 := false;  
                   }
      		   goto loc0;
 
   		loc loc2:  // drop second fork 
      		   when true do { 
                      fork2 := false; 
                   }
      		   goto loc3;
 
    		loc loc3:  // drop first fork
      		   when true do { 
                      fork1 := false; 
                   }
      		      goto loc0;
  	}
 
  	active thread Philosopher2() {
    		loc loc0:  // take second fork
      		   when !fork2 do { 
                      fork2 := true; 
                   }
      		   goto loc1;
 
    		loc loc1:  // take first fork
      		   when !fork1 do { 
                      fork1 := true; }
      		      goto loc2;
 
                   when fork1 do { 
                      fork2 := false; 
                   }
      		   goto loc0;
 
    		loc loc2: // drop first fork
      		   when true do { 
                      fork1 := false; 
                   }
      		   goto loc3;
 
    		loc loc3:  // drop put second fork
      		   when true do { 
                      fork2 := false; 
                   }
      		   goto loc0;
  	}
 
 

Consider the following property description for the dining philosophers.

// Liveness Property:
 //
 //  If a philosopher picks up a fork, he will eventually release it
 //  (this can be done for fork 1 or 2) 
 //
 // LTL:
 //   
 //    f = [] (fork1/2 --> <> !fork1/2)

1. (3 points) Write the complement of the property so it is expressed as a never-claim.
2. (5 points) Create the Buechi Automaton for the never-claim in the previous problem. Express the automaton in either a dotty format or the text format used to describe the dinning philosopher protocol above (i.e., locations with guarded or unguarded commands). Please label accept locations as locX:accept where X is a number. For example, loc1:accept.
3. (15 points) Perform on-the-fly model checking to see if our system satisfies the property (i.e., check the intersection of the model and the never claim). Please show the entire search graph as we did in class.When doing to the intersection, treat each location as as single atomic step.