The statements in the init
process's do loop are run in sequence.
do
:: true ->
level ! lvl;
lvl++;
(lvl > 9) -> break;
od
The very first time the do loop is run it will send lvl
over the level
channel, increase the lvl
(so it is now 1) and then test (lvl > 9)
. This is false so will block and causes the timeout.
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 will still not perform as expected. When lvl
is greater than 9 both options of the do loop are valid and either one can be chosen, so the loop will not necessarily break when lvl > 9
it could choose to continue to send the lvl
over the level
channel and increase lvl
.
You need to have a condition on the first do option as well as the second:
do
:: (lvl <= 9) ->
level ! lvl;
lvl++;
:: (lvl > 9) -> break;
od
It might be nicer to use the for loop 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 Sensor
's do loop, when the init
process has finished Sensor
will still try to read from the level
channel and timeout.