为什么 promela 模型超时?
Why is the promela model timing out?
我正在研究一个相当简单的 promela 模型。使用两个不同的模块,它充当 crosswalk/Traffic 灯。第一个模块是输出当前信号(绿色、红色、黄色、未决)的交通灯。该模块还接收一个名为 "pedestrian" 的信号作为输入,该信号充当有行人想要过马路的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号(绿色、黄色、绿色)。它将行人信号输出到交通灯模块。该模块简单地定义了行人是否正在过马路、等待或不在场。我的问题是,在 运行 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]
问题很容易发现,系统卡在这段代码中:
if
::(count >= 60) ->
sigG_out ! 1;
count = 0;
traffic_mode = green;
fi
如果 count
不大于或等于 60
会怎样?
进程无法执行(唯一的)分支,因为条件是false
,所以他们都停在那里等待它变成true
将来某个时候。
您应该提供一个替代分支,例如 else -> skip
,以便进程可以简单地通过 if ... fi
语句。
我正在研究一个相当简单的 promela 模型。使用两个不同的模块,它充当 crosswalk/Traffic 灯。第一个模块是输出当前信号(绿色、红色、黄色、未决)的交通灯。该模块还接收一个名为 "pedestrian" 的信号作为输入,该信号充当有行人想要过马路的指示器。第二个模块充当人行横道。它接收来自交通灯模块的输出信号(绿色、黄色、绿色)。它将行人信号输出到交通灯模块。该模块简单地定义了行人是否正在过马路、等待或不在场。我的问题是,在 运行 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]
问题很容易发现,系统卡在这段代码中:
if
::(count >= 60) ->
sigG_out ! 1;
count = 0;
traffic_mode = green;
fi
如果 count
不大于或等于 60
会怎样?
进程无法执行(唯一的)分支,因为条件是false
,所以他们都停在那里等待它变成true
将来某个时候。
您应该提供一个替代分支,例如 else -> skip
,以便进程可以简单地通过 if ... fi
语句。