为什么promela模型会超时？

Question

我正在研究一个相当简单的promela模型。使用两个不同的模块，它充当人行横道/交通灯。第一个模块是输出当前信号的交通灯（绿色，红色，黄色，待定）。该模块还接收作为输入的称为“行人”的信号，该信号用作行人想穿过的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色，黄色，绿色）。它将行人信号输出到交通灯模块。这个模块简单地定义行人是否在穿越，等待或不在场。我的问题是，在Spin中运行模型时，一旦人行横道开始执行其前几个语句，它就会超时。我附加了从命令行收到的跟踪图像。我对Spin和Promela是全新的，因此我不完全确定如何使用跟踪信息来查找代码中的问题。任何帮助是极大的赞赏。

下面是完整的模型代码：

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

的问题是很容易被发现，系统将陷在这个代码在这里：

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

什么如果count不大于或等于60会发生？

的过程不能执行（只）的分支，因为病情false，所以他们都停在那里等待它成为true在未来的一段时间。

您应该提供另一个分支，如else -> skip，这样进程可以简单地通过该if ... fi语句。