/* VERSION 1 introduces plumbing	2 increases SNARFSIZE from 4096 to 32000 */#define	VERSION	2#define	TBLOCKSIZE 512		  /* largest piece of text sent to terminal */#define	DATASIZE  (UTFmax*TBLOCKSIZE+30) /* ... including protocol header stuff */#define	SNARFSIZE 32000		/* maximum length of exchanged snarf buffer, must fit in 15 bits *//* * Messages originating at the terminal */typedef enum Tmesg{	Tversion,	/* version */	Tstartcmdfile,	/* terminal just opened command frame */	Tcheck,		/* ask host to poke with Hcheck */	Trequest,	/* request data to fill a hole */	Torigin,	/* gimme an Horigin near here */	Tstartfile,	/* terminal just opened a file's frame */	Tworkfile,	/* set file to which commands apply */	Ttype,		/* add some characters, but terminal already knows */	Tcut,	Tpaste,	Tsnarf,	Tstartnewfile,	/* terminal just opened a new frame */	Twrite,		/* write file */	Tclose,		/* terminal requests file close; check mod. status */	Tlook,		/* search for literal current text */	Tsearch,	/* search for last regular expression */	Tsend,		/* pretend he typed stuff */	Tdclick,	/* double click */	Tstartsnarf,	/* initiate snarf buffer exchange */	Tsetsnarf,	/* remember string in snarf buffer */	Tack,		/* acknowledge Hack */	Texit,		/* exit */	Tplumb,		/* send plumb message */	TMAX,}Tmesg;/* * Messages originating at the host */typedef enum Hmesg{	Hversion,	/* version */	Hbindname,	/* attach name[0] to text in terminal */	Hcurrent,	/* make named file the typing file */	Hnewname,	/* create "" name in menu */	Hmovname,	/* move file name in menu */	Hgrow,		/* insert space in rasp */	Hcheck0,	/* see below */	Hcheck,		/* ask terminal to check whether it needs more data */	Hunlock,	/* command is finished; user can do things */	Hdata,		/* store this data in previously allocated space */	Horigin,	/* set origin of file/frame in terminal */	Hunlockfile,	/* unlock file in terminal */	Hsetdot,	/* set dot in terminal */	Hgrowdata,	/* Hgrow + Hdata folded together */	Hmoveto,	/* scrolling, context search, etc. */	Hclean,		/* named file is now 'clean' */	Hdirty,		/* named file is now 'dirty' */	Hcut,		/* remove space from rasp */	Hsetpat,	/* set remembered regular expression */	Hdelname,	/* delete file name from menu */	Hclose,		/* close file and remove from menu */	Hsetsnarf,	/* remember string in snarf buffer */	Hsnarflen,	/* report length of implicit snarf */	Hack,		/* request acknowledgement */	Hexit,	Hplumb,		/* return plumb message to terminal - version 1 */	HMAX,}Hmesg;typedef struct Header{	uchar	type;		/* one of the above */	uchar	count0;		/* low bits of data size */	uchar	count1;		/* high bits of data size */	uchar	data[1];	/* variable size */}Header;/* * File transfer protocol schematic, a la Holzmann * #define N	6 *  * chan h = [4] of { mtype }; * chan t = [4] of { mtype }; *  * mtype = {	Hgrow, Hdata, * 		Hcheck, Hcheck0, * 		Trequest, Tcheck, * 	}; *  * active proctype host() * {	byte n; *  * 	do * 	:: n <  N -> n++; t!Hgrow * 	:: n == N -> n++; t!Hcheck0 *  * 	:: h?Trequest -> t!Hdata * 	:: h?Tcheck   -> t!Hcheck * 	od * } *  * active proctype term() * { * 	do * 	:: t?Hgrow   -> h!Trequest * 	:: t?Hdata   -> skip * 	:: t?Hcheck0 -> h!Tcheck * 	:: t?Hcheck  -> * 		if * 		:: h!Trequest -> progress: h!Tcheck * 		:: break * 		fi * 	od; * 	printf("term exits\n") * } * * From: gerard@research.bell-labs.com * Date: Tue Jul 17 13:47:23 EDT 2001 * To: rob@research.bell-labs.com *  * spin -c 	(or -a) spec * pcc -DNP -o pan pan.c * pan -l *  * proves that there are no non-progress cycles * (infinite executions *not* passing through * the statement marked with a label starting * with the prefix "progress") *  */