1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
/* 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")
*
*/
|