CSCI 6962 DCI Exercise 3

 

1. Use pi-calculus to model the 2-dining philosopher problem.

 

2. Use SUM and STRUCT to prove the SUM2 Rule:

 

       

α

       
    Q   -->   Q'    
-----------------
         

α

     
  P + Q   -->   Q'