[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC simulation mode
Thanks, Markus!
> * 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.
The "new" word is definitely a typo here. Fixed that.
> * 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.
Good point! I agree that running a simulation as a smoke test is a
typical scenario. Another use case is to explore the state space of a
protocol with too large state space, before applying any reasonable
abstraction. I guess, the current approach of computing all successors
would not work on large sets anyways, so one would have to use
TLC!RandomElement to emulate something like that.
Best,
Igor
On Fri, May 1, 2026 at 1:04 AM Markus Kuppe
<tlaplus-google-group@xxxxxxxxxxx> wrote:
>
> 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.
--
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/CACooHMBbJOuoRfqJUg%2B5Drct%3DiZWm%3D1Z%2BLsQH2E--WGOjTDapw%40mail.gmail.com.