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

[Hillel Wayne]

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

[Markus Kuppe]

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.

[Hillel Wayne]

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