scanf - to read input from the standard input stream.
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.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|