[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Why same number of TLC distinct states occupys different disk space size
Besides the fingerprint set, TLC stores a state queue, a trace, and the liveness graph on disk, and, thus, the disk space will vary depending on a spec’s variables and values.
> On Jan 12, 2023, at 4:50 AM, Vince Wu <fzuwwl@xxxxxxxxx> wrote:
> I read from **Specifying Systems** that:
> >> In the actual implementation, the nodes of the graph G are not the views of states, but ngerprints of those views. A TLC ngerprint 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/1DE6F1A0-F547-4017-A8A8-4D16DB8E43F7%40lemmster.de.