to read input from the standard input stream.
There is no routine in Promela to read input from
the standard input stream or from any file or device.
The reason is that Promela models must be
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
routine, and that sends to user processes that request
its services a non-deterministically chosen response
from the set of anticipated responses.