Promela |
Predefined |
STDIN |
NAME
STDIN -
predefined read-only channel, for use in simulation.
SYNTAX
chan STDIN; STDIN?var
DESCRIPTION
During simulation runs, it is sometimes useful to be able
to connect Spin to other programs that can produce useful
input, or directly to the standard input stream
to read input from the terminal or from a file.
EXAMPLES
A sample use of this feature is this model of a word count program:
chan STDIN; /* no channel initialization */ init { int c, nl, nw, nc; bool inword = false; do :: STDIN?c -> if :: c == -1 -> break /* EOF */ :: c == '\en' -> nc++; nl++ :: else -> nc++ fi; if :: c == ' ' || c == '\et' || c == '\en' -> inword = false :: else -> if :: !inword -> nw++; inword = true :: else /* do nothing */ fi fi od; printf("%d\t%d\t%d\n", nl, nw, nc) }
NOTES
The STDIN channel can be used only in simulations.
The name has no special meaning in verification.
A verification for the example model would report
an attempt to receive data from an unitialized channel.
SEE ALSO
chan
poll
printf
receive
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |