自旋和PROMELA工作

-1

首先，我总是达到深度的这个问题：0。我尝试了所有可能性。其次，我想达到ltl公式中提到的那些州。那么这个语法是否正确？ Screenshot 自旋和PROMELA工作

离开链接时做了一个内嵌图像 –

此外，您获得清晰的错误信息提示一个可能的解决方案。它是否试过跟随它，哪些值你尝试过什么是结果目前还不清楚。 –

@PatrickTrentin先生，我不知道该怎么做。请给我你的电子邮件ID。我想和你讨论一下。为什么深度达到0的问题一再出现。 –

关于错误

旋清楚地解释发生了什么事：

VECTORSZ太小，重新编译pan.c与-DVECTORSZ = N与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-03 07:19:37 DaveFar

Thank you so much sir @ DaveFar..this has so so helpful。 –

@Amrita Dahiya：我很高兴能够提供帮助。要将答案标记为已接受，请单击答案旁边的复选标记以将其从灰色变为填充。 – DaveFar

回答