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

Re: [tlaplus] Problem with instance substitutions



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


On 31 Aug 2018, at 17:48, Bekir Oguz <beki...@xxxxxxxxx> 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 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:

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



--
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.