Promela Reference -- printf(4)


Basic Statement


printf - for printing text during random or guided simulation runs.

printf( string [ , arg_lst ] )
printm( name )



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 , in double quotes.

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

In addition, the white-space escape sequences \et (for a tab character) and \en (for a newline) are also recognized. Unlike the C version, optional width and precision fields are not supported.

The alternative form printm can be used to print just the symbolic name of an mtype constant. The two print commands in the following sequence, for instance, would both print the string pear :

The method using printf works only when Spin runs in simulation mode though, it does not work when an error trail is reproduced with the verifier (e.g., when embedded C code fragments are used). The alternative, using printm , always works.


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 as part of a straight execution. When Spin generates the verifier's source text, therefore, it replaces every call to printf with a special one that is called Printf . The latter function is only allowed to produce output during the replay of an error trace. This function can also be called from within embedded C code fragments, to suppress unwanted output during verification runs.

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. For instance, when the statement

is used, the string State Idle will included in the message sequence chart when this statement is reached.

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

These simulation breakpoints can be made conditional by embedding them into selection constructs. For instance:


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 23 December 2021)