predefined read-only channel.
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 on a Unix\(rg
system, to read input from the terminal or from a file.
An sample use of this feature is the following
word count program in Promela:
chan STDIN; /* requires Spin version 3.1 or later */
int c, nl, nw, nc;
bool inword = false;
:: STDIN?c ->
:: c == -1 -> break /* EOF */
:: c == '\n' -> nc++; nl++
:: else -> nc++
:: c == ' ' || c == '\t' || c == '\n' ->
inword = false
:: else ->
:: !inword ->
nw++; inword = true
:: else /* do nothing */
printf("%d\t%d\t%d\n", nl, nw, nc)
The STDIN channel is meant to be used only during simulation.
The name has no special semantics during verification.
A model checking run for the above example would report
an attempt to receive data from an unitialized channel.