Re: [tlaplus] Why same number of TLC distinct states occupys different disk space size

[Markus Kuppe]

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.

Markus

> On Jan 12, 2023, at 4:50 AM, Vince Wu <fzu...@gmail.com> 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?