Promela |
Declarator |
show |
NAME
show -
to allow for tracking of the access to specific variables
in message sequence charts.
DESCRIPTION
This keyword has no semantic content. It only serves to
determine which variables should be tracked and included
in message sequence chart displays in the Xspin tool.
Updates of the value of all variables that are declared
with this prefix are maintained visually, in a separate
process line, in these message sequence charts.
NOTES
The use of this prefix only affects the information that Xspin
includes in message sequence charts, and the information that Spin
includes in Postscript versions of message sequence charts under
Spin option
-M .
SEE ALSO
datatypes
hidden
local
show
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |