使用Spin和Promela語法進行LTL模型檢查

Question

我試圖重現Dijkstra在標題爲「合作順序進程」的論文中編寫的ALGOL 60代碼，該代碼是第一次嘗試解決互斥問題，這裏是語法：

begin integer turn; turn:= 1; 
     parbegin 
     process 1: begin Ll: if turn = 2 then goto Ll; 
          critical section 1; 
          turn:= 2; 
          remainder of cycle 1; goto L1 
       end; 
     process 2: begin L2: if turn = 1 then goto L2; 
          critical section 2; 
          turn:= 1; 
          remainder of cycle 2; goto L2 
        end 
     parend 
end 

於是，我就重現PROMELA上面的代碼，這裏是我的代碼：

#define true 1 
#define Aturn true 
#define Bturn false 

bool turn, status; 

active proctype A() 
{ 
    L1: (turn == 1); 
    status = Aturn; 
    goto L1; 
    /* critical section */ 
    turn = 1; 

} 

active proctype B() 
{ 
    L2: (turn == 2); 
    status = Bturn; 
    goto L2; 
    /* critical section */ 
    turn = 2; 
} 

never{ /* ![]p */ 
    if 
    :: (!status) -> skip 
    fi; 
} 

init 
{ turn = 1; 
    run A(); run B(); 
} 

我想要做的是，驗證公平財產永遠不會舉行，因爲標籤L1無限運行。

這裏的問題是，我從來沒有要求塊未產生任何錯誤，輸出我得到的只是說，我的發言是從未達到過..

這裏是iSpin

spin -a dekker.pml 
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c 
./pan -m10000 
Pid: 46025 

(Spin Version 6.2.3 -- 24 October 2012) 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    - (not selected) 
    assertion violations + 
    cycle checks  - (disabled by -DSAFETY) 
    invalid end states + 

State-vector 44 byte, depth reached 8, errors: 0 
     11 states, stored 
     9 states, matched 
     20 transitions (= stored+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.291 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 


unreached in proctype A 
    dekker.pml:13, state 4, "turn = 1" 
    dekker.pml:15, state 5, "-end-" 
    (2 of 5 states) 
unreached in proctype B 
    dekker.pml:20, state 2, "status = 0" 
    dekker.pml:23, state 4, "turn = 2" 
    dekker.pml:24, state 5, "-end-" 
    (3 of 5 states) 
unreached in claim never_0 
    dekker.pml:30, state 5, "-end-" 
    (1 of 5 states) 
unreached in init 
    (0 of 4 states) 

pan: elapsed time 0 seconds 
No errors found -- did you verify all claims? 

實際輸出的

我已閱讀never{..}塊的所有旋轉文檔，但無法找到我的答案（這裏是link），我也嘗試過使用ltl{..}塊（link），但這只是給了我語法錯誤，甚至儘管它在文檔中明確提到它c一個在init和proctypes之外，有人可以幫我糾正這個代碼嗎？

謝謝

Answer 1

你已經重新定義了'真'，這不可能是好的。我摒棄了重新定義，從未聲稱失敗。但是，失敗對你的目標來說並不重要 - 最初的「地位」狀態是「虛假」的，因此永不退縮，這是失敗。

另外，將1或0賦值給bool是稍微糟糕的形式;改爲分配true或false - 或使用位。爲什麼不更緊密地遵循Dijkstra代碼 - 使用'int'或'byte'。性能不會成爲這個問題的一個問題。

如果你打電話給'跑' - 只是一個或另一個，你不需要'積極'。

我的 '過程1' 的翻譯是：

proctype A() 
{ 
L1: turn !=2 -> 
    /* critical section */ 
    status = Aturn; 
    turn = 2 
    /* remainder of cycle 1 */ 
    goto L1; 
} 

，但我可能是錯上。