Subversion Repositories planix.SVN

/* 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")
 * 
 */