parallel-processing - 是否可以检查 SPIN/PROMELA 中变量的最大值

Question

在我的模型检查代码中，我只对找到某个变量的最大值感兴趣。我现在采用的过程是有一个 assert 语句assert( var < MAX_VALUE )，并以二进制搜索方式不断更改 MAX_VALUE。但是，如果 SPIN 真的有办法在一次运行中给出变量的最大可能值，那就更好了。我知道 UPPAAL 有一个sup运营商。SPIN 中是否有任何等价物？

Answer 1

似乎不存在这样一个Promela具有max影响的运算符（涉及有限域，因此等效于sup）。

一种可能的方法是在探索状态空间时记录状态信息，例如通过Promela 规范中的嵌入式 C 代码。每当更改值时，嵌入式 C 代码会将 的值转储var到外部文件，var如下所示：

c_code{
    FILE *fp;
    int max_value;
}

连同一个inline：

int var;

inline set_var(value){
    var = value;
    c_code{
        fp = fopen("max_value.txt", "r");
        fscanf(fp, "%d", & max_value);
        fclose(fp);
        if (now.var > max_value){
            fp = fopen("max_value.txt", "w");
            fprintf(fp, max_value);
            fclose(fp);
        }

}

为了找到最大值，应该枚举整个状态空间，这取决于检查的是哪种属性，以及是否应用了偏序归约。

这种方法可以通过更有效地访问文件来改进。