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 */ 132