Why same number of TLC distinct states occupy different disk space
7 views
Skip to first unread message
Vince Wu
Jan 12, 2023, 8:20:14 AM1/12/23
to tlaplus
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?
>> 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?
Reply all
Reply to author
Forward
0 new messages