Hi everyone.
For a TLA+ project I'm working on, I wanted to use Parameterized instantiation in order to have a "general" module, that is to say a module where I would only have to change the variables names and a few other lines, and it would work for any number of variables.
In order to do so, I added a constant operator in the form of a set containing every variable, and made my state transitions iterate through this set by universal quantification, calling the instantiation state transition with each variable as a parameter in turn.
But when I did so, TLC never generated a state after the
initial one.
What I gathered from playing with PrintT is that, somewhere along the line, TLC defined the next-state value of my variable within the universal quantification. Thus, when I tried to define it in the state transition of the parameterized instantiation, TLC interpreted it as a test for equality and evaluated it at FALSE.
I still do not know where it does so. I guess it must be caused by my definition of a set of variables, that is a constant operator. Yet I did not manage to find a clear cut answer in Specifying Systems.
This is the reason underlying this message : to ask an explanation to someone better at TLA+ and TLC than me. For if I must abandon this idea, I at least want to understand why I have to.
But my specification was way to big to send here, so I wrote a little toy example where the error still emerges.
In it, the specification supermodule has two variables, which are both initialized at 0. The only transition is one where both variables are changed to 1 (through the mix of parameterized instantiation and universal quantification explained above). And the only temporal property to check is that both variables will eventually be equal to 1.
The issue mentionned above still appears in this toy example : TLC only generates the initial state.
Does someone have a precise explanation of this behavior ?
Thanks in advance, and have a good day.
Adam Shimi