如何在promela/SP中對此代碼進行建模？

Question

以下算法嘗試在兩個進程P1和P2之間實施互斥 ，每個進程都運行下面的代碼。 你可以假設最初SEMA = 0

while true do{ 
atomic{if sema = 0 
then sema:= 1 
else 
go to line 2} 
critical section; 
sema:= 0; 
    } 

我如何能在PROMELA/SPIN這個代碼模型？

謝謝。

Answer 1

這應該是相當簡單：

active proctype P() { 
    bit sema = 0; 

    do 
    :: atomic { 
     sema == 0 -> sema = 1 
     } 

     // critical section 

     sema = 0 
    od 
} 

也許你不需要do循環，如果你的代碼只需要它的一些積極的等待。原子塊只有在sema設置爲0時纔可執行，然後立即執行。 Spin有一個內置的被動等待語義。