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

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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?

Thanks
Markus