Changes by: David Noblet (dnoblet at cs.caltech.edu)
Date: 2005-09-16 02:22:05 -0700 (Fri, 16 Sep 2005)
Revision: 2025
Log message:

      I made some edits to get the model into a form that can be verified by TLC. 
      
      It runs through the model checker (with two processes) in about 10 minutes.
      
      [dnoblet@flywheel:~/tla]> java -Xms1024M -Xmx1024M -cp /cs/prl/dump/tla/ tlc.TLC -workers 8 -difftrace ViewChange.tla
      TLC Version 2.0 of August 18, 2005
      Model-checking
      Parsing file ViewChange.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/Naturals.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/FiniteSets.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/Sequences.tla
      Parsing file /cs/prl/dump/tla/tlasany/StandardModules/TLC.tla
      Semantic processing of module Naturals
      Semantic processing of module Sequences
      Semantic processing of module FiniteSets
      Semantic processing of module TLC
      Semantic processing of module ViewChange
      Finished computing initial states: 2 distinct states generated.
      Progress(52): 524929 states generated, 150760 distinct states found, 11240 states left on queue.
      Progress(115): 4306979 states generated, 1128915 distinct states found, 18165 states left on queue.
      Model checking completed. No error has been found.
        Estimates of the probability that TLC did not check all reachable states
        because two distinct states had the same fingerprint:
          calculated (optimistic):  2.5112817216065095E-7
          based on the actual fingerprints:  6.347960939726746E-7
      4915297 states generated, 1271251 distinct states found, 0 states left on queue.
      The depth of the complete state graph search is 147.
      
      

Changes	Path
+39 -9	mojavefs/shmem/model/gc/view_change/tla/ViewChange.tla