Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2005-09-15 00:36:41 -0700 (Thu, 15 Sep 2005)
Revision: 2021
Log message:

      This is the spin model that should be similar to the TLA model we have.
      
      I just ran it in verification mode and it finished in about 5-7 minutes.
      
      [crt@dhcp-133-187 spin]$ ./gcomm.spin
      Depth=     336 States=   1e+06 Transitions= 4.5289e+07 Memory= 178.852
      (Spin Version 4.2.5 -- 2 April 2005)
              + Partial Order Reduction
      
      Full statespace search for:
              never claim             - (none specified)
              assertion violations    +
              cycle checks            - (disabled by -DSAFETY)
              invalid end states      +
      
      State-vector 176 byte, depth reached 336, errors: 0
      1.40245e+06 states, stored
      6.48361e+07 states, matched
      6.62386e+07 transitions (= stored+matched)
             7 atomic steps
      hash conflicts: 7.85311e+07 (resolved)
      
      Stats on memory usage (in Megabytes):
      263.660 equivalent memory usage for states (stored*(State-vector + overhead))
      247.803 actual memory usage for states (compression: 93.99%)
              State-vector as stored = 165 byte + 12 byte overhead
      2.097   memory used for hash table (-w19)
      0.320   memory used for DFS stack (-m10000)
      0.436   memory lost to fragmentation
      249.816 total actual memory usage
      
      unreached in proctype node_active
              line 741, state 933, "-end-"
              (336 of 933 states)
      unreached in proctype :init:
              (0 of 12 states)
      
      

Changes	Path
+2 -1	mojavefs/shmem/OMakefile
Added	mojavefs/shmem/model/OMakefile
Added	mojavefs/shmem/model/gc/view_change/spin/OMakefile
+303 -87	mojavefs/shmem/model/gc/view_change/spin/gcomm.pml