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

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

From: Hillel Wayne <hwayne@xxxxxxxxx>
Date: Mon, 16 Dec 2024 12:00:19 -0600
User-agent: Mozilla Thunderbird

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/bc3ee38f-e053-48f2-8b62-78fb15674434%40gmail.com.

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

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