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

Question

在用户手册 2.5（我使用的是 2.5.4）的第 23 页的最后一段中：

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

我已经测试了很多不同的例子来 运行 类似的东西，但我做不到 最后。这是其中之一：

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;

或类似这样的内容：

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

错误是"invalid subrange 1 .. n"

有人可以帮助我吗？你能给我一些例子，类型说明符包含定义和模块形式参数的名称并且 运行 正确吗？

事实上这段代码是 fiat-shamir 协议的一部分，我正在测试一个 ctl 对不同的 n 值（n 不能是一个常数整数），并寻找一个反例。

Answer 1

问题是 third_party.n 不是静态可评估的。它取决于 third_party.p 和 third_party.q 的值，它们都是可变的。因此，该模块未使用可静态评估的表达式进行实例化。

一个可能有效的例子是：

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;