Can anyone explain to me the order of what happens in the following?
if
:: a_channel??5 -> // do A
:: value_1 == value_2 -> // do B
fi;
So basically how I understand it is that for the statement to be executable, 5 needs to be in the channel. I understand that 5 will then be removed from the channel as a result(if it is indeed in the channel). What I don't undertstand is when 5 will be removed. Will 5 be removed after the statement is executed or will it be removed before during the check for execution.
Promela ref link for receiving: http://spinroot.com/spin/Man/receive.html
Assume a_channel??5 is contained in the body of some process P_i.
Will 5 be removed after the statement is executed or will it be removed before during the check for execution.
The "check for execution" is a necessary but not sufficient condition for the removal of 5 from the channel. The other, necessary, condition is that P_i is selected for execution and executes the statement a_channel??5.
A more detailed answer.
The statement a_channel??5 is a statement that it is not always executable. It is executable only when 5 is in channel. (e.g. if 5 was in the channel, but it has been removed [e.g. by someone else], a_channel??5 is no longer executable)
After each time a process P_i executes an atomic (set of) instruction(s), the scheduler may decide to pre-empt it and to allow some other process P_j with some executable instruction to continue.
When a process P_i reaches a non-executable statement, it is always immediately pre-empted by the scheduler. In this case, it is an error condition if there is no other process P_j with some immediately executable instruction that can be scheduled for execution (i.e. the famous "invalid end state" error).
If statement a_channel??5 is executable and process P_i is selected for execution (or keeps going), then a_channel??5 executes atomically and it immediately removes the (first occurrence) of the value 5 from the channel.