自旋proctype未得「 - 完 - 」

我在自旋模型檢查很新，想知道這是什麼錯誤意味着：自旋proctype未得「 - 完 - 」

unreached in proctype P1 
    ex2.pml:16, state 11, "-end-" 
    (1 of 11 states) 
unreached in proctype P2 
    ex2.pml:29, state 11, "-end-" 
    (1 of 11 states)

這裏是我的代碼：

int y1, y2; 
byte insideCritical; 

active proctype P1(){ 
do 
    ::true-> 
     y2 = y1 + 1; 
     (y1 == 0 || y2 < y1); 
     /* Entering critical section */ 
      insideCritical++; 
      assert(insideCritical < 2); 
      insideCritical--; 
     /* Exiting critical section */ 
     y2 = 0; 
od 
} 
active proctype P2(){ 
do 
    ::true-> 
     y1 = y2 + 1; 
     (y2 == 0 || y1 < y2); 
     /* Entering critical section */ 
      insideCritical++; 
      assert(insideCritical < 2); 
      insideCritical--; 
     /* Exiting critical section */ 
     y1 = 0; 
od 
}

它實際上不必結束，它是一個互斥程序，用於檢查兩個進程是否不在關鍵部分。錯誤是否意味着程序沒有結束？謝謝！

來源

2014-03-31 Javi

Spin通知您，您的proctypes永遠不會達到「結束」狀態，這當然是真實的，因爲它們由無限循環組成。如果這不是有意的行爲，那將是一個有用的信息。在你的情況，但是，你可能只是告訴旋轉，該計劃允許在該州最終通過添加結束標籤你的代碼對應的DO循環，例如：

active proctype P1(){ 
    endHere: 
    do 
    :: true-> 
    y2 = y1 + 1; 
    (y1 == 0 || y2 < y1); 
    /* Entering critical section */ 
     insideCritical++; 
     assert(insideCritical < 2); 
     insideCritical--; 
    /* Exiting critical section */ 
    y2 = 0; 
    od 
}

的結束標籤是以「結束」開頭的任何標籤。如果您的proctype以這種方式標記的狀態結束，Spin將不會向您顯示這些警告。

來源

2014-03-31 16:06:55 rindPHI

太好了！就像我想的那樣..謝謝！ – Javi

檢查的答案是一個很好的答案;通過適當地添加end標籤來明確是一種很好的形式。但是，它並不總是能夠做到這一點，因此，您可以通過與-n標誌運行pan驗證安靜SPIN：

-n : no listing of unreached states at the end of the run

來源

2014-04-09 14:36:53 GoZoner

自旋proctype未得「 - 完 - 」

回答

相關問題