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