एल टी एल मॉडल स्पिन और Promela सिंटैक्स का उपयोग

Question

मैं 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(); 
} 

मुझे क्या करना कोशिश कर रहा हूँ है, सत्यापित करें कि निष्पक्षता संपत्ति क्योंकि लेबल पकड़ कभी नहीं होगा एल 1 असीम चल रहा है।

यहां मुद्दा यह मेरी का दावा है कि कभी नहीं ब्लॉक किसी भी त्रुटि के उत्पादन नहीं है, उत्पादन मैं बस मिल का कहना है कि मेरे बयान कभी नहीं पहुँच गया था ..

यहाँ 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) लेकिन यह मुझे सिंटैक्स त्रुटि भी देता है हालांकि इसका स्पष्ट रूप से दस्तावेज़ीकरण में उल्लेख किया गया है कि यह सी init और proctypes के बाहर एक हो, क्या कोई मुझे इस कोड को सही करने में मदद कर सकता है?

धन्यवाद

Answer 1

आप नए सिरे से परिभाषित किया है 'सही' जो संभवतः अच्छा नहीं हो सकता। मैंने उस परिभाषा को धुंधला कर दिया और कभी दावा विफल नहीं हुआ। लेकिन, विफलता आपके लक्ष्य के लिए अनिवार्य है - कि 'स्थिति' की प्रारंभिक स्थिति 'झूठी' है और इस प्रकार कभी भी बाहर निकलने का दावा नहीं करता है, जो विफलता है।

इसके अलावा, यह एक बूल को 1 या 0 असाइन करने के लिए थोड़ा खराब रूप है; इसके बजाय सही या गलत असाइन करें - या बिट का उपयोग करें। डीजस्ट्रा कोड का अधिक बारीकी से पालन क्यों न करें - 'int' या 'बाइट' का उपयोग करें। ऐसा नहीं है कि इस समस्या में प्रदर्शन एक मुद्दा होगा।

यदि आप 'रन' कहने जा रहे हैं तो आपको 'सक्रिय' की आवश्यकता नहीं है - केवल एक या दूसरे।

'प्रक्रिया 1' का मेरा अनुवाद होगा:

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

लेकिन मैं उस पर गलत हो सकता है।