[tlaplus] Why same number of TLC distinct states occupy different disk space

[Vince Wu <fzuwwl@xxxxxxxxx>]

I read from **Specifying Systems** that:

>> In the actual implementation, the nodes of the graph G are not the views of states, but fingerprints of those views. A TLC fingerprint is a 64-bit number generated by a "hashing" function.

According to this I assume that the same number of distinct states should occupy similar disk spaces.

But when I am verifying two raft TLA+ spec using TLC:

1. https://github.com/kikimo/tla-raft/blob/master/Raft.tla
2. https://github.com/kikimo/raft-tlaplus/blob/main/specifications/standard-raft/Raft.tla

I found that for both 4 billions of distinct states, the first spec took about 320G disk space while the second spec took just about 60G disk space. How could this happend?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/608d9234-fa71-40e1-bff6-a75958f5f08en%40googlegroups.com.