SPIN：解釋錯誤跟蹤

我試圖解決與農民，狼，山羊和捲心菜有關的任務。SPIN：解釋錯誤跟蹤

所以，我發現瞭如下因素PROMELA描述：

#define fin (all_right_side == true) 
#define wg (g_and_w == false) 
#define gc (g_and_c == false) 

ltl ltl_0 { <> fin && [] (wg && gc) } 

bool all_right_side, g_and_w, g_and_c; 
active proctype river() 
{ 
bit f = 0, 
w = 0, 
g = 0, 
c = 0; 

all_right_side = false; 
g_and_w = false; 
g_and_c = false; 
printf("MSC: f %c w %c g %c c %c \n", f, w, g, c); 

do 
:: (f==1) && (f == w) && (f ==g) && (f == c) -> 
     all_right_side = true; 
     break; 
:: else -> 
     if 
      :: (f == w) -> 
        f = 1 - f; 
        w = 1 - w; 
      :: (f == c) -> 
        f = 1 - f; 
        w = 1 - c; 
      :: (f == g) -> 
        f = 1 - f; 
        w = 1 - g; 
      :: (true) -> 
        f = 1 - f; 
     fi; 

     printf("M f %c w %c g %c c %c \n", f, w, g, c); 

     if 
      :: (f != g && g == c) -> 
        g_and_c = true; 
      :: (f != g && g == w) -> 
        g_and_w = true; 
      ::else -> 
        skip 
     fi 
od; 

printf ("MSC: OK!\n") 
}

我添加有一個LTL-式：LTL ltl_0 {<>鰭& & []（WG & & GC）} 驗證，狼不會吃山羊，山羊不會吃白菜。我想要舉一個例子，農民如何運輸他所有的需求（w-g-c）而不損失。

當運行驗證時，得到以下結果：狀態矢量20字節，深度達到59，錯誤：1 64個狀態，存儲 23個州，匹配 87轉變（=存儲+匹配） 0原子步驟散列衝突：0（已解決）

這意味着該程序爲我生成了一個示例。但我無法解釋它。 * .pml.trial文件的內容是：enter image description here

請幫我解釋。

來源

2017-01-03 julitta_94

爲了「解釋」它，你可以使每一個採取行動的東西intellegibile時間打印在標準輸出修改你的源代碼。

例如爲：

  :: (f == w) -> 
        if 
         :: f == 0 -> printf("LEFT ---[farmer, wolf]--> RIGHT\n"); 
         :: f == 1 -> printf("LEFT <--[farmer, wolf]--- RIGHT\n"); 
         :: else -> skip; 
        fi; 
        f = 1 - f; 
        w = 1 - w;

+的情況下(f == c)，(f == g)和(true)類似的東西。

注：你的源代碼已經提供printf("M f %c w %c g %c c %c \n", f, w, g, c);，可如果你記住，0意味着left和1意味着right用於解釋的反例。儘管如此，我寧願更多的詳細的跟蹤。

你做的每一個可能的過渡在此之後，你可以看到你反例內發生的事情通過運行旋下列方式

~$ spin -t file_name.pml

選項-t重播的最新trail發現旋在違反一些斷言/財產。

來源

2017-01-03 12:31:18

有幾種方法可以解釋跟蹤。

使用iSpin：
- 去模擬/在播放模式
- ，選擇引導並輸入您的跟蹤文件的名稱
- 運行

這將逐步顯示每個進程所採取的行動，包括諸如進程號，實例類型名稱，行號麻煩等信息執行指令，執行指令代碼。

做同樣的旋轉：
使用命令

spin -t -p xyz.pml

理解跟蹤文件的語法：
在文件中的每個行是一個一步由模擬器採取。第一欄只是序號。第二列是進程號（pids）。（例如，init將爲0，它啓動/運行的第一個進程將爲1，依此類推。）第三列是轉換編號。如果你只想知道發生了什麼，你可以看看pid，然後閱讀說明書

來源

2017-10-03 10:56:40

SPIN：解釋錯誤跟蹤

回答

相關問題