1 /* VERSION 1 introduces plumbing
2 	2 increases SNARFSIZE from 4096 to 32000
3  */
4 #define	VERSION	2
5 
6 #define	TBLOCKSIZE 512		  /* largest piece of text sent to terminal */
7 #define	DATASIZE  (UTFmax*TBLOCKSIZE+30) /* ... including protocol header stuff */
8 #define	SNARFSIZE 32000		/* maximum length of exchanged snarf buffer, must fit in 15 bits */
9 /*
10  * Messages originating at the terminal
11  */
12 typedef enum Tmesg
13 {
14 	Tversion,	/* version */
15 	Tstartcmdfile,	/* terminal just opened command frame */
16 	Tcheck,		/* ask host to poke with Hcheck */
17 	Trequest,	/* request data to fill a hole */
18 	Torigin,	/* gimme an Horigin near here */
19 	Tstartfile,	/* terminal just opened a file's frame */
20 	Tworkfile,	/* set file to which commands apply */
21 	Ttype,		/* add some characters, but terminal already knows */
22 	Tcut,
23 	Tpaste,
24 	Tsnarf,
25 	Tstartnewfile,	/* terminal just opened a new frame */
26 	Twrite,		/* write file */
27 	Tclose,		/* terminal requests file close; check mod. status */
28 	Tlook,		/* search for literal current text */
29 	Tsearch,	/* search for last regular expression */
30 	Tsend,		/* pretend he typed stuff */
31 	Tdclick,	/* double click */
32 	Tstartsnarf,	/* initiate snarf buffer exchange */
33 	Tsetsnarf,	/* remember string in snarf buffer */
34 	Tack,		/* acknowledge Hack */
35 	Texit,		/* exit */
36 	Tplumb,		/* send plumb message */
37 	TMAX
38 }Tmesg;
39 /*
40  * Messages originating at the host
41  */
42 typedef enum Hmesg
43 {
44 	Hversion,	/* version */
45 	Hbindname,	/* attach name[0] to text in terminal */
46 	Hcurrent,	/* make named file the typing file */
47 	Hnewname,	/* create "" name in menu */
48 	Hmovname,	/* move file name in menu */
49 	Hgrow,		/* insert space in rasp */
50 	Hcheck0,	/* see below */
51 	Hcheck,		/* ask terminal to check whether it needs more data */
52 	Hunlock,	/* command is finished; user can do things */
53 	Hdata,		/* store this data in previously allocated space */
54 	Horigin,	/* set origin of file/frame in terminal */
55 	Hunlockfile,	/* unlock file in terminal */
56 	Hsetdot,	/* set dot in terminal */
57 	Hgrowdata,	/* Hgrow + Hdata folded together */
58 	Hmoveto,	/* scrolling, context search, etc. */
59 	Hclean,		/* named file is now 'clean' */
60 	Hdirty,		/* named file is now 'dirty' */
61 	Hcut,		/* remove space from rasp */
62 	Hsetpat,	/* set remembered regular expression */
63 	Hdelname,	/* delete file name from menu */
64 	Hclose,		/* close file and remove from menu */
65 	Hsetsnarf,	/* remember string in snarf buffer */
66 	Hsnarflen,	/* report length of implicit snarf */
67 	Hack,		/* request acknowledgement */
68 	Hexit,
69 	Hplumb,		/* return plumb message to terminal - version 1 */
70 	HMAX
71 }Hmesg;
72 typedef struct Header{
73 	uchar	type;		/* one of the above */
74 	uchar	count0;		/* low bits of data size */
75 	uchar	count1;		/* high bits of data size */
76 	uchar	data[1];	/* variable size */
77 }Header;
78 
79 /*
80  * File transfer protocol schematic, a la Holzmann
81  * #define N	6
82  *
83  * chan h = [4] of { mtype };
84  * chan t = [4] of { mtype };
85  *
86  * mtype = {	Hgrow, Hdata,
87  * 		Hcheck, Hcheck0,
88  * 		Trequest, Tcheck,
89  * 	};
90  *
91  * active proctype host()
92  * {	byte n;
93  *
94  * 	do
95  * 	:: n <  N -> n++; t!Hgrow
96  * 	:: n == N -> n++; t!Hcheck0
97  *
98  * 	:: h?Trequest -> t!Hdata
99  * 	:: h?Tcheck   -> t!Hcheck
100  * 	od
101  * }
102  *
103  * active proctype term()
104  * {
105  * 	do
106  * 	:: t?Hgrow   -> h!Trequest
107  * 	:: t?Hdata   -> skip
108  * 	:: t?Hcheck0 -> h!Tcheck
109  * 	:: t?Hcheck  ->
110  * 		if
111  * 		:: h!Trequest -> progress: h!Tcheck
112  * 		:: break
113  * 		fi
114  * 	od;
115  * 	printf("term exits\n")
116  * }
117  *
118  * From: gerard@research.bell-labs.com
119  * Date: Tue Jul 17 13:47:23 EDT 2001
120  * To: rob@research.bell-labs.com
121  *
122  * spin -c 	(or -a) spec
123  * pcc -DNP -o pan pan.c
124  * pan -l
125  *
126  * proves that there are no non-progress cycles
127  * (infinite executions *not* passing through
128  * the statement marked with a label starting
129  * with the prefix "progress")
130  *
131  */