SPIN驗證：不能證明LTL式

Question

我有相當simpe發送器 - 接收協議：

#define SZ 4 
int sent = 0; 
int received = 0; 
chan ch = [SZ] of {int}; 
int varch; 
init { 
    do 
    :: ((len(ch) < SZ) && (received != 1)) -> 
     d_step { 
     ch ! 1; sent = 1; printf("sent\n"); 
    } 
    :: ((len(ch) == SZ) || ((received == 1) && (len(ch) > 0))) -> 
    d_step { 
     ch ? varch; received = 1; printf("received\n"); 
    } 
    :: 1 -> /* simulates ramdomness */ 
     atomic { 
      printf("timeout1\n");/*break; */ 
    } 
    od; 
} 

它發送四個包，然後接收它們。然後我試圖證明屬性：總是發送意味着最終得到：

零擔PR {[（（發送== 1） - >（<>（收到== 1）））}

...什麼也沒有發生：SPIN沒有找到這個屬性證明和它的否定。

爲什麼？

Answer 1

因此，通過快速檢查，LTL財產不可能得到滿足。零擔物業包括always，但一個可行的執行是do::od聲明永遠採取/* simulates randomness */選項。在這種情況下，將不會收到隊列，並且LTL失敗。

我SPIN運行證實了上面的（我把你的代碼放到一個文件 'sr.pml'）

$ spin -a sr.pml 
$ gcc -o pan pan.c 
$ ./pan -a 
pan:1: acceptance cycle (at depth 16) 
pan: wrote sr.pml.trail 

(Spin Version 6.3.2 -- 17 May 2014) 
Warning: Search not completed 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (pr) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 60 byte, depth reached 20, errors: 1 
     12 states, stored (14 visited) 
     0 states, matched 
     14 transitions (= visited+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.001 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.290 actual memory usage for states 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    128.730 total actual memory usage 



pan: elapsed time 0 seconds 

，然後我們可以看到與路徑：

$ spin -p -t sr.pml 
ltl pr: [] ((! ((sent==1))) || (<> ((received==1)))) 
starting claim 1 
using statement merging 
Never claim moves to line 4 [(1)] 
    2: proc 0 (:init::1) sr.pml:8 (state 1) [(((len(ch)<4)&&(received!=1)))] 
    4: proc 0 (:init::1) sr.pml:9 (state 5) [ch!1] 
    4: proc 0 (:init::1) sr.pml:10 (state 3) [sent = 1] 
      sent 
    4: proc 0 (:init::1) sr.pml:10 (state 4) [printf('sent\\n')] 
Never claim moves to line 3 [((!(!((sent==1)))&&!((received==1))))] 
    6: proc 0 (:init::1) sr.pml:8 (state 1) [(((len(ch)<4)&&(received!=1)))] 
Never claim moves to line 8 [(!((received==1)))] 
    8: proc 0 (:init::1) sr.pml:9 (state 5) [ch!1] 
    8: proc 0 (:init::1) sr.pml:10 (state 3) [sent = 1] 
      sent 
    8: proc 0 (:init::1) sr.pml:10 (state 4) [printf('sent\\n')] 
10: proc 0 (:init::1) sr.pml:8 (state 1) [(((len(ch)<4)&&(received!=1)))] 
12: proc 0 (:init::1) sr.pml:9 (state 5) [ch!1] 
12: proc 0 (:init::1) sr.pml:10 (state 3) [sent = 1] 
      sent 
12: proc 0 (:init::1) sr.pml:10 (state 4) [printf('sent\\n')] 
14: proc 0 (:init::1) sr.pml:8 (state 1) [(((len(ch)<4)&&(received!=1)))] 
16: proc 0 (:init::1) sr.pml:9 (state 5) [ch!1] 
16: proc 0 (:init::1) sr.pml:10 (state 3) [sent = 1] 
      sent 
16: proc 0 (:init::1) sr.pml:10 (state 4) [printf('sent\\n')] 
    <<<<<START OF CYCLE>>>>> 
18: proc 0 (:init::1) sr.pml:16 (state 11) [(1)] 
      timeout1 
20: proc 0 (:init::1) sr.pml:18 (state 12) [printf('timeout1\\n')] 
spin: trail ends after 20 steps 
#processes: 1 
     sent = 1 
     received = 0 
     queue 1 (ch): [1][1][1][1] 
     varch = 0 
20: proc 0 (:init::1) sr.pml:7 (state 14) 
20: proc - (pr:1) _spin_nvr.tmp:7 (state 10) 
1 processes created 

的<<<<<START OF CYCLE>>>>節目第16行的sr.pml（:: 1 -> ...）永久執行。此外，LTL還存在其他故障。使用'./pan -a -i'運行SPIN搜索以查找最短路徑;這表明您的LTL沒有找到您想要查找的內容。