如何將僞代碼更改爲NuSMV代碼？

Question

我的教授決定給我們數學學生一個代碼，以改變成NuSMV，我似乎無法找到其他任何地方的幫助，我閱讀的教科書只有6頁，只描述某些屬性。 Module main是NuSMV代碼的一個例子，他說用這個格式的例子來編寫僞代碼。 我不知道如何編寫while循環，並設置什麼是真實的？並將旗1成爲一個國家，併成爲另一個國家？

while(true) do 
    flag1 := true 
    while flag2 do 
    if turn=2 
     flag1 := false; 
     wait until turn = 1; 
     flag1 := true 
    Critical section 
    turn := 2 
    flag1 := false; 

Answer 1

它看起來像你試圖模擬德克爾/ Dijkstra算法互斥兩個過程之中。

步驟根據您的問題，應該只有1-4。我增加了一些更多的信息，以提供更全面的圖片，說明使用NuSMV可以實現什麼。

我使用了相同算法的稍微不同的版本，但其基本思想是相同的。

---

IDEA：存在的方法轉換僞代碼成NuSMV型號：

1. 標籤的進入和出口點的每個語句您的代碼：

   --  void p(iflag, turn, id) { 
   -- l0: while(true) do 
   -- l1:  flag := true 
   -- l2:  while iflag do 
   -- l3:  if turn != id 
   -- l4:   flag := false; 
   -- l5:   wait until turn = id; 
   -- l6:   flag := true 
   -- l7:  // Critical section 
   -- l8:  turn := 1 - id 
   -- l9:  flag := false; 
   --  } 
   

   請注意，一些陳述，例如while iflag do，可能有不止一個出口點取決於後衛的價值：如果iflag是真實的，那麼出口點L3，否則出口點L7。

2. 創建對應模塊，是以相同輸入並具有狀態變量，它的計算結果爲新引入的標籤。

   MODULE p(iflag, turn, id) 
   VAR 
       state : { l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, error }; 
       flag : boolean; 
   

   這裏，我添加了特殊的狀態錯誤通知。這只是爲了確保在定義期間狀態的轉換關係，我們不會遺漏任何正確的轉換步驟。一般來說，它應該被省略，因爲它不屬於原始代碼。

3. 定義的轉換關係爲狀態：

   ASSIGN 
       init(state) := l0; 
       next(state) := case 
       state = l0    : l1; 
       state = l1    : l2; 
       state = l2 & iflag  : l3; 
       state = l2 & !iflag  : l7; 
       state = l3 & turn != id : l4; 
       state = l3 & turn = id : l2; 
       state = l4    : l5; 
       state = l5 & turn != id : l5; 
       state = l5 & turn = id : l6; 
       state = l6    : l2; 
       state = l7    : l8; 
       state = l8    : l9; 
       state = l9    : l0; 
       TRUE     : error; -- if you match this then the above 
               -- description of transitions are incomplete 
       esac; 
   

   正如你所看到的，我只是每一個連接切入點與相應出口點。此外，只要超過一個出口點爲給定切入點定義我還添加了其他狀態條件，以確定哪些線接下來執行。

4. 添加的過渡關係爲標誌：

   init(flag) := FALSE; 
   next(flag) := case 
       state = l1 | state = l6 : TRUE; 
       state = l4 | state = l9 : FALSE; 
       TRUE     : flag; 
   esac; 
   

5. 添加一些定義來識別的代碼部分中的過程被執行：

   DEFINE 
       critical_section := (state = l7); 
       trying_section := (state = l1 | state = l2 | state = l3 | 
           state = l4 | state = l5 | state = l6); 
   

6. 創建主模塊這會創建兩個實例p：

   MODULE main() 
   VAR 
       turn : {0, 1}; 
       p1 : p(p2.flag, turn, 0); 
       p2 : p(p1.flag, turn, 1); 
   
   ASSIGN 
       init(turn) := 0; 
       next(turn) := case 
       p1.state = l8 : 1; 
       p2.state = l8 : 0; 
       TRUE   : turn; 
       esac; 
   

7. 添加一些非常典型互斥性通過模型檢查驗證：

   --*-- PROPERTIES --*-- 
   
   -- Safety: two processes are never in the critical section at the same time 
   CTLSPEC AG !(p1.critical_section & p2.critical_section); 
   
   -- Liveness: if a process is in the trying section, then sooner or later 
   --   it will access the critical section. 
   CTLSPEC AG (p1.trying_section -> AF p1.critical_section); 
   
   -- Absence of Starvation 
   CTLSPEC ! EF AG (p1.trying_section & p2.trying_section); 
   
   -- Never in Error State 
   CTLSPEC AG !(p1.state = error); 
   

8. 運行該工具

   ~$ NuSMV -int 
   

   ，並檢查所有屬性已驗證：

   NuSMV > reset; read_model -i dekker.smv; go; check_property 
   -- specification AG !(p1.critical_section & p2.critical_section) is true 
   -- specification AG (p1.trying_section -> AF p1.critical_section) is true 
   -- specification !(EF (AG (p1.trying_section & p2.trying_section))) is true 
   -- specification AG !(p1.state = error) is true 
   

---

注：

1. 如果在步驟和仔細一看，幾個州尋找多餘的。例如，總是可以摺疊只有一個入口和出口點的連續狀態。我會把這個留給你作爲練習。

2. 請注意，爲了簡單起見，我使用了模塊的同步組合。在實踐中，通過讓兩個進程異步運行，驗證會更有意義。但是，這需要使模型比您真正需要的問題更復雜，因此超出了我的答案範圍。

3. 如果您想了解更多關於NuSMV，你可以在它的documentation看看或者看看這個course的第二部分。