Promela Modellierung mit Spin

Question

Ich arbeite an einem Promela-Modell, das 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, sobald der Zählwert auf 60 geht, ein Timeout auftritt. Ich glaube, dass die Aussage "SigG_out! 1" den Fehler verursacht, aber ich weiß nicht warum. 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 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; 
int 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 } 

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; 
     :: else -> skip; 
     fi 
     ::(traffic_mode == green) -> 
     if 
     ::(count < 60) -> 
      count = count + 1; 
     ::(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; 
     if 
     ::(count >= 60) -> 
      sigY_out ! 1; 
      count = 0; 
      traffic_mode = yellow; 
     ::else -> skip; 
     fi 
     ::(traffic_mode == yellow) -> 
     count = count + 1; 
     if 
     ::(count >= 5) -> 
      sigR_out ! 1; 
      count = 0; 
      traffic_mode = red; 
     :: else -> skip; 
     fi 
     fi 
od 

} 



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

} 

Answer 1

Sie verwenden channels falsch, diese Linie insbesondere würde ich nicht einmal wissen, wie sie interpretieren:

:: (sigG_in == 1) -> 

---

1. Ihre Kanäle sind Synchron, was bedeutet, dass immer dann, wenn ein Prozess sendet etwas auf der einen Seite, ein anderer Prozess am anderen Ende des Kanal, um die Nachricht zu überhören müssen. Ansonsten blockiert der Prozess bis sich die Situation ändert. Ihre Kanäle sind synchron, weil Sie sie der Größe 0 deklariert haben.

2. von einem Kanal zu lesen, müssen Sie die richtige Syntax verwenden:

   int some_var; 
   ... 
   some_channel?some_var; 
   // here some_var contains value received through some_channel 
   

---

Es scheint ein bisschen sinnlos verwenden drei verschiedene Kanäle, anders zu sein Signale senden . Wie wäre es mit drei verschiedenen Werten?

mtype = { RED, GREEN, YELLOW }; 
chan c = [0] of { mtype }; 
... 
c!RED 
... 
// (some other process) 
... 
mtype var; 
c?var; 
// here var contains RED 
...