为什么promela模型超时了？

Question

我正在研究一个promela模型，它非常简单。它使用两个不同的模块，充当人行横道/交通灯。第一个模块是输出当前信号的交通灯(绿色、红色、黄色、挂起)。该模块还接收一个称为“行人”的信号作为输入，该信号作为一个指示符，表示有行人想要过马路。第二个模块充当人行横道。它接收来自交通灯模块(绿色、黄色、绿色)的输出信号。它将行人信号输出到交通灯模块。这个模块简单地定义了行人是否在过路、等待或不存在。我的问题是，在运行模型的旋转，它超时，一旦人行横道开始脚趾执行其最初的几个语句。我已经附加了从命令行接收到的跟踪的图像。我对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语句。