| Hello Bekir, the specific issue that TLC complains about is that when evaluating the initial-state predicate in module Node (instantiated in Cluster), the second conjunct is memberSelf[n] = n (where n is bound to an element of set nodes). The evaluation fails because the variable `memberSelf' has not yet been assigned a value in the initial state that TLC is currently constructing. When evaluating an initial condition, TLC interprets an equality "variable = _expression_" as an assignment if `variable' has not yet been assigned a value. However, your equality is not of that form: the left-hand side is not just a variable. More generally, the approach that you chose for specifying your system will not work. Let me illustrate the problem using a very simple example where you have a finite set of processes, each of which uses a counter variable. It may be tempting to try and specify the system as follows: ---- MODULE Proc ---- VARIABLE c Init == c = 0 Next == c' = c + 1 ==== ---- MODULE System ---- CONSTANT PSet VARIABLE counter P(n) == INSTANCE Proc WITH c <- counter[n] Init == \A n \in PSet : P(n)!Init Next == \E n \in PSet : P(n)!Next ==== Unfortunately, a formula such as \A n \in 1..5 : counter[n] = 0 does not unambiguously describe the value that the variable counter should have. For example, it is satisfied by all sequences <<0, 0, ..., 0>> whose length is at least 5. Even more, TLA+ does not specify the values of `42[0]' or `{1,2,3}[0]', and we do not know if the formula evaluates to true or false when counter = 42 or counter = {1,2,3}. Not only is TLC not clever enough to compute the right initial value, but the specification is too weak for characterizing the set of such values. The case of the next-state relation is even worse: the above specification only says that some counter component gets incremented but does not constrain at all the behavior of the other counter components. You could in principle correct these problems as follows: ---- MODULE System ---- CONSTANT PSet VARIABLE counter P(n) == INSTANCE Proc WITH c <- counter[n] Init == /\ counter \in [PSet -> Nat] \* fix the shape of the overall value /\ \A n \in PSet : P(n)!Init \* initialize each component Next == /\ counter' \in [PSet -> Nat] \* fix the shape of the value in the next state /\ \E n \in PSet : P(n)!Next \* let one process do its step ... /\ \A m \in PSet \ {n} : UNCHANGED P(m)!c \* and constrain the other processes to stutter ==== However, now TLC will complain about being unable to enumerate the (infinite) set [PSet -> Nat]. It will work if you replace Nat by a finite set, but state computation will be extremely inefficient because TLC will first enumerate all sets of suitable functions and then filter out those that satisfy the specification. In practice, it is best to give up on the idea of specifying processes individually in a base module and specify the composition (and interaction) of these processes in a main module that instantiates the base module. We will rather want to write something like the following (and similarly for your specification): ---- MODULE System ---- CONSTANT PSet VARIABLE counter Init == counter = [n \in PSet |-> 0] Inc(n) == counter' = [counter EXCEPT ![n] = @+1] Next == \E n \in PSet : Inc(n) ==== Note that both the initialization and the update using the EXCEPT operate on entire arrays (functions) rather than on individual array positions. Chapter 10 of "Specifying Systems" discusses the issue of composing specifications in much detail. Hope this helps, Stephan
|