Promela Reference -- for(3)

Promela

Control-Flow

for


NAME
for - deterministic iteration statement.

SYNTAX
for '(' varref ':' expr '..' expr ')' '{' sequence '}'
for '(' varref in array ')' '{' sequence '}'
for '(' varref in channel ')' '{' sequence '}'

DESCRIPTION
The for statement was added in Spin Version 6 to simplify writing common loops over a user-defined range of values, the elements of an array, or the messages currently stored in a channel. For statements are internally converted into the corresponding Promela code, with the first statement issued being an assignment statement. This means that for statements are always executable (the guard statement is an assignment), independent of what the guard of the sequence in the body of the for is. Execution could of course still block inside the body of the for statement.

Caution: if you use a macroname in a for statement, e.g., as in:

	int i;
	for (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.

EXAMPLES
The simplest form of the for statement is to simply iterate the execution of a given sequence of statements for a range of values, which must consist of two expressions separated by the two character token '..'. For instance,

	int i;

	for (i : 1 .. 10) {
		printf("i = %d\n", i)
	}
will print the numbers 1 through 10.

If instead of a range we give the basename of an array, then the index values of the array are generated. For instance,

	int a[10];
	int i;

	for (i in a) {
		printf("i = %d\n", i)
	}
will print the numbers 0 through 9 (note the difference with the first example).

The third use of the for statement is to retrieve all messages from a channel in sequence. To be able to do this the channel has to be defined in a special way, with a single user-defined type as its contents. The following example illustrates this use.

	typedef m {
		bool b;
		int i;
		chan c;
	}

	init {
		m foo;
		chan x = [8] of { m };
		int i;

		foo.b = true;
		foo.i = 12;
		foo.c = x;
		x!foo;

		foo.b = false;
		foo.i = 10;
		foo.c = 0;
		x!foo;

		i = 1;
		for (foo in x) {
			printf("%d: %d %d %d\n", i, foo.b, foo.i, foo.c);
			i++
		}
	}
The output will be:
	1: 1 12 1
	2: 0 10 0
The messages are read, but not removed from the channel.

For statements can be nested arbitrarily.

NOTES
The first example creates code that is identical to the following Promela fragment:

	i = 1;
	do
	:: i <= 10 -> printf("i = %d\n", i); i++
	:: else -> break
	od
The second example is equivalent to:
	i = 0;
	do
	:: i < 10 -> printf("i = %d\n", i); i++
	:: else -> break
	od
The for statement in the third example is equivalent to:
	i = 1; /* from the user code preceding the for */
	_tmp_ = 0;
	do
	:: _tmp_ < len(x) ->
		x?foo; x!foo;		/* rotate in place */
		printf(...); i++;  /* from the user code in the for body */
		_tmp_++
	:: else -> break
	od
Note that the message are retrieved one by one by removing them from the head of the channel buffer and reinserting them at the tail. After all messages are read, the state of the channel is the same as it was before the for statement is executed, provided no other processes tried to receive from or send to this channel while the for statement is being executed. If this is a possibility, it would be best to enclose the for in an atomic or d_step sequence (depending on whether the body of the for statement contains any non-deterministic constructs).

Note also that to be able to keep track of the count this third form of the for statement introduces an extra local variable (of type byte or short depending on the number of slots defined in the channel declaration.

SEE ALSO
do
if
select
atomic
d_step


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 4 March 2013)