![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to cospan.1 CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / man / mana|
Return to cospan.1 CVS log | Up to [Research Unix] / researchv10dc / man / mana |
1.1 root 1: .TH COSPAN 1
2: .CT 1 prog_other
3: .SH NAME
4: cospan, psr \- coordination-specification analyzer
5: and pretty-printer
6: .SH SYNOPSIS
7: .B cospan
8: [
9: .I option ...
10: ]
11: .I file
12: .PP
13: .B psr
14: [
15: .I option ...
16: ]
17: .I file ...
18: .SH DESCRIPTION
19: .I Cospan
20: analyzes the behavior of coordinating systems.
21: Three types of input
22: .I file
23: are distinguished by suffix:
24: .TP
25: .B .sr
26: The normal case.
27: The file contains
28: .SM S/R
29: specifications as described in the reference, possibly including
30: .IR cpp (8)
31: commands, to be compiled into
32: .TP
33: .B .c
34: C code, which is compiled and linked into
35: .TP
36: .B .an
37: executable analysis program.
38: .PP
39: The options are
40: .TP
41: .BI -D name = value
42: .PD0
43: .TP
44: .BI -D name
45: .TP
46: .BI -U name
47: .TP
48: .BI -I directory
49: Same as in
50: .IR cc (1).
51: .PD
52: .TP
53: .B -v
54: Produce verbose syntax error messages.
55: .TP
56: .B -p
57: Suppress file-name/line-number information
58: for embedded C code.
59: .TP
60: .B -i
61: Produce an implementation version of
62: the C code.
63: .TP
64: .B -m
65: Produce a merged version of
66: the C code.
67: .TP
68: .B -n
69: Compile no transition checks (except deadlocks).
70: By default, the analysis gives a warning on the first stability violation
71: and aborts on non-semi-deterministic resolutions.
72: .TP
73: .B -b
74: Use C built-in (machine-dependent)
75: integer division operations.
76: By default, an
77: .SM S/R
78: integer division
79: .IB i / j
80: results in the greatest integer not higher then the
81: mathematical quotient, and the remainder operation
82: .IB i " mod " j
83: yields a result in the range
84: .RI 0... j \-1.
85: .TP
86: .BI -C opt
87: Pass option
88: .BI - opt
89: to the C compiler.
90: .TP
91: .BI -h size
92: Set the state hash table size to the next prime after
93: .I size ;
94: default is 32693.
95: .TP
96: .BI -H size
97: Similar to
98: .BI \-h size,
99: except that states which produce hash collisions are ignored.
100: .TP
101: .BI -t secs
102: Abort analysis after
103: the specified number of seconds.
104: .TP
105: .BI -V s
106: Produce verbose analysis output messages.
107: The string
108: .I s,
109: by default
110: .LR awel ,
111: specifies message types:
112: .I advice, warning, error,
113: or
114: .I list.
115: .TP
116: .B -r
117: Restart previously aborted analysis.
118: Recovery is possible in cases of hangups, interrupts,
119: software termination signals (due to a kill command),
120: timer alarms, no-space conditions, and aborts due to
121: .B -c
122: or
123: .B -L
124: requests.
125: .TP
126: .B -d
127: Abort on deadlocks.
128: By default, the analysis gives a warning on the first deadlock and reports
129: the number of deadlocks in the analysis summary.
130: .TP
131: .B -s
132: Abort on stability failures.
133: .TP
134: .B -l
135: List analysis on standard output.
136: .TP
137: .BI -T
138: Time each translation and execution step.
139: .PD0
140: .TP
141: .BI -L number,number
142: List analysis, reporting states
143: in the given range, and abort after searching the upper bound.
144: .TP
145: .BI -c number
146: Check each back-edge in the
147: component identified by the given
148: .I number
149: and abort analysis.
150: .PP
151: .TP
152: .BI CC= name
153: Use an alternate C compiler; default is
154: .BR CC=cc .
155: .PD
156: .PP
157: The order of the arguments is arbitrary, and several options may
158: be combined to a single argument, provided that option
159: values are terminated by white space.
160: Options can be preset by defining the environment variable
161: .BR COSPANOPT .
162: .PP
163: .I Psr
164: is a pretty-printer for
165: .SM S/R
166: specifications.
167: It places
168: .IR troff (1)
169: or
170: .I nroff
171: output on the standard output.
172: .PP
173: The options, which may be reset between
174: .I files,
175: are:
176: .TP
177: .B -d
178: Show current date in page footer.
179: .TP
180: .B -m
181: show file modification time in footer (default).
182: .TP
183: .BI -n N
184: Number every
185: .IR N th
186: line; default is
187: .BR -n0,
188: no numbering.
189: .TP
190: .BI -s N
191: Set type size
192: to
193: .I N
194: points, vertical spacing to
195: .IR N /60
196: inch, and tab stops every
197: .IR N /20
198: inch.
199: .TP
200: .BI -w N
201: Set the page width
202: to
203: .IR N
204: (in
205: .I troff
206: notation).
207: .PD0
208: .TP
209: .BI -f F
210: Use the
211: .I troff
212: font
213: .I F
214: and its italic, bold, and bold-italic counterparts.
215: Known fonts are
216: Bembo, CW, Euro, Futura, H, Hcond, Memphis, Optima, PA, R.
217: .TP
218: .BI -. request
219: Issue a
220: .I troff
221: request before printing the next
222: .IR file .
223: Multiple requests may be given.
224: .TP
225: .BI -T name
226: As in
227: .I troff.
228: Applies to all
229: .IR files .
230: If
231: .I name
232: is omitted,
233: .I troff
234: input is written on standard output.
235: .PD
236: .PP
237: .I Psr
238: sets the escape character to
239: .SM BEL.
240: The \e character is copied without
241: interpretation, to allow printing of embedded C code.
242: The macro
243: .B .SO
244: may be used to include
245: .I troff
246: text that uses the standard
247: escape character.
248: .PP
249: The strings
250: .BI DT ,
251: .BI L ,
252: and
253: .B R
254: contain today's date, the left-hand, and the right-hand side
255: of the page header, respectively.
256: .SH EXAMPLES
257: .TP
258: .B COSPANOPT=-TlImyincludedir cospan myfile.sr
259: equivalent to
260: .BR "cospan -T -l -Imyincludedir myfile.sr" .
261: .TP
262: .B psr -.ll6.5i -.lt6.5i myfile.sr
263: equivalent to
264: .BR "psr -w6.5i myfile.sr
265: .SH "FILES"
266: .TF /usr/lib/tmac/tmac.psr
267: .TP
268: .F *.R
269: recovery data
270: .PD0
271: .TP
272: .F *.T
273: error track
274: .TP
275: .F *.L
276: list output (
277: .B -L
278: option)
279: .TP
280: .F *.M
281: merging data
282: .TP
283: .F /tmp/srtm??????
284: temporary file
285: .TP
286: .F /usr/lib/sr
287: S/R compiler
288: .TP
289: .F /usr/lib/sr_D
290: S/R verbose compiler
291: .TP
292: .F /usr/include/crank.h
293: header file
294: .TP
295: .F /usr/include/crunch.h
296: implementation header file
297: .TP
298: .F /usr/libsr.a
299: analysis object library
300: .TP
301: .F /usr/lib/pretty
302: .I troff
303: preprocessor
304: .TP
305: .F /usr/lib/tmac/tmac.psr
306: .I troff
307: macros
308: .PD
309: .SH "SEE ALSO"
310: Z. Har'El and R. P. Kurshan,
311: .I
312: COSPAN User's Guide,
313: 11211-871009-21TM, AT&T Bell Laboratories.
314: .IR spin (1),
315: .IR d202 (1)
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.