Promela Reference -- scanf(6)

Promela

Omission

scanf


NAME
scanf - to read input from the standard input stream.

DESCRIPTION
There is no routine in Promela comparable to the C library function scanf to read input from the standard input stream or from a file or device. The reason is that Promela models must be closed to be verifiable. That is, all input sources must be part of the model. It is relatively easy to build a little process that acts as if it were the scanf routine, and that sends to user processes that request its services a non-deterministically chosen response from the set of anticipated responses.

As a small compromise, Promela does include a special predefined channel named STDIN that can be used to read characters from the standard input during simulation experiments. The use of STDIN is not supported in verification runs.

SEE ALSO
c_code
printf
STDIN


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)