Go to the first, previous, next, last section, table of contents.


3.2.10 Identifiers

An id, or identifier, is an expression which references an object. Objects are instances of modules, variables, and defined symbols. The syntax of an identifier is as follows.

id ::
        atom
        | "self"
        | id "." atom
        | id "[" simple_expr "]"

An atom identifies the object of that name as defined in a VAR or DEFINE declaration. If a identifies an instance of a module, then the expression `a.b' identifies the component object named `b' of instance `a'. This is precisely analogous to accessing a component of a structured data type. Note that an actual parameter of module `a' can identify another module instance `b', allowing `a' to access components of `b', as in the following example:

...  VAR
  a : foo(b);
  b : bar(a);
...

MODULE foo(x)
 DEFINE
   c := x.p | x.q;

MODULE bar(x)
 VAR
   p : boolean;
   q : boolean;

Here, the value of `c' is the logical or of `p' and `q'.

If `a' identifies an array, the expression `a[b]' identifies element `b' of array `a'. It is an error for the expression `b' to evaluate to a number outside the subscript bounds of array `a', or to a symbolic value.

It is possible to refer the name the current module has been instantiated to by using the self builtin identifier.

MODULE element(above, below, token)
 VAR
   Token : boolean;

 ASSIGN
   init(Token) := token;
   next(Token) := token-in;

 DEFINE
   above.token-in := Token;
   grant-out := below.grant-out;

MODULE cell
 VAR
   e2 : element(self,   e1, 0);
   e1 : element(e1  , self, 1);

 DEFINE
   e1.token-in := token-in;
   grant-out := grant-in & !e1.grant-out;

MODULE main
 VAR c1 : cell;

In this example the name the cell module has been instantiated to is passed to the submodule element. In the main module, declaring c1 to be an instance of module cell and defining above.token-in in module e2, really amounts to defining the symbol c1.token-in. When you, in the cell module, declare e1 to be an instance of module element, and you define grant-out in module e1 to be below.grant-out, you are really defining it to be the symbol c1.grant-out.



NuSMV <nusmv@irst.itc.it>