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 ;)).
this is because you combine a view statement with symmetry
reduction. Can you open an enhancement request on GitHub [1]?