[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].

Thanks
Markus

[1]
https://github.com/tlaplus/tlaplus/blob/f4763d800472fd3f5c4ce1913ee01cf46bf2a6d4/tlatools/src/tlc2/TLC.java#L138-L201
[2] https://github.com/tlaplus/tlaplus/issues/79