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 ismemberSelf[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 cInit == c = 0Next == c' = c + 1====---- MODULE System ----CONSTANT PSetVARIABLE counterP(n) == INSTANCE Proc WITH c <- counter[n]Init == \A n \in PSet : P(n)!InitNext == \E n \in PSet : P(n)!Next====Unfortunately, a formula such as\A n \in 1..5 : counter[n] = 0does 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 PSetVARIABLE counterP(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 componentNext ==  /\ 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 PSetVARIABLE counterInit == 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,StephanOn 31 Aug 2018, at 17:48, Bekir Oguz wrote:Dear all,I am trying to write a spec (Cluster) which refers to n number of instances of another spec (Node) and getting a substitution error like this: In evaluation, the identifier memberSelf is either undefined or not an operator.line 17, col 37 to line 17, col 46 of module ClusterI am new to TLA and does not understand well how this instance substitutions work in general. Looks like, during the Init operator of Node, I try to set the prime value of self, and then the model checker tries to substitute the self value to memberSelf[n] then it fails.Source code could be found here:And the error trace is like this:In evaluation, the identifier memberSelf is either undefined or not an operator.line 18, col 37 to line 18, col 46 of module ClusterThe error occurred when TLC was evaluating the nestedexpressions at the following positions:0. CInit1. Line 21, column 10 to line 22, column 67 in Cluster2. Line 21, column 13 to line 21, column 42 in Cluster3. Line 21, column 30 to line 21, column 42 in Cluster4. Line 16, column 1 to line 19, column 63 in Cluster5. Line 54, column 9 to line 60, column 59 in Node6. Line 54, column 12 to line 54, column 51 in Node7. Line 10, column 22 to line 10, column 45 in Node8. Line 55, column 12 to line 55, column 26 in Node9. Line 55, column 12 to line 55, column 15 in Node10. Line 18, column 37 to line 18, column 49 in Cluster11. Line 18, column 37 to line 18, column 46 in ClusterThanks in advance,Bekir -- 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.