Re: [tlaplus] Why same number of TLC distinct states occupys different disk space size
21 views
Skip to first unread message
Markus Kuppe
Jan 12, 2023, 11:47:47 AM1/12/23
to tla...@googlegroups.com
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?
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?
Reply all
Reply to author
Forward
0 new messages