[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] What's the difference between `-simulate` and `-generate`?

From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
Date: Mon, 16 Dec 2024 10:23:46 -0800
References: <bc3ee38f-e053-48f2-8b62-78fb15674434@gmail.com>

The `-generate` option was introduced as part of the work on https://www.youtube.com/watch?v=cYenTPD7740.  It should not be used to verify a specification, but only to collect statistics by generating finite prefixes of behaviors.

M.

> On Dec 16, 2024, at 10:00 AM, Hillel Wayne <hwayne@xxxxxxxxx> wrote:
> 
> It seems `-generate` adds a .probabilistic key, which seems to generate fewer states. Is that correct? Is there a more detailed or comprehensive explanation of what `-generate` does?
> H


-- 
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/3529E820-6F7C-41F2-9898-BF7DB6820455%40lemmster.de.

Follow-Ups:
- Re: [tlaplus] What's the difference between `-simulate` and `-generate`?
  - From: Hillel Wayne

References:
- [tlaplus] What's the difference between `-simulate` and `-generate`?
  - From: Hillel Wayne

Prev by Date: [tlaplus] What's the difference between `-simulate` and `-generate`?
Next by Date: [tlaplus] Re: Is there a decision procedure for telling whether a spec is machine-closed?
Previous by thread: [tlaplus] What's the difference between `-simulate` and `-generate`?
Next by thread: Re: [tlaplus] What's the difference between `-simulate` and `-generate`?
Index(es):
- Date
- Thread