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

Re: [tlaplus] Debug variables and VIEW

On 05.11.18 04:18, Catalin Marinas wrote:
I have a spec (cut-down version below) where I need to add a debug variable (cmd) to keep track of how an invariant fails. As expected, such variable increases the state space significantly while not having any other effect on the actual model. So I added a VIEW statement to the .cfg file so that 'cmd' is left out. While it indeed decreases the state space, it still doesn't go all the way to the no debug variable case.

TLC2 Version 2.13 of 18 July 2018

Without the 'cmd' debug variable (or cmd only set to inst[1] in the spec below, which is part of the symmetry optimisation):

5369 states generated, 244 distinct states found

With the debug variable and VIEW set to cpu_vars:

10341 states generated, 470 distinct states found

With the debug variable and default view:

32935 states generated, 1497 distinct states found

Is there anything I miss? Please note that I run TLC on the command line (I couldn't find an ARM build of the Toolbox ;)).

Hi Catalin,

this is because you combine a view statement with symmetry reduction.  Can you open an enhancement request on GitHub [1]?



[1] https://github.com/tlaplus/tlaplus/issues