Re: [tlaplus] TLC simulation mode

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

Unless you want TLC!RandomElement to bias successor selection with a custom (rational) distribution, TLC's -generate gives you the same "don't enumerate all successors" behavior: the simulator picks a random disjunct / existential quantification and returns the first successor. Note this samples over syntactic alternatives, not over the successor set. Minor technical limitation: -generate also does not yet support CASE statements.

M.

> On May 2, 2026, at 1:37 AM, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
> 
> 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.


-- 
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/E025CBB5-B533-439A-9D59-B2222B4477F4%40lemmster.de.