首先，我总是遇到这个深度问题：0。我尝试了每一种可能性。其次，我想达到 ltl 公式中提到的那些状态。那么这种语法是否正确？
问问题
235 次
1 回答
1
关于错误
Spin 清楚地解释了正在发生的事情：
VECTORSZ 太小，用 -DVECTORSZ=N 重新编译 pan.c，N>1024；
中止（深度 0）
这就是为什么你得到
状态向量 1024 字节，深度达到 0，错误：1
所以我会尝试
gcc -DVECTORSZ=2048 -o pan pan.c
关于 LTL 公式
你有很多不必要的括号；你可以写得更简单：
<>( (m[7]==2) && (m[11]==1) && (m[20]==1) && (m[54]==1) & (m[57]==1) && (m[81]==1) )
所以你有一个相当大的数组m，这就解释了为什么你的 1024 字节的状态向量是不够的。比增加状态向量更好的解决方案是减小m如果您仍然可以m以某种方式抽象检查您感兴趣的属性的大小。
你写你“想要达到你的 ltl 公式中提到的那些状态”。为每条路径检查 ltl 公式，因此在每条路径上，最终都必须达到一个状态，在该状态下，逻辑合取的所有子句都必须保持。如果您想找到一条达到逻辑连词的所有子句都成立的状态的路径，请否定您的 ltl 公式，即 []（您的否定子句的析取），并查看（您的）反例路径以防万一这样的状态是可以达到的。
于 2017-09-03T07:19:37.257 回答