121 		printf("seed used: %d\n", SeedUsed);  in alldone()
125 			printf("spin: %d error(s) - aborting\n",  in alldone()
128 			printf("Exit-Status 0\n");  in alldone()
181 	printf("use: spin [-option] ... [-option] file\n");  in usage()
182 	printf("\tNote: file must always be the last argument\n");  in usage()
183 	printf("\t-A apply slicing algorithm\n");  in usage()
184 	printf("\t-a generate a verifier in pan.c\n");  in usage()
185 	printf("\t-B no final state details in simulations\n");  in usage()
186 	printf("\t-b don't execute printfs in simulation\n");  in usage()
187 	printf("\t-C print channel access info (combine with -g etc.)\n");  in usage()
188 	printf("\t-c columnated -s -r simulation output\n");  in usage()
189 	printf("\t-d produce symbol-table information\n");  in usage()
190 	printf("\t-Dyyy pass -Dyyy to the preprocessor\n");  in usage()
191 	printf("\t-Eyyy pass yyy to the preprocessor\n");  in usage()
192 	printf("\t-e compute synchronous product of multiple never claims (modified by -L)\n");  in usage()
193 	printf("\t-f \"..formula..\"  translate LTL ");  in usage()
194 	printf("into never claim\n");  in usage()
195 	printf("\t-F file  like -f, but with the LTL formula stored in a 1-line file\n");  in usage()
196 	printf("\t-g print all global variables\n");  in usage()
197 	printf("\t-h at end of run, print value of seed for random nr generator used\n");  in usage()
198 	printf("\t-i interactive (random simulation)\n");  in usage()
199 	printf("\t-I show result of inlining and preprocessing\n");  in usage()
200 	printf("\t-J reverse eval order of nested unlesses\n");  in usage()
201 	printf("\t-jN skip the first N steps ");  in usage()
202 	printf("in simulation trail\n");  in usage()
203 	printf("\t-k fname use the trailfile stored in file fname, see also -t\n");  in usage()
204 	printf("\t-L when using -e, use strict language intersection\n");  in usage()
205 	printf("\t-l print all local variables\n");  in usage()
206 	printf("\t-M print msc-flow in Postscript\n");  in usage()
207 	printf("\t-m lose msgs sent to full queues\n");  in usage()
208 	printf("\t-N fname use never claim stored in file fname\n");  in usage()
209 	printf("\t-nN seed for random nr generator\n");  in usage()
210 	printf("\t-O use old scope rules (pre 5.3.0)\n");  in usage()
211 	printf("\t-o1 turn off dataflow-optimizations in verifier\n");  in usage()
212 	printf("\t-o2 don't hide write-only variables in verifier\n");  in usage()
213 	printf("\t-o3 turn off statement merging in verifier\n");  in usage()
214 	printf("\t-o4 turn on rendezvous optiomizations in verifier\n");  in usage()
215 	printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\n");  in usage()
216 	printf("\t-Pxxx use xxx for preprocessing\n");  in usage()
217 	printf("\t-p print all statements\n");  in usage()
218 	printf("\t-qN suppress io for queue N in printouts\n");  in usage()
219 	printf("\t-r print receive events\n");  in usage()
220 	printf("\t-S1 and -S2 separate pan source for claim and model\n");  in usage()
221 	printf("\t-s print send events\n");  in usage()
222 	printf("\t-T do not indent printf output\n");  in usage()
223 	printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");  in usage()
224 	printf("\t-Uyyy pass -Uyyy to the preprocessor\n");  in usage()
225 	printf("\t-uN stop a simulation run after N steps\n");  in usage()
226 	printf("\t-v verbose, more warnings\n");  in usage()
227 	printf("\t-w very verbose (when combined with -l or -g)\n");  in usage()
228 	printf("\t-[XYZ] reserved for use by xspin interface\n");  in usage()
229 	printf("\t-V print version number and exit\n");  in usage()
240 		printf("spin: dataflow optimizations turned %s\n",  in optimizations()
247 		printf("spin: dead variable elimination turned %s\n",  in optimizations()
254 		printf("spin: statement merging turned %s\n",  in optimizations()
262 		printf("spin: rendezvous optimization turned %s\n",  in optimizations()
269 		printf("spin: case caching turned %s\n",  in optimizations()
273 		printf("spin: bad or missing parameter on -o\n");  in optimizations()
348 		case 'V': printf("%s\n", SpinVersion);  in main()
369 		printf("spin: warning -o[123] option ignored in simulations\n");  in main()
375 		{	printf("spin: cannot open %s\n", *ltl_file);  in main()
379 		{	printf("spin: cannot read %s\n", *ltl_file);  in main()
395 			{	printf("spin: cannot create tmp file %s\n",  in main()
419 		{	printf("spin: cannot open %s\n", out1);  in main()
439 			printf("spin: missing argument to -f\n");  in main()
442 		printf("%s\n", SpinVersion);  in main()
450 		{	printf("spin: -c precludes all flags except -t\n");  in main()
542 	printf("spin: %s:%d, Error: ",  in non_fatal()
545 		printf(s1, s2);  in non_fatal()
547 		printf(s1);  in non_fatal()
549 		printf(" near '%s'", yytext);  in non_fatal()
550 	printf("\n");  in non_fatal()
576 	{	printf("spin: allocated %ld Gb, wanted %d bytes more\n",  in emalloc()
660 			printf("spin: Warning, never claim has side-effect\n");  in nn()
677 				printf("spin: warning, make sure that the S1 model\n");  in nn()
678 				printf("      also polls channel '%s' in its claim\n",  in nn()
691 		{	printf("spin: never, saw "); explain(t); printf("\n");  in nn()
695 	{	printf("spin: Warning, using %s outside never claim\n",  in nn()