NAME
STDIN - predefined read-only channel.

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 on a Unix\(rg system, to read input from the terminal or from a file.

EXAMPLES
An sample use of this feature is the following word count program in Promela:

chan STDIN;	/* requires Spin version 3.1 or later */



init {

        int c, nl, nw, nc;

        bool inword = false;



        do

        :: STDIN?c ->

                if

                :: c == -1 ->   break	/* EOF */

                :: c == '\n' -> nc++; nl++

                :: else ->      nc++

                fi;

                if

                :: c == ' ' || c == '\t' || c == '\n' ->

                        inword = false

                :: else ->

                        if

                        :: !inword ->

                                nw++; inword = true

                        :: else /* do nothing */

                        fi

                fi

        od;

        printf("%d\t%d\t%d\n", nl, nw, nc)

}.P2

NOTES 




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.

SEE ALSO 




chan(2), printf(4). 








Spin Online References


Promela Manual Index


Promela Grammar


Spin HomePage







(Page Updated: 16 December 1997)