[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Problem with instance substitutions



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 Cluster

I 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:
https://github.com/ing-bank/baker/blob/781c999602375526e9702c85d610d350aa7fe4de/tla/Cluster.tla 
https://github.com/ing-bank/baker/blob/781c999602375526e9702c85d610d350aa7fe4de/tla/Node.tla 

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 Cluster


The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. CInit

1. Line 21, column 10 to line 22, column 67 in Cluster

2. Line 21, column 13 to line 21, column 42 in Cluster

3. Line 21, column 30 to line 21, column 42 in Cluster

4. Line 16, column 1 to line 19, column 63 in Cluster

5. Line 54, column 9 to line 60, column 59 in Node

6. Line 54, column 12 to line 54, column 51 in Node

7. Line 10, column 22 to line 10, column 45 in Node

8. Line 55, column 12 to line 55, column 26 in Node

9. Line 55, column 12 to line 55, column 15 in Node

10. Line 18, column 37 to line 18, column 49 in Cluster

11. Line 18, column 37 to line 18, column 46 in Cluster



Thanks in advance,

Bekir