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

Re: [tlaplus] Re: understanding temporal properties

On 05.10.2018 17:08, Bekir Oguz wrote:
> Is there a way to ask the model checker to give all paths in which the
> invariable is falsifiable instead of stopping at the first failure?

Hi Bekir,

you can run TLC from the command-line with the "-continue" parameter [1]
which causes it to print error traces but keep exploring. This is not
supported from inside the Toolbox though [2].


[2] https://github.com/tlaplus/tlaplus/issues/79