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

Re: [tlaplus] Skipping model when a property is satisfied

On 05.10.2018 16:52, Zixian Cai wrote:
> I'm just wondering whether it is possible to provide condition(s) to the
> model checker so that if these conditions are satisfied at a point, it
> skips the current model without further exploring.

Hi Zixian,

what kind of conditions are you thinking about that cannot be stated as
safety or liveness properties?