NAME
printf - for printing text during simulation runs.

SYNTAX
printf( string [ , arg_lst ] )

EXECUTABILITY
True

EFFECT
None

DESCRIPTION
A printf statement is similar to a skip statement in the sense that it is always executable and has no other effect on the state of the system than to change the control-state of the process that executes it. A useful side-effect of the statement is that it can print a string on the standard output stream during simulation runs. The Promela printf statement supports a subset of the options from its namesake in the programming language C. The first argument is an arbitrary string , deliminated by double quotes.

Five conversion specifications are recognized within the string. Upon printing each subsequent conversion specification is replaced with the value of the next argument in sequence, from the argument list that follows the string.

%c	a single character,

%d	a decimal value,

%o	an unsigned octal value,

%u	an unsigned integer value,

%x	a hexadecimal value.

EXAMPLES

printf("hello world\n")

printf("%d\t%d\n", (-10)%(-9), (-10)<<(-2))

NOTES
Printf statements are useful during simulation and debugging of a verification model. In verification, however, they are of no value, and therefore not normally enabled. The order in which printf s are executed during verification is determined by the depth-first search traversal of the reachability graph, which does not necessarily make sense if interpreted it as part of a straight execution.

SPECIAL NOTES ON XSPIN
The text printed by a printf statement that begins with the five characters: MSC: (three letters followed by a colon and a space) is automatically included in message sequence charts, e.g.

printf("MSC: State Idle\n")

It is also possible to set breakpoints for a random simulation when using Xspin. To do so, the text that follows the MSC: prefix must match the five characters: BREAK , as in:

printf("MSC: BREAK\n")

SEE ALSO
skip(1), if(3), do(3).