What causes Promela / SPIN timeout?
I have the following promela code:
chan level = [0] of {int};
proctype Sensor (chan levelChan) {
int x;
do
:: true ->
levelChan ? x;
if
:: (x < 2) -> printf("low %d", x);
:: (x > 8) -> printf("high %d", x);
:: else -> printf("normal %d", x);
fi
od
}
init {
run Sensor(level);
int lvl = 5;
level ! lvl;
lvl = 0;
do
:: true ->
level ! lvl;
lvl++;
(lvl > 9) -> break;
od
}
I am expecting to send level information (0-9) to the channel and receive the low | normal | high depending on this level. It's pretty straightforward. But why does SPIN talk about its timeout all the time?
0: proc - (:root:) creates proc 0 (:init:)
Starting Sensor with pid 1
1: proc 0 (:init:) creates proc 1 (Sensor)
1: proc 0 (:init:) 1.pml:18 (state 1) [(run Sensor(level))]
2: proc 1 (Sensor) 1.pml:6 (state 11) [(1)]
3: proc 0 (:init:) 1.pml:20 (state 2) [lvl = 5]
4: proc 0 (:init:) 1.pml:20 (state 3) [level!lvl]
4: proc 1 (Sensor) 1.pml:8 (state 2) [levelChan?x]
5: proc 1 (Sensor) 1.pml:9 (state 9) [else]
6: proc 0 (:init:) 1.pml:21 (state 4) [lvl = 0]
normal 5 8: proc 1 (Sensor) 1.pml:12 (state 8) [printf('normal %d',x)]
9: proc 0 (:init:) 1.pml:22 (state 10) [(1)]
12: proc 1 (Sensor) 1.pml:6 (state 11) [(1)]
13: proc 0 (:init:) 1.pml:24 (state 6) [level!lvl]
13: proc 1 (Sensor) 1.pml:8 (state 2) [levelChan?x]
14: proc 1 (Sensor) 1.pml:9 (state 9) [((x<2))]
low 0 15: proc 1 (Sensor) 1.pml:10 (state 4) [printf('low %d',x)]
17: proc 0 (:init:) 1.pml:25 (state 7) [lvl = (lvl+1)]
19: proc 1 (Sensor) 1.pml:6 (state 11) [(1)]
timeout
#processes: 2
19: proc 1 (Sensor) 1.pml:8 (state 2)
19: proc 0 (:init:) 1.pml:26 (state 8)
2 processes created
Seems to do only 1 iteration of the do loop?
source to share
Cycle statements init
are executed sequentially.
do
:: true ->
level ! lvl;
lvl++;
(lvl > 9) -> break;
od
The first time the do loop is executed, it will lvl
pipe level
, increment lvl
(so it is now 1) and then test (lvl > 9)
. This is not correct, so it blocks and timeouts.
To have multiple options in a do loop, you need to ::
define the start of each option:
do
:: true ->
level ! lvl;
lvl++;
:: (lvl > 9) -> break;
od
However, this still won't work as expected. When lvl
greater than 9, both parameters of the do loop are valid and one of them can be selected, so the loop will not necessarily break when lvl > 9
it can choose to continue sending lvl
on the level
channel and increment lvl
.
You must have a condition for the first do option as well as the second:
do
:: (lvl <= 9) ->
level ! lvl;
lvl++;
:: (lvl > 9) -> break;
od
It might be better to use the for for syntax for this example:
init {
run Sensor(level);
int lvl = 5;
level ! lvl;
for (lvl : 0..9){
level ! lvl;
}
}
Note that this example will still have a timeout error caused by the Sensor
do loop , when the process init
exits Sensor
will still try to read from the pipe level
and timeout.
source to share