LTL-Modellprüfung mit Spin und Promela Syntax

Question

Ich versuche ALGOL 60-Code von Dijkstra in der Arbeit mit dem Titel "Kooperierende sequentielle Prozesse" zu reproduzieren, der Code ist der erste Versuch, das Mutex-Problem zu lösen, hier ist die Syntax:

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 

Also versuchte ich den obigen Code in Promela zu reproduzieren und hier ist mein Code:

#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(); 
} 

Was ich versuche zu tun, stellen Sie sicher, dass die Fairness Eigenschaft wird nie, weil das Etikett halten L1 läuft unendlich.

Das hier Problem ist, dass mein nie Block Anspruch keinen Fehler erzeugt, der Ausgang ich einfach zu bekommen, sagt, dass meine Aussage nie erreicht wurde ..

hier ist die tatsächliche Ausgabe von 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? 

Ich habe alle Dokumentation von Spin auf dem never{..} Block gelesen, konnte aber meine Antwort nicht finden (hier ist die link), auch ich habe versucht mit ltl{..} Blöcke als auch (link), aber das gab mir nur Syntaxfehler, auch obwohl es ausdrücklich in der Dokumentation erwähnt wird, dass es c ein sein außerhalb der init und proctypes, kann mir jemand helfen, diesen Code bitte korrigieren?

Danke

Answer 1

Du hast ‚true‘ neu definiert, was unmöglich gut sein kann. Ich habe diese Neudefinition gestrichen, und der Anspruch niemals versagt. Aber das Scheitern ist für Ihr Ziel unerheblich - dieser Anfangszustand des "Status" ist "falsch" und daher gibt es niemals einen Anspruch auf einen Ausstieg, was ein Fehler ist.

Auch ist es eine schlechte Form, 1 oder 0 zu einem Bool zuzuweisen; true oder false stattdessen zuweisen - oder Bit verwenden. Warum folgen Sie dem Dijkstra-Code nicht genauer - verwenden Sie ein 'int' oder 'byte'. Es ist nicht so, dass Leistung ein Problem in diesem Problem sein wird.

Sie brauchen nicht 'aktiv', wenn Sie 'run' aufrufen - nur das eine oder das andere.

Meine Übersetzung von '-Prozess 1' wäre:

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

aber ich konnte auf das falsch sein.