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 |