select - non-deterministic value selection.
select '(' name ':' expr '..' expr ')'
The select statement was added in Spin Version 6 to simplify writing a standard selection of a non-deterministic value from a specified range of values. Select statements are internally converted into the corresponding Promela code, with the first statement issued being an assignment statement. This means that select statements are always executable (the guard statement is an assignment), but can take several steps to execute. More precisely, if there are N values in the range to choose from, then the select statement can take between 1 and N steps to arrive at the non-deterministically chosen value. The sequence of steps can be embedded in an atomic (but not in a d_step) to optimize the execution.
Caution 1: Because the select is implemented with a non-deterministic do-loop (making it possible to use expressions for the ranges that are evaluated at run-time), you will not get very random behavior in simulation runs. Note that each time through the loop, a random simulation will give equal odds to selecting the end of the loop or its continuation, until the upper-limit is reached. That means that values close to the start are much more likely to be picked in simulation runs than values close to the end. The behavior in verification runs is of course guaranteed to be correct, with all possible choices being verified.
Caution 2: if you use a macroname in a select statement, e.g., as in:
int i; select (i : 1 .. N);make sure that you use a space before the name, or else the C preprocessor will not replace the symbol and you'll get an 'undeclared variable N' error.
A simple example of the use of a select statement is as follows,
select (i : 8..17); assert(i >= 8 && i <= 17);which is expanded into the following Promela code fragment that can non-deterministically select any value in the range provided:
i = 8; do :: i < 17 -> i++ :: break od
Spin Online References
Promela Manual Index
|(Page updated: 4 September 2021)|