Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-21 01:25:21 -0700 (Wed, 21 Sep 2005)
Revision: 7772
Log message:

      This model is almost perfect... 
      
      I do get a small discrepancy in the total number of states if I start 
      with different initial states. I can't really explain it but it might be 
      just an artifact of spin's way of displaying the number of states.
      
      Also, this model finds a counter-example for buffer size 5 and 2 processes
      but it seems to work fine for 2 processes with buffer size of 6.
      
      

Changes  Path
+4 -1 mojavefs/shmem/model/gc/view_change/spin/OMakefile
+105 -94 mojavefs/shmem/model/gc/view_change/spin/gcomm.pml