1 /* VERSION 1 introduces plumbing
2 2 increases SNARFSIZE from 4096 to 32000
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 */
10 * Messages originating at the terminal
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 */
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 */
36 Tplumb, /* send plumb message */
40 * Messages originating at the host
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 */
69 Hplumb, /* return plumb message to terminal */
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 */
80 * File transfer protocol schematic, a la Holzmann
83 * chan h = [4] of { mtype };
84 * chan t = [4] of { mtype };
86 * mtype = { Hgrow, Hdata,
91 * active proctype host()
95 * :: n < N -> n++; t!Hgrow
96 * :: n == N -> n++; t!Hcheck0
98 * :: h?Trequest -> t!Hdata
99 * :: h?Tcheck -> t!Hcheck
103 * active proctype term()
106 * :: t?Hgrow -> h!Trequest
108 * :: t?Hcheck0 -> h!Tcheck
111 * :: h!Trequest -> progress: h!Tcheck
115 * printf("term exits\n")
118 * From: gerard@research.bell-labs.com
119 * Date: Tue Jul 17 13:47:23 EDT 2001
120 * To: rob@research.bell-labs.com
122 * spin -c (or -a) spec
123 * pcc -DNP -o pan pan.c
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")