Re: [tlaplus] TLC simulation mode

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

Hi Igor,

thanks for conducting these experiments and summarizing the results in a blog post.  Two comments:

* The statement “The new TLC simulation mode achieves better coverage than random walks…” may be a bit misleading. There isn’t anything fundamentally new about the simulation mode itself, aside from the ability to collect statistics.

* On a related note, the statistics collection hasn’t been optimized. In practice, users are more likely to run simulations up to a wall-clock time bound rather than focus on detailed metrics. Additionally, collecting statistics requires repeatedly computing state fingerprints, which is relatively expensive^1. It could be useful to quantify this overhead by rerunning some of the same experiments with statistics collection disabled.

Markus

^1 As a possible mitigation, one could also consider collecting statistics on only a single TLC worker while the remaining workers do not collect statistics.

> On Apr 30, 2026, at 10:22 AM, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
> 
> Thanks Markus!
> 
> I've re-run the experiments with TLC and TLC simulation. TLC
> simulation achieves almost complete coverage much faster than random
> walks on the two-phase commit. On readers-writers and FPaxos, the
> model checker is still much better than simulation, both in terms of
> coverage and running times.
> 
> Here is the second blog post on this:
> https://protocols-made-fun.com/model-checking/simulation/2026/04/30/tlc-vs-simulation.html
> 
> Best,
> Igor
> 
> On Thu, Apr 16, 2026 at 7:35 PM Markus Kuppe
> <tlaplus-google-group@xxxxxxxxxxx> wrote:
>> 
>> You can get distinct state counts with a JVM system property and a small amount of TLA+.
>> 
>> Step 1: Enable extended statistics
>> 
>> Pass `-Dtlc2.tool.Simulator.extendedStatistics=true` to the JVM.
>> 
>> `java -Dtlc2.tool.Simulator.extendedStatistics=true -jar tla2tools.jar -simulate num=10000 MySpec`
>> 
>> This uses a HyperLogLog (constant space, approximate count) per worker to track distinct states. If you want exact counts and don't mind even more overhead, also pass `-Dtlc2.tool.Simulator.extendedStatistics.naive=true`
>> 
>> Step 2: Read the count via TLCGet("stats").distinct
>> 
>> With extended statistics enabled, TLCGet("stats").distinct returns the number of distinct states seen (instead of -1). You can use _PERIODIC to monitor it during simulation and POSTCONDITION to report it at the end.
>> 
>> Add to your spec:
>> 
>> ```tla
>> SimStats ==
>>    LET s == TLCGet("stats")
>>    IN PrintT(<<"traces", s.traces,
>>                "generated", s.generated,
>>                "distinct", s.distinct>>)
>> ```
>> 
>> Both need to be declared in the .cfg file:
>> 
>> ```
>> _PERIODIC SimStats
>> POSTCONDITION SimStats
>> ```
>> 
>> This will print something like the following at every progress interval and once at the end.
>> 
>> <<"traces", 10000, "generated", 2067418, "distinct", 8374>>
>> 
>> Caveats: The distinct count is per worker thread, not globally deduplicated across workers. With -workers 1 (the default) this doesn't matter. With multiple workers, each maintains its own counter. The HyperLogLog approximation is usually within a few percent of the true count. Use the naive flag if you need exactness.
>> 
>> M.
>> 
>> PS: TLCGet("stats”) also includes per-action counts, per-variable distinct values, and trace length statistics. I've used this (https://github.com/microsoft/CCF/issues/6537) to serialize the full record to ndjson and plot coverage over time.
>> 
>> 
>>> On Apr 15, 2026, at 12:49 AM, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
>>> 
>>> Is there an easy way to count how many distinct states the simulator visited?
>> 
>> --
>> 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 visit https://groups.google.com/d/msgid/tlaplus/0CDF0FD4-E507-4BF0-B1FD-81405E049A6B%40lemmster.de.
> 
> -- 
> 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 visit https://groups.google.com/d/msgid/tlaplus/CACooHMC_fsCtkY%3D4D4BJA47p%3DXPW_OVYL9rBn-70uE6k%2BoyFSg%40mail.gmail.com.

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/0FBF45DC-C0C2-4F7A-9E59-56045C037A48%40lemmster.de.