1. (10 points) Answer problems 1(f) through 1(k) from the SPIN Verification Examples and Exercises

2. (30 points) Answer problems 2(a) through 2(b) from the SPIN Verification Examples and Exercises. Note that the PROMELA code does not include all the transitions in the figure and it is missing transitions as well. Part of your answer should modify the PROMELA to match the diagrams. Also, for the second part, b, modify the PROMELA in S1 for both terminal A and terminal B.

3. (20 points) This problem comes from CalTech's CS 118 Assignment 4. Consider a distributed system that consists of five producers, one scheduler, and two consumers. Each producer has two tasks that need to be completed by a consumer. For each task, a producer sends a request to the scheduler. The scheduler has a queue to store up to five incoming producer requests. The scheduler, upon receiving a request, assigns the task to one of the consumers. The two consumers have their own separate queue of outstanding tasks. A consumer can only service one request at a time, but it can have up to two outstanding tasks waiting in the queue. Consumers do not acknowledge completion of tasks.

The definitions for prototypes Producer, Consumer, and init are provided below. Write the definition for prototype Scheduler for assigning tasks to the consumers. The scheduler is constrained by the following property when assigning tasks: it must balance the workloads of the two consumers. That is, a new task is always assigned to the consumer who has the fewest number of outstanding tasks in its queue. If the number of tasks currently assigned is equal, then the task could be assigned to either consumer. Prove with SPIN that your solution has the right properties.

mtype = { task }
chan prodToSched = [5] of {mtype, byte}
chan schedToCons[2] = [10] of {mtype, byte}
 
proctype Producer(byte me) {
  prodToSched!task(me)
  prodToSched!task(me)
}
 
proctype Consumer(byte me) { 
  byte you
  do
  :: schedToCons[me]?task(you)
  :: timeout -> break
  od
}
 
init { 
  byte i
  atomic { 
    for (i : 0 .. 4) {
      run Producer(i)
    }
    run Consumer(0)
    run Consumer(1)
  } 
}
 
active proctype Scheduler () {  
  /* you write this */
}

4. (50 points) Write a PROMELA verification model for Dikstra's Token Termination Algorithm (another presentation) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by N the number of nodes participating in the system.

• (25 points) All nodes are passive, the token goes one-time around, and the system terminates
• (10 points) Exactly one node is active, but it does not send any messages, and when it receives the token, it switches to passive and sends the token out black
• (10 points) The one active node may send at most one message total, and that message can be to to any other node; if a node receives a message causing it to become active, then it too may only send at most one message even if it is again activated by an incoming message; in this way, there can never be more than N messages ever sent. The node non-deterministically chooses if it will send a message or not.
• (5 points) Any node may start active (one message bound still applies)

Please note that messages related to the token do not count in the send/receive counters. Also note that a node becomes passive once it receives a token.