关于 NuSMV 中的类型说明符（错误：无效子范围）

Question

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

"类型说明符可以由两个用..分隔的表达式给出（）。 这两个表达式都必须计算为常量整数，并且 可能 包含定义和模块形式参数的名称。例如，-1 - P1 .. 5 + D1，其中P1指的是一个模块形参，D1指的是一个 定义。 P1 和 D1 都必须可以静态评估为整数常量。”

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

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;

错误是“无效的子范围 1 .. n”

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

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

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;