Promela |
Basic Statement |
printf |
NAME
printf -
for printing text during random or guided simulation runs.
SYNTAX
printf( string [ , arg_lst ] )
printm( name )
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 , 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.
%c a single character, %d a decimal value, %e an mtype constant, %o an unsigned octal value, %u an unsigned integer value, %x a hexadecimal value.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 :
mtype = { apple, pear, orange }; mtype x = pear; printf("%e", x); printm(x);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.
EXAMPLES
printf("numbers: %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
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
printf("MSC: State Idle\n")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:
printf("MSC: BREAK\n")These simulation breakpoints can be made conditional by embedding them into selection constructs. For instance:
if :: P -> printf("MSC: BREAK\n") :: else /* no breakpoint */ fi
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 23 December 2021) |