我在使用PROMELA編寫的代碼時出現錯誤

Question

我正在使用ispin，並且出現錯誤提示自旋：在10個步驟之後結束並且轉換失敗。

如何防止發生此錯誤？

Answer 1

您防止錯誤兩種方式之一發生：

1. 解決您的PROMELA模式 - 你有你的PROMELA需要被移除
2. 你發現一個錯誤的一個bug 您正在建模的系統。恭喜。您現在將錯誤報告給您正在建模的系統負責人。

在實踐中，當你有一個線索指示錯誤，你接下來做

spin -p -t <name of the model>.pml 

將打印出步步模型執行導致的錯誤。你衝他們確認他們是正確的 - 如果是這樣，見上面的＃2;如果不正確，請參閱＃1。在覈查高級參數設置窗口

tab.I也增加物理內存爲2048：

Answer 2

我有同樣的問題，它是把-DVECTORSZ後固定。