Spin model checker - Error: memory exhausted because of yacc stack size

Question

我创建了一个相当大的 Promela 模型（2362 个状态，其中总共有 29592 个转换），我想验证底层系统的 LTL 属性。模型在一个过程中全部定义如下：

int state=1;
bool p1a=true, p3=false, p1b=false;
active proctype model()
{
do
:: atomic{ state==1 -> state=1; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=4; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=5; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=6; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=133; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=134; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=136; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=137; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=138; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=265; p1a=true; p3=false; p1b=false }
:: atomic{ state==1 -> state=266; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=267; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=268; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=269; p1a=false; p3=false; p1b=false }
:: atomic{ state==1 -> state=270; p1a=false; p3=false; p1b=false }
:: atomic{ state==4 -> state=13; p1a=true; p3=false; p1b=false }
:: atomic{ state==4 -> state=14; p1a=false; p3=false; p1b=false }

.
. /* continues similarly */
.

:: atomic{ state==2376 -> state=1825; p1a=true; p3=true; p1b=false }
:: atomic{ state==2376 -> state=1837; p1a=true; p3=true; p1b=false }
od
}

ltl F {[]((p1a && p3) -> (<> p1b))}

您可以在这里找到整个文件：https://github.com/alevizada/bioFSA/blob/master/spin_files/abs_file_1.pml

当我运行:

spin -a filename.pml

我得到以下信息：

spin: filename.pml:19980, Error: memory exhausted   saw 'operator: ='
spin: filename.pml:19980, Error: no runable process saw 'operator: ='

查看.pml文件，相当于存储了19974个状态转移对

我在我的电脑和服务器上都试过了，所以我想系统内存不是问题。

旋转可以存储的这种对数是否有最大数量？如果是，如何解决并进行验证？

非常感谢！

编辑：似乎是解析器自旋正在使用 (yacc) 导致此问题。 yacc 分配一个具有 predefined/limited 内存的堆栈。我找到了关于如何更改它的 this 参考资料，但我不确定这些变量定义的文件应该在哪里。不过我怀疑是 y.tab.c。

有什么帮助吗？

谢谢！

解决方案

编辑 spin.y 中的以下行：

#define YYMAXDEPTH      20000

增加一个数字，然后重新安装 spin。它应该工作 :)

Answer 1

编辑 spin.y 中的以下行：

#define YYMAXDEPTH      20000

增加一个数字，然后重新安装 spin。它应该有效:)

Spin model checker - Error: memory exhausted because of yacc stack size

Spin model checker - Error: memory exhausted because of yacc stack size

memory

verification

model-checking

spin

promela

解决方案