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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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 <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.