使用 Spin 进行 Promela 建模

Question

我正在研究一个相当简单的 promela 模型。使用两个不同的模块，它充当 crosswalk/Traffic 灯。第一个模块是输出当前信号（绿色、红色、黄色、未决）的交通灯。该模块还接收一个名为 "pedestrian" 的信号作为输入，该信号充当有行人想要过马路的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号（绿色、黄色、绿色）。它将行人信号输出到交通灯模块。该模块简单地定义了行人是否正在过马路、等待或不在场。我的问题是，一旦计数值达到 60，就会发生超时。我相信语句 "SigG_out ! 1" 导致了错误，但我不知道为什么。我附上了从命令行收到的跟踪图像。我对 Spin 和 Promela 是全新的，所以我不确定如何使用跟踪中的信息来查找我在代码中的问题。非常感谢任何帮助。

完整模型的代码如下：

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

您使用的 channels 不正确，特别是这一行我什至不知道如何解释它：

:: (sigG_in == 1) ->

你的通道是同步的，这意味着每当一个进程发送在一侧的东西时，另一个进程必须在频道的另一端收听才能传送消息。否则，进程阻塞直到情况发生变化。您的频道是 同步的 因为您声明它们的大小为 0.

要从频道读取，您需要使用正确的语法：

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

使用三个不同的通道发送不同的信号似乎有点没有意义。使用三个不同的值怎么样？

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

使用 Spin 进行 Promela 建模

Promela modeling with Spin

model-checking

spin

promela