自旋和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

回答