1
我正在研究一個相當簡單的promela模型。使用兩個不同的模塊,它充當人行橫道/交通燈。第一個模塊是輸出當前信號的交通燈(綠色,紅色,黃色,待定)。該模塊還接收作爲輸入的稱爲「行人」的信號,該信號用作行人想穿過的指示器。第二個模塊充當人行橫道。它接收來自交通燈模塊的輸出信號(綠色,黃色,綠色)。它將行人信號輸出到交通燈模塊。這個模塊簡單地定義行人是否在穿越,等待或不在場。我的問題是,在Spin中運行模型時,一旦人行橫道開始執行其前幾個語句,它就會超時。我附加了從命令行收到的跟蹤圖像。我對Spin和Promela是全新的,因此我不完全確定如何使用跟蹤信息來查找代碼中的問題。任何幫助是極大的讚賞。爲什麼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]
感謝您的回答。這解決了超時。不過,我確實有另一個問題。一旦計數超過60,它想要做sigY_out! 1,但我收到錯誤「發送到未初始化的chan」。我猜這個變量連接到的通道在某種程度上是未初始化的。不完全確定如何解決這個問題。 – Flower
@花這很可能是因爲你的系統中有活動的進程,輸入變量初始化爲0.只需刪除'active'關鍵字即可。 –
當計數達到60時,現在它超時。 – Flower