| Hi,
the key elements of your toy module are
Mod(s) == INSTANCE mod WITH s <- s
All == {s0, s1} t == \A s \in All : Mod(s)!Add
where in mod we have
Let's assume that TLC attempts to evaluate action t in state z where both variables s0 and s1 have value 0. Then All = {0} and the definition of t boils down to Mod(0)!Add, which in turn evaluates to 0' = 1, which is FALSE, so there is no successor state of z for action t.
It seems to me that your mental picture is a semantics of "call by name" where set All would contain references to the variables s0 and s1 rather than the values of these variables.
Back to your original intention: the canonical way to obtain a generic specification is to use functions (arrays). More precisely, a single variable evaluates to a function, and each "array cell" corresponds to the individual variables that you have in mind. Concretely,
CONSTANT Dom VARIABLE s
\** initialize the entire array Init == s = [d \in Dom |-> 0]
\** update certain elements of the array trans(D) == s' = [d \in Dom |-> IF d \in D THEN 1 ELSE s[d]]
\** next-state relation: update some array elements Next == \E D \in SUBSET Dom : trans(D)
In practice, of course, both the update and the conditions on the choice of the subset to update would be more complicated.
Note in particular that the action trans has to define the new value of the overall function and that it is not enough to write, say,
trans(D) == /\ \A d \in D : s'[d] = 1 /\ \A d \in Dom \ D : UNCHANGED s[d]
because this does not uniquely define the domain of s' (for example, it could be a superset of the original domain). In fact, the above definition does not even specify that s' is a function. In principle, you could write something like
trans(D) == /\ s' \in [Dom -> 0 .. 10] /\ \A d \in D : s'[d] = 1 /\ \A d \in Dom \ D : UNCHANGED s[d]
but TLC is very inefficient in evaluating this definition because it would actually enumerate all possible functions and remove those that do not satisfy the formula in order to compute the only possible successor state.
Hope this helps, Stephan
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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<mod.tla><supermodule.tla>
|