About a type specifier in NuSMV (error: invalid subrange)

In the last paragraph, page # 23 of user manual 2.5 (I am using 2.5.4):

"A type specifier can be given by two expressions separated by .. (<TWO DOTS>). The two expressions have both to evaluate to constants integer numbers, and may contain names of defines and module formal parameters. For example, -1 - P1 .. 5 + D1, where P1 refers to a module formal parameter, and D1 refers to a define. Both P1 and D1 have to be statically evaluable to integer constants."

I have tested many different examples to run something like it but I couldn't finally. This is one of them:

MODULE main
VAR
    third_party : third_party;
    alice : alice(third_party.n); 

MODULE third_party
FROZENVAR
    p : 0..1000;
    q : 0..1000;
DEFINE 
    n := p * q;

MODULE alice(n)
FROZENVAR
    r :  1 .. n;

or something like this:

MODULE main
FROZENVAR
        p : 0..1000;
        q : 0..1000;
VAR
alice : alice(n);
    DEFINE 
        n := p * q;
MODULE alice(n)
    FROZENVAR
        r :  1 .. n;

The error is "invalid subrange 1 .. n"

Can anybody help me? Can you give me examples that type specifier contain names of defines and module formal parameters and run correctly?

Indeed this code is part of fiat-shamir protocol, and I am testing a ctl on different values of n (n cannot be a constant integer), and looking for a counterexample.

Solution

The problem is that third_party.n is not statically evaluable. It depends on the values of third_party.p and third_party.q, which are both variable. Therefore, the module is not instantiated with a statically evaluable expression.

An example that may work is:

MODULE main
VAR
    third_party : third_party;
    alice : alice(third_party.n); 

MODULE third_party
FROZENVAR
    p : 0..1000;
    q : 0..1000;
DEFINE 
    n := 10 * 10;

MODULE alice(n)
FROZENVAR
    r :  1 .. n;