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

[Hillel Wayne <hwayne@xxxxxxxxx>]

We were able to find a minimal example demonstrating the differences:

---- MODULE testgenerate ----
EXTENDS TLC, Integers

VARIABLE x

Set == 1..100000

Init == x = 0

Pick ==
    /\ x = 0
    /\ \E y \in Set:
        x' = y

Done ==
    /\ x # 0
    /\ UNCHANGED x

Next == Pick \/ Done

Spec == Init /\ [][Next]_x

Invariant == x # 999
====

Running this with `-generate num=1000` is significantly faster than 
running `-simulate num=1000`, but if you add `INVARIANT Invariant`, 
`-generate num=1` passes while `-simulate num=1` finds an error.

H

On 12/16/2024 12:23 PM, Markus Kuppe wrote:
> 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/aaf33846-bf1f-4200-881a-114dfc688af1%40gmail.com.