17dd7cddfSDavid du Colombier /* VERSION 1 introduces plumbing 27dd7cddfSDavid du Colombier 2 increases SNARFSIZE from 4096 to 32000 37dd7cddfSDavid du Colombier */ 47dd7cddfSDavid du Colombier #define VERSION 2 53e12c5d1SDavid du Colombier 63e12c5d1SDavid du Colombier #define TBLOCKSIZE 512 /* largest piece of text sent to terminal */ 73e12c5d1SDavid du Colombier #define DATASIZE (UTFmax*TBLOCKSIZE+30) /* ... including protocol header stuff */ 87dd7cddfSDavid du Colombier #define SNARFSIZE 32000 /* maximum length of exchanged snarf buffer, must fit in 15 bits */ 93e12c5d1SDavid du Colombier /* 103e12c5d1SDavid du Colombier * Messages originating at the terminal 113e12c5d1SDavid du Colombier */ 123e12c5d1SDavid du Colombier typedef enum Tmesg 133e12c5d1SDavid du Colombier { 143e12c5d1SDavid du Colombier Tversion, /* version */ 153e12c5d1SDavid du Colombier Tstartcmdfile, /* terminal just opened command frame */ 163e12c5d1SDavid du Colombier Tcheck, /* ask host to poke with Hcheck */ 173e12c5d1SDavid du Colombier Trequest, /* request data to fill a hole */ 183e12c5d1SDavid du Colombier Torigin, /* gimme an Horigin near here */ 193e12c5d1SDavid du Colombier Tstartfile, /* terminal just opened a file's frame */ 203e12c5d1SDavid du Colombier Tworkfile, /* set file to which commands apply */ 213e12c5d1SDavid du Colombier Ttype, /* add some characters, but terminal already knows */ 223e12c5d1SDavid du Colombier Tcut, 233e12c5d1SDavid du Colombier Tpaste, 243e12c5d1SDavid du Colombier Tsnarf, 253e12c5d1SDavid du Colombier Tstartnewfile, /* terminal just opened a new frame */ 263e12c5d1SDavid du Colombier Twrite, /* write file */ 273e12c5d1SDavid du Colombier Tclose, /* terminal requests file close; check mod. status */ 283e12c5d1SDavid du Colombier Tlook, /* search for literal current text */ 293e12c5d1SDavid du Colombier Tsearch, /* search for last regular expression */ 303e12c5d1SDavid du Colombier Tsend, /* pretend he typed stuff */ 313e12c5d1SDavid du Colombier Tdclick, /* double click */ 323e12c5d1SDavid du Colombier Tstartsnarf, /* initiate snarf buffer exchange */ 333e12c5d1SDavid du Colombier Tsetsnarf, /* remember string in snarf buffer */ 343e12c5d1SDavid du Colombier Tack, /* acknowledge Hack */ 353e12c5d1SDavid du Colombier Texit, /* exit */ 367dd7cddfSDavid du Colombier Tplumb, /* send plumb message */ 373e12c5d1SDavid du Colombier TMAX, 383e12c5d1SDavid du Colombier }Tmesg; 393e12c5d1SDavid du Colombier /* 403e12c5d1SDavid du Colombier * Messages originating at the host 413e12c5d1SDavid du Colombier */ 423e12c5d1SDavid du Colombier typedef enum Hmesg 433e12c5d1SDavid du Colombier { 443e12c5d1SDavid du Colombier Hversion, /* version */ 453e12c5d1SDavid du Colombier Hbindname, /* attach name[0] to text in terminal */ 463e12c5d1SDavid du Colombier Hcurrent, /* make named file the typing file */ 473e12c5d1SDavid du Colombier Hnewname, /* create "" name in menu */ 483e12c5d1SDavid du Colombier Hmovname, /* move file name in menu */ 493e12c5d1SDavid du Colombier Hgrow, /* insert space in rasp */ 503e12c5d1SDavid du Colombier Hcheck0, /* see below */ 513e12c5d1SDavid du Colombier Hcheck, /* ask terminal to check whether it needs more data */ 523e12c5d1SDavid du Colombier Hunlock, /* command is finished; user can do things */ 533e12c5d1SDavid du Colombier Hdata, /* store this data in previously allocated space */ 543e12c5d1SDavid du Colombier Horigin, /* set origin of file/frame in terminal */ 553e12c5d1SDavid du Colombier Hunlockfile, /* unlock file in terminal */ 563e12c5d1SDavid du Colombier Hsetdot, /* set dot in terminal */ 573e12c5d1SDavid du Colombier Hgrowdata, /* Hgrow + Hdata folded together */ 583e12c5d1SDavid du Colombier Hmoveto, /* scrolling, context search, etc. */ 593e12c5d1SDavid du Colombier Hclean, /* named file is now 'clean' */ 603e12c5d1SDavid du Colombier Hdirty, /* named file is now 'dirty' */ 613e12c5d1SDavid du Colombier Hcut, /* remove space from rasp */ 623e12c5d1SDavid du Colombier Hsetpat, /* set remembered regular expression */ 633e12c5d1SDavid du Colombier Hdelname, /* delete file name from menu */ 643e12c5d1SDavid du Colombier Hclose, /* close file and remove from menu */ 653e12c5d1SDavid du Colombier Hsetsnarf, /* remember string in snarf buffer */ 663e12c5d1SDavid du Colombier Hsnarflen, /* report length of implicit snarf */ 673e12c5d1SDavid du Colombier Hack, /* request acknowledgement */ 683e12c5d1SDavid du Colombier Hexit, 69*e7d29567SDavid du Colombier Hplumb, /* return plumb message to terminal - version 1 */ 703e12c5d1SDavid du Colombier HMAX, 713e12c5d1SDavid du Colombier }Hmesg; 723e12c5d1SDavid du Colombier typedef struct Header{ 733e12c5d1SDavid du Colombier uchar type; /* one of the above */ 743e12c5d1SDavid du Colombier uchar count0; /* low bits of data size */ 753e12c5d1SDavid du Colombier uchar count1; /* high bits of data size */ 763e12c5d1SDavid du Colombier uchar data[1]; /* variable size */ 773e12c5d1SDavid du Colombier }Header; 789a747e4fSDavid du Colombier 793e12c5d1SDavid du Colombier /* 803e12c5d1SDavid du Colombier * File transfer protocol schematic, a la Holzmann 819a747e4fSDavid du Colombier * #define N 6 823e12c5d1SDavid du Colombier * 839a747e4fSDavid du Colombier * chan h = [4] of { mtype }; 849a747e4fSDavid du Colombier * chan t = [4] of { mtype }; 859a747e4fSDavid du Colombier * 869a747e4fSDavid du Colombier * mtype = { Hgrow, Hdata, 879a747e4fSDavid du Colombier * Hcheck, Hcheck0, 889a747e4fSDavid du Colombier * Trequest, Tcheck, 899a747e4fSDavid du Colombier * }; 909a747e4fSDavid du Colombier * 919a747e4fSDavid du Colombier * active proctype host() 929a747e4fSDavid du Colombier * { byte n; 933e12c5d1SDavid du Colombier * 943e12c5d1SDavid du Colombier * do 959a747e4fSDavid du Colombier * :: n < N -> n++; t!Hgrow 969a747e4fSDavid du Colombier * :: n == N -> n++; t!Hcheck0 979a747e4fSDavid du Colombier * 983e12c5d1SDavid du Colombier * :: h?Trequest -> t!Hdata 993e12c5d1SDavid du Colombier * :: h?Tcheck -> t!Hcheck 1003e12c5d1SDavid du Colombier * od 1013e12c5d1SDavid du Colombier * } 1029a747e4fSDavid du Colombier * 1039a747e4fSDavid du Colombier * active proctype term() 1049a747e4fSDavid du Colombier * { 1053e12c5d1SDavid du Colombier * do 1063e12c5d1SDavid du Colombier * :: t?Hgrow -> h!Trequest 1073e12c5d1SDavid du Colombier * :: t?Hdata -> skip 1083e12c5d1SDavid du Colombier * :: t?Hcheck0 -> h!Tcheck 1093e12c5d1SDavid du Colombier * :: t?Hcheck -> 1103e12c5d1SDavid du Colombier * if 1119a747e4fSDavid du Colombier * :: h!Trequest -> progress: h!Tcheck 1123e12c5d1SDavid du Colombier * :: break 1133e12c5d1SDavid du Colombier * fi 1149a747e4fSDavid du Colombier * od; 1159a747e4fSDavid du Colombier * printf("term exits\n") 1163e12c5d1SDavid du Colombier * } 1179a747e4fSDavid du Colombier * 1189a747e4fSDavid du Colombier * From: gerard@research.bell-labs.com 1199a747e4fSDavid du Colombier * Date: Tue Jul 17 13:47:23 EDT 2001 1209a747e4fSDavid du Colombier * To: rob@research.bell-labs.com 1219a747e4fSDavid du Colombier * 1229a747e4fSDavid du Colombier * spin -c (or -a) spec 1239a747e4fSDavid du Colombier * pcc -DNP -o pan pan.c 1249a747e4fSDavid du Colombier * pan -l 1259a747e4fSDavid du Colombier * 1269a747e4fSDavid du Colombier * proves that there are no non-progress cycles 1279a747e4fSDavid du Colombier * (infinite executions *not* passing through 1289a747e4fSDavid du Colombier * the statement marked with a label starting 1299a747e4fSDavid du Colombier * with the prefix "progress") 1309a747e4fSDavid du Colombier * 1313e12c5d1SDavid du Colombier */ 132