Warum läuft das Promela-Modell?

Question

Ich arbeite an einem Promela-Modell, das es ziemlich einfach ist. Mit zwei verschiedenen Modulen fungiert es als Zebrastreifen/Ampel. Das erste Modul ist die Ampel, die das aktuelle Signal ausgibt (grün, rot, gelb, anstehend). Dieses Modul empfängt auch ein Signal mit dem Namen "Fußgänger", das als Indikator dafür dient, dass Fußgänger durchqueren wollen. Das zweite Modul fungiert als der Zebrastreifen. Er empfängt Ausgangssignale vom Ampelmodul (grün, gelb, grün). Es gibt das Fußgängersignal an das Ampelmodul aus. Dieses Modul definiert einfach, ob der/die Fußgänger/-innen sich kreuzen, warten oder nicht anwesend sind. Mein Problem ist, dass nach dem Ausführen des Modells in Spin das Zeitlimit überschritten wird, sobald der Zebrastreifen seine ersten paar Anweisungen ausführt. Ich habe das Abbild der Ablaufverfolgung, die ich von der Befehlszeile erhalten habe, angehängt. Ich bin Spin und Promela völlig neu und daher bin ich mir nicht ganz sicher, wie ich die Informationen aus der Ablaufverfolgung verwenden soll, um mein Problem im Code zu finden. Jede Hilfe wird sehr geschätzt. Hier

ist der Code für das komplette Modell:

mtype = {red, green, yellow, pending, none, crossing, waiting}; 
mtype traffic_mode; 
mtype crosswalk_mode; 
byte count; 
chan pedestrian_chan = [0] of {byte}; 
chan sigR_chan = [0] of {byte}; 
chan sigG_chan = [0] of {byte}; 
chan sigY_chan = [0] of {byte}; 

ltl l1 {!<> (pedestrian_chan[0] == 1) && (traffic_mode == green || traffic_mode == yellow || traffic_mode == pending)} 
ltl l2 {[]<> (pedestrian_chan[0] == 1) -> crosswalk_mode == crossing } 

active proctype traffic_controller(chan pedestrian_in, sigR_out, sigG_out, sigY_out) 

{ 

do 
    ::if 
     ::(traffic_mode == red) -> 
     count = count + 1; 
     if 
     ::(count >= 60) -> 
      sigG_out ! 1; 
      count = 0; 
      traffic_mode = green; 
     fi 
     ::(traffic_mode == green) -> 
     if 
     ::(count < 60) -> 
      count = count + 1; 
      traffic_mode = green; 
     ::(pedestrian_in == 1 & count < 60) -> 
      count = count + 1; 
      traffic_mode = pending; 
     ::(pedestrian_in == 1 & count >= 60) 
      count = 0; 
      traffic_mode = yellow; 
     fi 
     ::(traffic_mode == pending) -> 
     count = count + 1; 
     traffic_mode = pending; 
     if 
     ::(count >= 60) -> 
      sigY_out ! 1; 
      count = 0; 
      traffic_mode = yellow; 
     fi 
     ::(traffic_mode == yellow) -> 
     count = count + 1; 
     traffic_mode = yellow; 
     if 
     ::(count >= 5) -> 
      sigR_out ! 1; 
      count = 0; 
     fi 
     fi 
od 

} 



active proctype crosswalk(chan sigR_in, sigG_in, sigY_in, pedestrian_out) 

{ 
do 
    ::if 
     ::(crosswalk_mode == crossing) -> 
     if 
     ::(sigG_in == 1) -> crosswalk_mode = none; 
     fi 
     ::(crosswalk_mode == none) -> 
     if 
     :: (1 == 1) -> crosswalk_mode = none; 
     :: (1 == 1) -> 
      pedestrian_out ! 1; 
      crosswalk_mode = waiting; 
     fi 
     ::(crosswalk_mode == waiting) -> 
     if 
     ::(sigR_in == 1) -> crosswalk_mode = crossing; 
     fi 
     fi 
od 
} 
init 

{ 
    count = 0; 
    traffic_mode = red; 
    crosswalk_mode = crossing; 

    atomic 
    { 
     run traffic_controller(pedestrian_chan, sigR_chan, sigG_chan, sigY_chan); 
     run crosswalk(sigR_chan, sigG_chan, sigY_chan, pedestrian_chan); 
    } 
} 


[![enter image description here][1]][1] 

Answer 1

Das Problem ist sehr leicht zu erkennen, wird das System in diesem Code hier fest:

if 
    ::(count >= 60) -> 
     sigG_out ! 1; 
     count = 0; 
     traffic_mode = green; 
    fi 

was passiert, wenn count nicht größer oder gleich ist 60?

Die Prozesse können den (nur) Zweig nicht ausgeführt werden, weil die Bedingung false ist, so dass sie beide dort anhalten gewartet es true einige Zeit in der Zukunft zu werden.

Sie sollten einen alternativen Zweig wie else -> skip bereitstellen, damit die Prozesse einfach über diese if ... fi Anweisung hinausgehen können.