projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
move everything out of trunk
[lttv.git] / verif / Spin / Src5.1.6 / pangen1.h
1 /***** spin: pangen1.h *****/
2
3 /* Copyright (c) 1989-2008 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
11 /* (c) 2007: small additions for V5.0 to support multi-core verifications */
12
13 static char *Code2a[] = { /* the tail of procedure run() */
14 "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
15 " if (!state_tables",
16 "#ifdef HAS_CODE",
17 " && !readtrail",
18 "#endif",
19 "#if NCORE>1",
20 " && core_id == 0",
21 "#endif",
22 " )",
23 " { printf(\"warning: for p.o. reduction to be valid \");",
24 " printf(\"the never claim must be stutter-invariant\\n\");",
25 " printf(\"(never claims generated from LTL \");",
26 " printf(\"formulae are stutter-invariant)\\n\");",
27 " }",
28 "#endif",
29 " UnBlock; /* disable rendez-vous */",
30 "#ifdef BITSTATE",
31 #ifndef POWOW
32 " if (udmem)",
33 " { udmem *= 1024L*1024L;",
34 " #if NCORE>1",
35 " if (!readtrail)",
36 " { void init_SS(unsigned long);",
37 " init_SS((unsigned long) udmem);",
38 " } else",
39 " #endif",
40 " SS = (uchar *) emalloc(udmem);",
41 " bstore = bstore_mod;",
42 " } else",
43 #endif
44 " #if NCORE>1",
45 " { void init_SS(unsigned long);",
46 " init_SS(ONE_L<<(ssize-3));",
47 " }",
48 " #else",
49 " SS = (uchar *) emalloc(ONE_L<<(ssize-3));",
50 " #endif",
51 "#else", /* if not BITSTATE */
52 " hinit();",
53 "#endif",
54 "#if defined(FULLSTACK) && defined(BITSTATE)",
55 " onstack_init();",
56 "#endif",
57 "#if defined(CNTRSTACK) && !defined(BFS)",
58 " LL = (uchar *) emalloc(ONE_L<<(ssize-3));",
59 "#endif",
60 " stack = ( Stack *) emalloc(sizeof(Stack));",
61 " svtack = (Svtack *) emalloc(sizeof(Svtack));",
62 " /* a place to point for Pptr of non-running procs: */",
63 " noptr = (uchar *) emalloc(Maxbody * sizeof(char));",
64 "#ifdef SVDUMP",
65 " if (vprefix > 0)",
66 " write(svfd, (uchar *) &vprefix, sizeof(int));",
67 "#endif",
68 "#ifdef VERI",
69 " Addproc(VERI); /* never - pid = 0 */",
70 "#endif",
71 " active_procs(); /* started after never */",
72 "#ifdef EVENT_TRACE",
73 " now._event = start_event;",
74 " reached[EVENT_TRACE][start_event] = 1;",
75 "#endif",
76
77 "#ifdef HAS_CODE",
78 " globinit();",
79 "#endif",
80 "#ifdef BITSTATE",
81 "go_again:",
82 "#endif",
83 " do_the_search();",
84 "#ifdef BITSTATE",
85 " if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
86 " { printf(\"Run %%d:\\n\", HASH_NR);",
87 " wrap_stats();",
88 " printf(\"\\n\");",
89 " memset(SS, 0, ONE_L<<(ssize-3));",
90 "#ifdef CNTRSTACK",
91 " memset(LL, 0, ONE_L<<(ssize-3));",
92 "#endif",
93 "#ifdef FULLSTACK",
94 " memset((uchar *) S_Tab, 0, ",
95 " maxdepth*sizeof(struct H_el *));",
96 "#endif",
97 " nstates=nlinks=truncs=truncs2=ngrabs = 0;",
98 " nlost=nShadow=hcmp = 0;",
99 " Fa=Fh=Zh=Zn = 0;",
100 " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
101 " goto go_again;",
102 " }",
103 "#endif",
104 "}",
105 "#ifdef HAS_PROVIDED",
106 "int provided(int, uchar, int, Trans *);",
107 "#endif",
108
109 "#if NCORE>1",
110 "#define GLOBAL_LOCK (0)",
111 "#ifndef CS_N",
112 "#define CS_N (256*NCORE)", /* must be a power of 2 */
113 "#endif",
114
115 "#ifdef NGQ", /* no global queue */
116 "#define NR_QS (NCORE)",
117 "#define CS_NR (CS_N+1) /* 2^N + 1, nr critical sections */",
118 "#define GQ_RD GLOBAL_LOCK", /* not really used in this mode */
119 "#define GQ_WR GLOBAL_LOCK", /* but just in case... */
120 "#define CS_ID (1 + (int) (j1 & (CS_N-1))) /* mask: 2^N - 1, zero reserved */",
121 "#define QLOCK(n) (1+n)", /* overlaps first n zones of hashtable */
122 "#else",
123 "#define NR_QS (NCORE+1)", /* add a global queue */
124 "#define CS_NR (CS_N+3)", /* 2 extra locks for global q */
125 "#define GQ_RD (1)", /* read access to global q */
126 "#define GQ_WR (2)", /* write access to global q */
127 "#define CS_ID (3 + (int) (j1 & (CS_N-1)))",
128 "#define QLOCK(n) (3+n)",/* overlaps first n zones of hashtable */
129 "#endif",
130 "",
131 "void e_critical(int);",
132 "void x_critical(int);",
133 "",
134 "#ifndef SEP_STATE",
135 " #define enter_critical(w) e_critical(w)",
136 " #define leave_critical(w) x_critical(w)",
137 "#else",
138 " #ifdef NGQ",
139 " #define enter_critical(w) { if (w < 1+NCORE) e_critical(w); }",
140 " #define leave_critical(w) { if (w < 1+NCORE) x_critical(w); }",
141 " #else",
142 " #define enter_critical(w) { if (w < 3+NCORE) e_critical(w); }",
143 " #define leave_critical(w) { if (w < 3+NCORE) x_critical(w); }",
144 " #endif",
145 "#endif",
146 "",
147 "int",
148 "cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */
149 "{ va_list args;",
150 " enter_critical(GLOBAL_LOCK); /* printing */",
151 " printf(\"cpu%%d: \", core_id);",
152 " fflush(stdout);",
153 " va_start(args, fmt);",
154 " vprintf(fmt, args);",
155 " va_end(args);",
156 " fflush(stdout);",
157 " leave_critical(GLOBAL_LOCK);",
158 " return 1;",
159 "}",
160 "#else",
161 "int",
162 "cpu_printf(const char *fmt, ...)",
163 "{ va_list args;",
164 " va_start(args, fmt);",
165 " vprintf(fmt, args);",
166 " va_end(args);",
167 " return 1;",
168 "}",
169 "#endif",
170
171 #ifndef PRINTF
172 "int",
173 "Printf(const char *fmt, ...)",
174 "{ /* Make sure the args to Printf",
175 " * are always evaluated (e.g., they",
176 " * could contain a run stmnt)",
177 " * but do not generate the output",
178 " * during verification runs",
179 " * unless explicitly wanted",
180 " * If this fails on your system",
181 " * compile SPIN itself -DPRINTF",
182 " * and this code is not generated",
183 " */",
184 "#ifdef HAS_CODE",
185 " if (readtrail)",
186 " { va_list args;",
187 " va_start(args, fmt);",
188 " vprintf(fmt, args);",
189 " va_end(args);",
190 " return 1;",
191 " }",
192 "#endif",
193 "#ifdef PRINTF",
194 " va_list args;",
195 " va_start(args, fmt);",
196 " vprintf(fmt, args);",
197 " va_end(args);",
198 "#endif",
199 " return 1;",
200 "}",
201 #endif
202 "extern void printm(int);",
203
204 "#ifndef SC",
205 "#define getframe(i) &trail[i];",
206 "#else",
207 "static long HHH, DDD, hiwater;",
208 "static long CNT1, CNT2;",
209 "static int stackwrite;",
210 "static int stackread;",
211 "static Trail frameptr;",
212 "Trail *",
213 "getframe(int d)",
214 "{",
215 " if (CNT1 == CNT2)",
216 " return &trail[d];",
217 "",
218 " if (d >= (CNT1-CNT2)*DDD)",
219 " return &trail[d - (CNT1-CNT2)*DDD];",
220 "",
221 " if (!stackread",
222 " && (stackread = open(stackfile, 0)) < 0)",
223 " { printf(\"getframe: cannot open %%s\\n\", stackfile);",
224 " wrapup();",
225 " }",
226 " if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1",
227 " || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
228 " { printf(\"getframe: frame read error\\n\");",
229 " wrapup();",
230 " }",
231 " return &frameptr;",
232 "}",
233 "#endif",
234
235 "#if !defined(SAFETY) && !defined(BITSTATE)",
236 "#if !defined(FULLSTACK) || defined(MA)",
237 "#define depth_of(x) A_depth /* an estimate */",
238 "#else",
239 "int",
240 "depth_of(struct H_el *s)",
241 "{ Trail *t; int d;",
242 " for (d = 0; d <= A_depth; d++)",
243 " { t = getframe(d);",
244 " if (s == t->ostate)",
245 " return d;",
246 " }",
247 " printf(\"pan: cannot happen, depth_of\\n\");",
248 " return depthfound;",
249 "}",
250 "#endif",
251 "#endif",
252
253 "#if NCORE>1",
254 "extern void cleanup_shm(int);",
255 "volatile unsigned int *search_terminated; /* to signal early termination */",
256 /*
257 * Meaning of bitflags in search_terminated:
258 * 1 set by pan_exit
259 * 2 set by wrapup
260 * 4 set by uerror
261 * 8 set by sudden_stop -- called after someone_crashed and [Uu]error
262 * 16 set by cleanup_shm
263 * 32 set by give_up -- called on signal
264 * 64 set by proxy_exit
265 * 128 set by proxy on write port failure
266 * 256 set by proxy on someone_crashed
267 *
268 * Flags 8|32|128|256 indicate abnormal termination
269 *
270 * The flags are checked in 4 functions in the code:
271 * sudden_stop()
272 * someone_crashed() (proxy and pan version)
273 * mem_hand_off()
274 */
275 "#endif",
276 "void",
277 "pan_exit(int val)",
278 "{ void stop_timer(void);",
279 " if (signoff)",
280 " { printf(\"--end of output--\\n\");",
281 " }",
282 "#if NCORE>1",
283 " if (search_terminated != NULL)",
284 " { *search_terminated |= 1; /* pan_exit */",
285 " }",
286 "#ifdef USE_DISK",
287 " { void dsk_stats(void);",
288 " dsk_stats();",
289 " }",
290 "#endif",
291 " if (!state_tables && !readtrail)",
292 " { cleanup_shm(1);",
293 " }",
294 "#endif",
295 " if (val == 2)",
296 " { val = 0;",
297 " } else",
298 " { stop_timer();",
299 " }",
300 " exit(val);",
301 "}",
302
303 "#ifdef HAS_CODE",
304 "char *",
305 "transmognify(char *s)",
306 "{ char *v, *w;",
307 " static char buf[2][2048];",
308 " int i, toggle = 0;",
309
310 " if (!s || strlen(s) > 2047) return s;",
311 " memset(buf[0], 0, 2048);",
312 " memset(buf[1], 0, 2048);",
313 " strcpy(buf[toggle], s);",
314 " while ((v = strstr(buf[toggle], \"{c_code\")))", /* assign v */
315 " { *v = '\\0'; v++;",
316 " strcpy(buf[1-toggle], buf[toggle]);",
317 " for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
318 " if (*w != '}') return s;",
319 " *w = '\\0'; w++;",
320 " for (i = 0; code_lookup[i].c; i++)",
321 " if (strcmp(v, code_lookup[i].c) == 0",
322 " && strlen(v) == strlen(code_lookup[i].c))",
323 " { if (strlen(buf[1-toggle])",
324 " + strlen(code_lookup[i].t)",
325 " + strlen(w) > 2047)",
326 " return s;",
327 " strcat(buf[1-toggle], code_lookup[i].t);",
328 " break;",
329 " }",
330 " strcat(buf[1-toggle], w);",
331 " toggle = 1 - toggle;",
332 " }",
333 " buf[toggle][2047] = '\\0';",
334 " return buf[toggle];",
335 "}",
336 "#else",
337 "char * transmognify(char *s) { return s; }",
338 "#endif",
339
340 "#ifdef HAS_CODE",
341 "void",
342 "add_src_txt(int ot, int tt)",
343 "{ Trans *t;",
344 " char *q;",
345 "",
346 " for (t = trans[ot][tt]; t; t = t->nxt)",
347 " { printf(\"\\t\\t\");",
348
349 " q = transmognify(t->tp);",
350 " for ( ; q && *q; q++)",
351 " if (*q == '\\n')",
352 " printf(\"\\\\n\");",
353 " else",
354 " putchar(*q);",
355 " printf(\"\\n\");",
356 " }",
357 "}",
358 "void",
359 "wrap_trail(void)",
360 "{ static int wrap_in_progress = 0;",
361 " int i; short II;",
362 " P0 *z;",
363 "",
364 " if (wrap_in_progress++) return;",
365 "",
366 " printf(\"spin: trail ends after %%ld steps\\n\", depth);",
367 " if (onlyproc >= 0)",
368 " { if (onlyproc >= now._nr_pr) { pan_exit(0); }",
369 " II = onlyproc;",
370 " z = (P0 *)pptr(II);",
371 " printf(\"%%3ld:\tproc %%d (%%s) \",",
372 " depth, II, procname[z->_t]);",
373 " for (i = 0; src_all[i].src; i++)",
374 " if (src_all[i].tp == (int) z->_t)",
375 " { printf(\" line %%3d\",",
376 " src_all[i].src[z->_p]);",
377 " break;",
378 " }",
379 " printf(\" (state %%2d)\", z->_p);",
380 " if (!stopstate[z->_t][z->_p])",
381 " printf(\" (invalid end state)\");",
382 " printf(\"\\n\");",
383 " add_src_txt(z->_t, z->_p);",
384 " pan_exit(0);",
385 " }",
386 " printf(\"#processes %%d:\\n\", now._nr_pr);",
387 " if (depth < 0) depth = 0;",
388 " for (II = 0; II < now._nr_pr; II++)",
389 " { z = (P0 *)pptr(II);",
390 " printf(\"%%3ld:\tproc %%d (%%s) \",",
391 " depth, II, procname[z->_t]);",
392 " for (i = 0; src_all[i].src; i++)",
393 " if (src_all[i].tp == (int) z->_t)",
394 " { printf(\" line %%3d\",",
395 " src_all[i].src[z->_p]);",
396 " break;",
397 " }",
398 " printf(\" (state %%2d)\", z->_p);",
399 " if (!stopstate[z->_t][z->_p])",
400 " printf(\" (invalid end state)\");",
401 " printf(\"\\n\");",
402 " add_src_txt(z->_t, z->_p);",
403 " }",
404 " c_globals();",
405 " for (II = 0; II < now._nr_pr; II++)",
406 " { z = (P0 *)pptr(II);",
407 " c_locals(II, z->_t);",
408 " }",
409 "#ifdef ON_EXIT",
410 " ON_EXIT;",
411 "#endif",
412 " pan_exit(0);",
413 "}",
414 "FILE *",
415 "findtrail(void)",
416 "{ FILE *fd;",
417 " char fnm[512], *q;",
418 " char MyFile[512];", /* avoid using a non-writable string */
419 " char MySuffix[16];",
420 " int try_core;",
421 " int candidate_files;",
422 "",
423 " if (trailfilename != NULL)",
424 " { fd = fopen(trailfilename, \"r\");",
425 " if (fd == NULL)",
426 " { printf(\"pan: cannot find %%s\\n\", trailfilename);",
427 " pan_exit(1);",
428 " } /* else */",
429 " goto success;",
430 " }",
431 "talk:",
432 " try_core = 1;",
433 " candidate_files = 0;",
434 " tprefix = \"trail\";",
435 " strcpy(MyFile, TrailFile);",
436 " do { /* see if there's more than one possible trailfile */",
437 " if (whichtrail)",
438 " { sprintf(fnm, \"%%s%%d.%%s\",",
439 " MyFile, whichtrail, tprefix);",
440 " fd = fopen(fnm, \"r\");",
441 " if (fd != NULL)",
442 " { candidate_files++;",
443 " if (verbose==100)",
444 " printf(\"trail%%d: %%s\\n\",",
445 " candidate_files, fnm);",
446 " fclose(fd);",
447 " }",
448 " if ((q = strchr(MyFile, \'.\')) != NULL)",
449 " { *q = \'\\0\';", /* e.g., strip .pml */
450 " sprintf(fnm, \"%%s%%d.%%s\",",
451 " MyFile, whichtrail, tprefix);",
452 " *q = \'.\';",
453 " fd = fopen(fnm, \"r\");",
454 " if (fd != NULL)",
455 " { candidate_files++;",
456 " if (verbose==100)",
457 " printf(\"trail%%d: %%s\\n\",",
458 " candidate_files, fnm);",
459 " fclose(fd);",
460 " } }",
461 " } else",
462 " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
463 " fd = fopen(fnm, \"r\");",
464 " if (fd != NULL)",
465 " { candidate_files++;",
466 " if (verbose==100)",
467 " printf(\"trail%%d: %%s\\n\",",
468 " candidate_files, fnm);",
469 " fclose(fd);",
470 " }",
471 " if ((q = strchr(MyFile, \'.\')) != NULL)",
472 " { *q = \'\\0\';", /* e.g., strip .pml */
473 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
474 " *q = \'.\';",
475 " fd = fopen(fnm, \"r\");",
476 " if (fd != NULL)",
477 " { candidate_files++;",
478 " if (verbose==100)",
479 " printf(\"trail%%d: %%s\\n\",",
480 " candidate_files, fnm);",
481 " fclose(fd);",
482 " } } }",
483 " tprefix = MySuffix;",
484 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
485 " } while (try_core <= NCORE);",
486 "",
487 " if (candidate_files != 1)",
488 " { if (verbose != 100)",
489 " { printf(\"error: there are %%d trail files:\\n\",",
490 " candidate_files);",
491 " verbose = 100;",
492 " goto talk;",
493 " } else",
494 " { printf(\"pan: rm or mv all except one\\n\");",
495 " exit(1);",
496 " } }",
497
498 " try_core = 1;",
499 " strcpy(MyFile, TrailFile); /* restore */",
500 " tprefix = \"trail\";",
501 "try_again:",
502 " if (whichtrail)",
503 " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
504 " fd = fopen(fnm, \"r\");",
505 " if (fd == NULL && (q = strchr(MyFile, \'.\')))",
506 " { *q = \'\\0\';", /* e.g., strip .pml on original file */
507 " sprintf(fnm, \"%%s%%d.%%s\",",
508 " MyFile, whichtrail, tprefix);",
509 " *q = \'.\';",
510 " fd = fopen(fnm, \"r\");",
511 " }",
512 " } else",
513 " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
514 " fd = fopen(fnm, \"r\");",
515 " if (fd == NULL && (q = strchr(MyFile, \'.\')))",
516 " { *q = \'\\0\';", /* e.g., strip .pml on original file */
517 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
518 " *q = \'.\';",
519 " fd = fopen(fnm, \"r\");",
520 " } }",
521 " if (fd == NULL)",
522 " { if (try_core < NCORE)",
523 " { tprefix = MySuffix;",
524 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
525 " goto try_again;",
526 " }",
527 " printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
528 " pan_exit(1);",
529 " }",
530 "success:",
531 "#if NCORE>1 && defined(SEP_STATE)",
532 " { void set_root(void); /* for partial traces from local root */",
533 " set_root();",
534 " }",
535 "#endif",
536 " return fd;",
537 "}",
538 "",
539 "uchar do_transit(Trans *, short);",
540 "",
541 "void",
542 "getrail(void)",
543 "{ FILE *fd;",
544 " char *q;",
545 " int i, t_id, lastnever=-1; short II;",
546 " Trans *t;",
547 " P0 *z;",
548 "",
549 " fd = findtrail(); /* exits if unsuccessful */",
550 " while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
551 " { if (depth == -1)",
552 " printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
553 " if (depth < 0)",
554 " continue;",
555 " if (i > now._nr_pr)",
556 " { printf(\"pan: Error, proc %%d invalid pid \", i);",
557 " printf(\"transition %%d\\n\", t_id);",
558 " break;",
559 " }",
560 " II = i;",
561 " z = (P0 *)pptr(II);",
562 " for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
563 " if (t->t_id == (T_ID) t_id)",
564 " break;",
565 " if (!t)",
566 " { for (i = 0; i < NrStates[z->_t]; i++)",
567 " { t = trans[z->_t][i];",
568 " if (t && t->t_id == (T_ID) t_id)",
569 " { printf(\"\\tRecovered at state %%d\\n\", i);",
570 " z->_p = i;",
571 " goto recovered;",
572 " } }",
573 " printf(\"pan: Error, proc %%d type %%d state %%d: \",",
574 " II, z->_t, z->_p);",
575 " printf(\"transition %%d not found\\n\", t_id);",
576 " printf(\"pan: list of possible transitions in this process:\\n\");",
577 " if (z->_t >= 0 && z->_t <= _NP_)",
578 " for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
579 " printf(\" t_id %%d -- case %%d, [%%s]\\n\",",
580 " t->t_id, t->forw, t->tp);",
581 " break; /* pan_exit(1); */",
582 " }",
583 "recovered:",
584 " q = transmognify(t->tp);",
585 " if (gui) simvals[0] = \'\\0\';",
586
587 " this = pptr(II);",
588 " trpt->tau |= 1;", /* timeout always possible */
589 " if (!do_transit(t, II))",
590 " { if (onlyproc >= 0 && II != onlyproc)",
591 " goto moveon;",
592 " printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
593 " printf(\" most likely causes: missing c_track statements\\n\");",
594 " printf(\" or illegal side-effects in c_expr statements\\n\");",
595 " }",
596
597 " if (onlyproc >= 0 && II != onlyproc)",
598 " goto moveon;",
599
600 " if (verbose)",
601 " { printf(\"%%3ld: proc %%2d (%%s) \", depth, II, procname[z->_t]);",
602
603 " for (i = 0; src_all[i].src; i++)",
604 " if (src_all[i].tp == (int) z->_t)",
605 " { printf(\" line %%3d \\\"%%s\\\" \",",
606 " src_all[i].src[z->_p], PanSource);",
607 " break;",
608 " }",
609
610 " printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",",
611 " z->_p, t_id, t->forw, q?q:\"\");",
612
613 " c_globals();",
614 " for (i = 0; i < now._nr_pr; i++)",
615 " { c_locals(i, ((P0 *)pptr(i))->_t);",
616 " }",
617 " } else",
618 " if (strcmp(procname[z->_t], \":never:\") == 0)",
619 " { if (lastnever != (int) z->_p)",
620 " { for (i = 0; src_all[i].src; i++)",
621 " if (src_all[i].tp == (int) z->_t)",
622 " { printf(\"MSC: ~G %%d\\n\",",
623 " src_all[i].src[z->_p]);",
624 " break;",
625 " }",
626 " if (!src_all[i].src)",
627 " printf(\"MSC: ~R %%d\\n\", z->_p);",
628 " }",
629 " lastnever = z->_p;",
630 " goto sameas;",
631 " } else",
632 " if (strcmp(procname[z->_t], \":np_:\") != 0)",
633 " {",
634 "sameas: if (no_rck) goto moveon;",
635 " if (coltrace)",
636 " { printf(\"%%ld: \", depth);",
637 " for (i = 0; i < II; i++)",
638 " printf(\"\\t\\t\");",
639 " printf(\"%%s(%%d):\", procname[z->_t], II);",
640 " printf(\"[%%s]\\n\", q?q:\"\");",
641 " } else if (!silent)",
642 " { if (strlen(simvals) > 0) {",
643 " printf(\"%%3ld: proc %%2d (%%s)\", ",
644 " depth, II, procname[z->_t]);",
645 " for (i = 0; src_all[i].src; i++)",
646 " if (src_all[i].tp == (int) z->_t)",
647 " { printf(\" line %%3d \\\"%%s\\\" \",",
648 " src_all[i].src[z->_p], PanSource);",
649 " break;",
650 " }",
651 " printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
652 " }",
653 " printf(\"%%3ld: proc %%2d (%%s)\", ",
654 " depth, II, procname[z->_t]);",
655 " for (i = 0; src_all[i].src; i++)",
656 " if (src_all[i].tp == (int) z->_t)",
657 " { printf(\" line %%3d \\\"%%s\\\" \",",
658 " src_all[i].src[z->_p], PanSource);",
659 " break;",
660 " }",
661 " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
662 " /* printf(\"\\n\"); */",
663 " } }",
664 "moveon: z->_p = t->st;",
665 " }",
666 " wrap_trail();",
667 "}",
668 "#endif",
669 "int",
670 "f_pid(int pt)",
671 "{ int i;",
672 " P0 *z;",
673 " for (i = 0; i < now._nr_pr; i++)",
674 " { z = (P0 *)pptr(i);",
675 " if (z->_t == (unsigned) pt)",
676 " return BASE+z->_pid;",
677 " }",
678 " return -1;",
679 "}",
680 "#ifdef VERI",
681 "void check_claim(int);",
682 "#endif",
683 "",
684 "#if !defined(HASH64) && !defined(HASH32)",
685 " #define HASH32",
686 "#endif",
687 "#if defined(HASH32) && defined(SAFETY) && !defined(SFH) && !defined(SPACE)",
688 " #define SFH",
689 "#endif",
690 "#if defined(SFH) && (defined(BITSTATE) || defined(COLLAPSE) || defined(HC) || defined(HASH64))",
691 " #undef SFH", /* need 2 hash fcts, for which Jenkins is best */
692 "#endif", /* or a 64 bit hash, which we dont have for SFH */
693 "#if defined(SFH) && !defined(NOCOMP)",
694 " #define NOCOMP /* go for speed */",
695 "#endif",
696 "#if NCORE>1 && !defined(GLOB_HEAP)",
697 " #define SEP_HEAP /* version 5.1.2 */",
698 "#endif",
699 "",
700 "#ifdef BITSTATE",
701 #ifndef POWOW
702 "int",
703 "bstore_mod(char *v, int n) /* hasharray size not a power of two */",
704 "{ unsigned long x, y;",
705 " unsigned int i = 1;",
706 "",
707 " d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
708 " x = K1; y = j3;", /* was K2 before 5.1.1 */
709 " for (;;)",
710 " { if (!(SS[x%%udmem]&(1<<y))) break;", /* take the hit in speed */
711 " if (i == hfns) {",
712 "#ifdef DEBUG",
713 " printf(\"Old bitstate\\n\");",
714 "#endif",
715 " return 1;",
716 " }",
717 " x = (x + K2 + i);", /* no mask, using mod - was K1 before 5.1.1 */
718 " y = (y + j4) & 7;",
719 " i++;",
720 " }",
721 "#ifdef RANDSTOR",
722 " if (rand()%%100 > RANDSTOR) return 0;",
723 "#endif",
724 " for (;;)",
725 " { SS[x%%udmem] |= (1<<y);",
726 " if (i == hfns) break;", /* done */
727 " x = (x + K2 + i);", /* no mask - was K1 before 5.1.1 */
728 " y = (y + j4) & 7;",
729 " i++;",
730 " }",
731 "#ifdef DEBUG",
732 " printf(\"New bitstate\\n\");",
733 "#endif",
734 " if (now._a_t&1)",
735 " { nShadow++;",
736 " }",
737 " return 0;",
738 "}",
739 #endif
740 "int",
741 "bstore_reg(char *v, int n) /* extended hashing, Peter Dillinger, 2004 */",
742 "{ unsigned long x, y;",
743 " unsigned int i = 1;",
744 "",
745 " d_hash((uchar *) v, n); /* sets j1-j4 */",
746 " x = j2; y = j3;",
747 " for (;;)",
748 " { if (!(SS[x]&(1<<y))) break;", /* at least one bit not set */
749 " if (i == hfns) {",
750 "#ifdef DEBUG",
751 " printf(\"Old bitstate\\n\");",
752 "#endif",
753 " return 1;",
754 " }",
755 " x = (x + j1 + i) & nmask;",
756 " y = (y + j4) & 7;",
757 " i++;",
758 " }",
759 "#ifdef RANDSTOR",
760 " if (rand()%%100 > RANDSTOR) return 0;",
761 "#endif",
762 " for (;;)",
763 " { SS[x] |= (1<<y);",
764 " if (i == hfns) break;", /* done */
765 " x = (x + j1 + i) & nmask;",
766 " y = (y + j4) & 7;",
767 " i++;",
768 " }",
769 "#ifdef DEBUG",
770 " printf(\"New bitstate\\n\");",
771 "#endif",
772 " if (now._a_t&1)",
773 " { nShadow++;",
774 " }",
775 " return 0;",
776 "}",
777 "#endif", /* BITSTATE */
778 "unsigned long TMODE = 0666; /* file permission bits for trail files */",
779 "",
780 "int trcnt=1;",
781 "char snap[64], fnm[512];",
782 "",
783 "int",
784 "make_trail(void)",
785 "{ int fd;",
786 " char *q;",
787 " char MyFile[512];",
788 " int w_flags = O_CREAT|O_WRONLY|O_TRUNC;",
789 "",
790 " if (exclusive == 1 && iterative == 0)",
791 " { w_flags |= O_EXCL;",
792 " }",
793 "",
794 " q = strrchr(TrailFile, \'/\');",
795 " if (q == NULL) q = TrailFile; else q++;",
796 " strcpy(MyFile, q); /* TrailFile is not a writable string */",
797 "",
798 " if (iterative == 0 && Nr_Trails++ > 0)",
799 " { sprintf(fnm, \"%%s%%d.%%s\",",
800 " MyFile, Nr_Trails-1, tprefix);",
801 " } else",
802 " {",
803 "#ifdef PUTPID",
804 " sprintf(fnm, \"%%s%%d.%%s\", MyFile, getpid(), tprefix);",
805 "#else",
806 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
807 "#endif",
808 " }",
809 #if 1
810 " if ((fd = open(fnm, w_flags, TMODE)) < 0)",
811 #else
812 " if ((fd = creat(fnm, TMODE)) < 0)",
813 #endif
814 " { if ((q = strchr(MyFile, \'.\')))",
815 " { *q = \'\\0\';", /* strip .pml */
816 " if (iterative == 0 && Nr_Trails-1 > 0)",
817 " sprintf(fnm, \"%%s%%d.%%s\",",
818 " MyFile, Nr_Trails-1, tprefix);",
819 " else",
820 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
821 " *q = \'.\';",
822 #if 1
823 " fd = open(fnm, w_flags, TMODE);",
824 #else
825 " fd = creat(fnm, TMODE);",
826 #endif
827 " } }",
828 " if (fd < 0)",
829 " { printf(\"pan: cannot create %%s\\n\", fnm);",
830 " perror(\"cause\");",
831 " } else",
832 " {",
833 "#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))",
834 " void write_root(void); ",
835 " write_root();",
836 "#else",
837 " printf(\"pan: wrote %%s\\n\", fnm);",
838 "#endif",
839 " }",
840 " return fd;",
841 "}",
842 "",
843 "#ifndef FREQ",
844 "#define FREQ (1000000)",
845 "#endif",
846 0
847 };
848
849 static char *Code2b[] = { /* breadth-first search option */
850 "#ifdef BFS",
851 "#define Q_PROVISO",
852 "#ifndef INLINE_REV",
853 "#define INLINE_REV",
854 "#endif",
855 "",
856 "typedef struct SV_Hold {",
857 " State *sv;",
858 " int sz;",
859 " struct SV_Hold *nxt;",
860 "} SV_Hold;",
861 "",
862 "typedef struct EV_Hold {",
863 " char *sv;", /* Mask */
864 " int sz;", /* vsize */
865 " int nrpr;",
866 " int nrqs;",
867 " char *po;",
868 " char *qo;",
869 " char *ps, *qs;",
870 " struct EV_Hold *nxt;",
871 "} EV_Hold;",
872 "",
873 "typedef struct BFS_Trail {",
874 " Trail *frame;",
875 " SV_Hold *onow;",
876 " EV_Hold *omask;",
877 "#ifdef Q_PROVISO",
878 " struct H_el *lstate;",
879 "#endif",
880 " short boq;",
881 " struct BFS_Trail *nxt;",
882 "} BFS_Trail;",
883 "",
884 "BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
885 "",
886 "SV_Hold *svhold, *svfree;",
887 "",
888 "#ifdef BFS_DISK",
889 "#ifndef BFS_LIMIT",
890 " #define BFS_LIMIT 100000",
891 "#endif",
892 "#ifndef BFS_DSK_LIMIT",
893 " #define BFS_DSK_LIMIT 1000000",
894 "#endif",
895
896 "#if defined(WIN32) || defined(WIN64)",
897 " #define RFLAGS (O_RDONLY|O_BINARY)",
898 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
899 "#else",
900 " #define RFLAGS (O_RDONLY)",
901 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)",
902 "#endif",
903
904 "long bfs_size_limit;",
905 "int bfs_dsk_write = -1;",
906 "int bfs_dsk_read = -1;",
907 "long bfs_dsk_writes, bfs_dsk_reads;",
908 "int bfs_dsk_seqno_w, bfs_dsk_seqno_r;",
909 "#endif",
910 "",
911 "uchar do_reverse(Trans *, short, uchar);",
912 "void snapshot(void);",
913 "",
914 "SV_Hold *",
915 "getsv(int n)",
916 "{ SV_Hold *h = (SV_Hold *) 0, *oh;",
917 "",
918 " oh = (SV_Hold *) 0;",
919 " for (h = svfree; h; oh = h, h = h->nxt)",
920 " { if (n == h->sz)",
921 " { if (!oh)",
922 " svfree = h->nxt;",
923 " else",
924 " oh->nxt = h->nxt;",
925 " h->nxt = (SV_Hold *) 0;",
926 " break;",
927 " }",
928 " if (n < h->sz)",
929 " { h = (SV_Hold *) 0;",
930 " break;",
931 " }",
932 " /* else continue */",
933 " }",
934 "",
935 " if (!h)",
936 " { h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
937 " h->sz = n;",
938 "#ifdef BFS_DISK",
939 " if (bfs_size_limit >= BFS_LIMIT)",
940 " { h->sv = (State *) 0; /* means: read disk */",
941 " bfs_dsk_writes++; /* count */",
942 " if (bfs_dsk_write < 0 /* file descriptor */",
943 " || bfs_dsk_writes%%BFS_DSK_LIMIT == 0)",
944 " { char dsk_nm[32];",
945 " if (bfs_dsk_write >= 0)",
946 " { (void) close(bfs_dsk_write);",
947 " }",
948 " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_w++);",
949 " bfs_dsk_write = open(dsk_nm, WFLAGS, 0644);",
950 " if (bfs_dsk_write < 0)",
951 " { Uerror(\"could not create tmp disk file\");",
952 " }",
953 " printf(\"pan: created disk file %%s\\n\", dsk_nm);",
954 " }",
955 " if (write(bfs_dsk_write, (char *) &now, n) != n)",
956 " { Uerror(\"aborting -- disk write failed (disk full?)\");",
957 " }",
958 " return h; /* no memcpy */",
959 " }", /* else */
960 " bfs_size_limit++;",
961 "#endif",
962 " h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
963 " }",
964 "",
965 " memcpy((char *)h->sv, (char *)&now, n);",
966 " return h;",
967 "}",
968 "",
969 "EV_Hold *",
970 "getsv_mask(int n)",
971 "{ EV_Hold *h;",
972 " static EV_Hold *kept = (EV_Hold *) 0;",
973 "",
974 " for (h = kept; h; h = h->nxt)",
975 " if (n == h->sz",
976 " && (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
977 " && (now._nr_pr == h->nrpr)",
978 " && (now._nr_qs == h->nrqs)",
979 "#if VECTORSZ>32000",
980 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
981 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
982 "#else",
983 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
984 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
985 "#endif",
986 " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
987 " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
988 " break;",
989 " if (!h)",
990 " { h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
991 " h->sz = n;",
992 " h->nrpr = now._nr_pr;",
993 " h->nrqs = now._nr_qs;",
994 "",
995 " h->sv = (char *) emalloc(n * sizeof(char));",
996 " memcpy((char *) h->sv, (char *) Mask, n);",
997 "",
998 " if (now._nr_pr > 0)",
999 " { h->ps = (char *) emalloc(now._nr_pr * sizeof(int));",
1000 " memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(uchar));",
1001 "#if VECTORSZ>32000",
1002 " h->po = (char *) emalloc(now._nr_pr * sizeof(int));",
1003 " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
1004 "#else",
1005 " h->po = (char *) emalloc(now._nr_pr * sizeof(short));",
1006 " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
1007 "#endif",
1008 " }",
1009 " if (now._nr_qs > 0)",
1010 " { h->qs = (char *) emalloc(now._nr_qs * sizeof(int));",
1011 " memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(uchar));",
1012 "#if VECTORSZ>32000",
1013 " h->qo = (char *) emalloc(now._nr_qs * sizeof(int));",
1014 " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
1015 "#else",
1016 " h->qo = (char *) emalloc(now._nr_qs * sizeof(short));",
1017 " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
1018 "#endif",
1019 " }",
1020 "",
1021 " h->nxt = kept;",
1022 " kept = h;",
1023 " }",
1024 " return h;",
1025 "}",
1026 "",
1027 "void",
1028 "freesv(SV_Hold *p)",
1029 "{ SV_Hold *h, *oh;",
1030 "",
1031 " oh = (SV_Hold *) 0;",
1032 " for (h = svfree; h; oh = h, h = h->nxt)",
1033 " if (h->sz >= p->sz)",
1034 " break;",
1035 "",
1036 " if (!oh)",
1037 " { p->nxt = svfree;",
1038 " svfree = p;",
1039 " } else",
1040 " { p->nxt = h;",
1041 " oh->nxt = p;",
1042 " }",
1043 "}",
1044 "",
1045 "BFS_Trail *",
1046 "get_bfs_frame(void)",
1047 "{ BFS_Trail *t;",
1048 "",
1049 " if (bfs_free)",
1050 " { t = bfs_free;",
1051 " bfs_free = bfs_free->nxt;",
1052 " t->nxt = (BFS_Trail *) 0;",
1053 " } else",
1054 " { t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
1055 " }",
1056 " t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
1057 " return t;",
1058 "}",
1059 "",
1060 "void",
1061 "push_bfs(Trail *f, int d)",
1062 "{ BFS_Trail *t;",
1063 "",
1064 " t = get_bfs_frame();",
1065 " memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
1066 " t->frame->o_tt = d; /* depth */",
1067 "",
1068 " t->boq = boq;",
1069 " t->onow = getsv(vsize);",
1070 " t->omask = getsv_mask(vsize);",
1071 "#if defined(FULLSTACK) && defined(Q_PROVISO)",
1072 " t->lstate = Lstate;",
1073 "#endif",
1074 " if (!bfs_bot)",
1075 " { bfs_bot = bfs_trail = t;",
1076 " } else",
1077 " { bfs_bot->nxt = t;",
1078 " bfs_bot = t;",
1079 " }",
1080 "#ifdef CHECK",
1081 " printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
1082 "#endif",
1083 "}",
1084 "",
1085 "Trail *",
1086 "pop_bfs(void)",
1087 "{ BFS_Trail *t;",
1088 "",
1089 " if (!bfs_trail)",
1090 " return (Trail *) 0;",
1091 "",
1092 " t = bfs_trail;",
1093 " bfs_trail = t->nxt;",
1094 " if (!bfs_trail)",
1095 " bfs_bot = (BFS_Trail *) 0;",
1096 "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
1097 " if (t->lstate) t->lstate->tagged = 0;",
1098 "#endif",
1099 "",
1100 " t->nxt = bfs_free;",
1101 " bfs_free = t;",
1102 "",
1103 " vsize = t->onow->sz;",
1104 " boq = t->boq;",
1105 "#ifdef BFS_DISK",
1106 " if (t->onow->sv == (State *) 0)",
1107 " { char dsk_nm[32];",
1108 " bfs_dsk_reads++; /* count */",
1109 " if (bfs_dsk_read >= 0 /* file descriptor */",
1110 " && bfs_dsk_reads%%BFS_DSK_LIMIT == 0)",
1111 " { (void) close(bfs_dsk_read);",
1112 " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r-1);",
1113 " (void) unlink(dsk_nm);",
1114 " bfs_dsk_read = -1;",
1115 " }",
1116 " if (bfs_dsk_read < 0)",
1117 " { sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r++);",
1118 " bfs_dsk_read = open(dsk_nm, RFLAGS);",
1119 " if (bfs_dsk_read < 0)",
1120 " { Uerror(\"could not open temp disk file\");",
1121 " } }",
1122 " if (read(bfs_dsk_read, (char *) &now, vsize) != vsize)",
1123 " { Uerror(\"bad bfs disk file read\");",
1124 " }",
1125 "#ifndef NOVSZ",
1126 " if (now._vsz != vsize)",
1127 " { Uerror(\"disk read vsz mismatch\");",
1128 " }",
1129 "#endif",
1130 " } else",
1131 "#endif",
1132 " memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
1133 " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
1134
1135 " if (now._nr_pr > 0)",
1136 "#if VECTORSZ>32000",
1137 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
1138 "#else",
1139 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
1140 "#endif",
1141 " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
1142 " }",
1143 " if (now._nr_qs > 0)",
1144 "#if VECTORSZ>32000",
1145 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
1146 "#else",
1147 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
1148 "#endif",
1149 " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
1150 " }",
1151
1152 "#ifdef BFS_DISK",
1153 " if (t->onow->sv != (State *) 0)",
1154 "#endif",
1155 " freesv(t->onow); /* omask not freed */",
1156 "#ifdef CHECK",
1157 " printf(\"POP %%u (%%d)\\n\", t->frame, t->frame->o_tt);",
1158 "#endif",
1159 " return t->frame;",
1160 "}",
1161 "",
1162 "void",
1163 "store_state(Trail *ntrpt, int shortcut, short oboq)",
1164 "{",
1165 "#ifdef VERI",
1166 " Trans *t2 = (Trans *) 0;",
1167 " uchar ot; int tt, E_state;",
1168 " uchar o_opm = trpt->o_pm, *othis = this;",
1169 "",
1170 " if (shortcut)",
1171 " {",
1172 "#ifdef VERBOSE",
1173 " printf(\"claim: shortcut\\n\");",
1174 "#endif",
1175 " goto store_it; /* no claim move */",
1176 " }",
1177 "",
1178 " this = (((uchar *)&now)+proc_offset[0]); /* 0 = never claim */",
1179 " trpt->o_pm = 0;", /* to interpret else in never claim */
1180 "",
1181 " tt = (int) ((P0 *)this)->_p;",
1182 " ot = (uchar) ((P0 *)this)->_t;",
1183 "",
1184 "#ifdef HAS_UNLESS",
1185 " E_state = 0;",
1186 "#endif",
1187 " for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
1188 " {",
1189 "#ifdef HAS_UNLESS",
1190 " if (E_state > 0",
1191 " && E_state != t2->e_trans)",
1192 " break;",
1193 "#endif",
1194 " if (do_transit(t2, 0))",
1195 " {",
1196 "#ifdef VERBOSE",
1197 " if (!reached[ot][t2->st])",
1198 " printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",",
1199 " trpt->o_tt, ((P0 *)this)->_p, t2->st);",
1200 "#endif",
1201 "#ifdef HAS_UNLESS",
1202 " E_state = t2->e_trans;",
1203 "#endif",
1204 " if (t2->st > 0)",
1205 " { ((P0 *)this)->_p = t2->st;",
1206 " reached[ot][t2->st] = 1;",
1207 "#ifndef NOCLAIM",
1208 " check_claim(t2->st);",
1209 "#endif",
1210 " }",
1211 " if (now._nr_pr == 0) /* claim terminated */",
1212 " uerror(\"end state in claim reached\");",
1213 "",
1214 "#ifdef PEG",
1215 " peg[t2->forw]++;",
1216 "#endif",
1217 " trpt->o_pm |= 1;",
1218 " if (t2->atom&2)", /* atomic in claim */
1219 " Uerror(\"atomic in claim not supported in BFS mode\");",
1220 "store_it:",
1221 "",
1222 "#endif", /* VERI */
1223 "",
1224 "#ifdef BITSTATE",
1225 " if (!bstore((char *)&now, vsize))",
1226 "#else",
1227 "#ifdef MA",
1228 " if (!gstore((char *)&now, vsize, 0))",
1229 "#else",
1230 " if (!hstore((char *)&now, vsize))",
1231 "#endif",
1232 "#endif",
1233 " { static long sdone = (long) 0; long ndone;",
1234 " nstates++;",
1235 "#ifndef NOREDUCE",
1236 " trpt->tau |= 64;", /* succ definitely outside stack */
1237 "#endif",
1238 " ndone = (unsigned long) (nstates/((double) FREQ));",
1239 " if (ndone != sdone && mreached%%10 != 0)",
1240 " { snapshot();",
1241 " sdone = ndone;",
1242 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
1243 " if (nstates > ((double)(1<<(ssize+1))))",
1244 " { void resize_hashtable(void);",
1245 " resize_hashtable();",
1246 " }",
1247 "#endif",
1248 " }",
1249 "#if SYNC",
1250 " if (boq != -1)",
1251 " midrv++;",
1252 " else if (oboq != -1)",
1253 " { Trail *x;",
1254 " x = (Trail *) trpt->ostate; /* pre-rv state */",
1255 " if (x) x->o_pm |= 4; /* mark success */",
1256 " }",
1257 "#endif",
1258 " push_bfs(ntrpt, trpt->o_tt+1);",
1259 " } else",
1260 " { truncs++;",
1261
1262 "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
1263 "#if !defined(BITSTATE)",
1264 " if (Lstate && Lstate->tagged) trpt->tau |= 64;",
1265 "#else",
1266 " if (trpt->tau&32)",
1267 " { BFS_Trail *tprov;",
1268 " for (tprov = bfs_trail; tprov; tprov = tprov->nxt)",
1269 " if (tprov->onow->sv != (State *) 0",
1270 " && memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize) == 0)",
1271 " { trpt->tau |= 64;",
1272 " break; /* state is in queue */",
1273 " } }",
1274 "#endif",
1275 "#endif",
1276 " }",
1277 "#ifdef VERI",
1278 " ((P0 *)this)->_p = tt; /* reset claim */",
1279 " if (t2)",
1280 " do_reverse(t2, 0, 0);",
1281 " else",
1282 " break;",
1283 " } }",
1284 " this = othis;",
1285 " trpt->o_pm = o_opm;",
1286 "#endif",
1287 "}",
1288 "",
1289 "Trail *ntrpt;", /* 4.2.8 */
1290 "",
1291 "void",
1292 "bfs(void)",
1293 "{ Trans *t; Trail *otrpt, *x;",
1294 " uchar _n, _m, ot, nps = 0;",
1295 " int tt, E_state;",
1296 " short II, From = (short) (now._nr_pr-1), To = BASE;",
1297 " short oboq = boq;",
1298 "",
1299 " ntrpt = (Trail *) emalloc(sizeof(Trail));",
1300 " trpt->ostate = (struct H_el *) 0;",
1301 " trpt->tau = 0;",
1302 "",
1303 " trpt->o_tt = -1;",
1304 " store_state(ntrpt, 0, oboq); /* initial state */",
1305 "",
1306 " while ((otrpt = pop_bfs())) /* also restores now */",
1307 " { memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));",
1308 "#if defined(C_States) && (HAS_TRACK==1)",
1309 " c_revert((uchar *) &(now.c_state[0]));",
1310 "#endif",
1311 " if (trpt->o_pm & 4)",
1312 " {",
1313 "#ifdef VERBOSE",
1314 " printf(\"Revisit of atomic not needed (%%d)\\n\",",
1315 " trpt->o_pm);", /* at least 1 rv succeeded */
1316 "#endif",
1317 " continue;",
1318 " }",
1319 "#ifndef NOREDUCE",
1320 " nps = 0;",
1321 "#endif",
1322 " if (trpt->o_pm == 8)",
1323 " { revrv++;",
1324 " if (trpt->tau&8)",
1325 " {",
1326 "#ifdef VERBOSE",
1327 " printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
1328 " trpt->o_pm, trpt->tau);",
1329 "#endif",
1330 " trpt->tau &= ~8;",
1331 " }",
1332 "#ifndef NOREDUCE",
1333 " else if (trpt->tau&32)", /* was a preselected move */
1334 " {",
1335 "#ifdef VERBOSE",
1336 " printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
1337 " trpt->o_pm, trpt->tau);",
1338 "#endif",
1339 " trpt->tau &= ~32;",
1340 " nps = 1; /* no preselection in repeat */",
1341 " }",
1342 "#endif",
1343 " }",
1344 " trpt->o_pm &= ~(4|8);",
1345 " if (trpt->o_tt > mreached)",
1346 " { mreached = trpt->o_tt;",
1347 " if (mreached%%10 == 0)",
1348 " { snapshot();",
1349 " } }",
1350 " depth = trpt->o_tt;",
1351
1352 " if (depth >= maxdepth)",
1353 " {",
1354 "#if SYNC",
1355 " Trail *x;",
1356 " if (boq != -1)",
1357 " { x = (Trail *) trpt->ostate;",
1358 " if (x) x->o_pm |= 4; /* not failing */",
1359 " }",
1360 "#endif",
1361 " truncs++;",
1362 " if (!warned)",
1363 " { warned = 1;",
1364 " printf(\"error: max search depth too small\\n\");",
1365 " }",
1366 " if (bounded)",
1367 " uerror(\"depth limit reached\");",
1368 " continue;",
1369 " }",
1370
1371 /* PO */
1372 "#ifndef NOREDUCE",
1373 " if (boq == -1 && !(trpt->tau&8) && nps == 0)",
1374 " for (II = now._nr_pr-1; II >= BASE; II -= 1)",
1375 " {",
1376 "Pickup: this = pptr(II);",
1377 " tt = (int) ((P0 *)this)->_p;",
1378 " ot = (uchar) ((P0 *)this)->_t;",
1379 " if (trans[ot][tt]->atom & 8)", /* safe */
1380 " { t = trans[ot][tt];",
1381 " if (t->qu[0] != 0)",
1382 " { Ccheck++;",
1383 " if (!q_cond(II, t))",
1384 " continue;",
1385 " Cholds++;",
1386 " }",
1387 " From = To = II;",
1388 " trpt->tau |= 32; /* preselect marker */",
1389 "#ifdef DEBUG",
1390 " printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
1391 " depth, II, trpt->tau);",
1392 "#endif",
1393 " goto MainLoop;",
1394 " } }",
1395 " trpt->tau &= ~32;", /* not preselected */
1396 "#endif",
1397 /* PO */
1398 "Repeat:",
1399 " if (trpt->tau&8) /* atomic */",
1400 " { From = To = (short ) trpt->pr;",
1401 " nlinks++;",
1402 " } else",
1403 " { From = now._nr_pr-1;",
1404 " To = BASE;",
1405 " }",
1406 "MainLoop:",
1407 " _n = _m = 0;",
1408 " for (II = From; II >= To; II -= 1)",
1409 " {",
1410 " this = (((uchar *)&now)+proc_offset[II]);",
1411 " tt = (int) ((P0 *)this)->_p;",
1412 " ot = (uchar) ((P0 *)this)->_t;",
1413 "#if SYNC",
1414 " /* no rendezvous with same proc */",
1415 " if (boq != -1 && trpt->pr == II) continue;",
1416 "#endif",
1417 " ntrpt->pr = (uchar) II;",
1418 " ntrpt->st = tt; ",
1419 " trpt->o_pm &= ~1; /* no move yet */",
1420 "#ifdef EVENT_TRACE",
1421 " trpt->o_event = now._event;",
1422 "#endif",
1423 "#ifdef HAS_PROVIDED",
1424 " if (!provided(II, ot, tt, t)) continue;",
1425 "#endif",
1426 "#ifdef HAS_UNLESS",
1427 " E_state = 0;",
1428 "#endif",
1429 " for (t = trans[ot][tt]; t; t = t->nxt)",
1430 " {",
1431 "#ifdef HAS_UNLESS",
1432 " if (E_state > 0",
1433 " && E_state != t->e_trans)",
1434 " break;",
1435 "#endif",
1436 " ntrpt->o_t = t;",
1437 "",
1438 " oboq = boq;",
1439 "",
1440 " if (!(_m = do_transit(t, II)))",
1441 " continue;",
1442 "",
1443 " trpt->o_pm |= 1; /* we moved */",
1444 " (trpt+1)->o_m = _m; /* for unsend */",
1445 "#ifdef PEG",
1446 " peg[t->forw]++;",
1447 "#endif",
1448 "#ifdef CHECK",
1449 " printf(\"%%3d: proc %%d exec %%d, \",",
1450 " depth, II, t->forw);",
1451 " printf(\"%%d to %%d, %%s %%s %%s\",",
1452 " tt, t->st, t->tp,",
1453 " (t->atom&2)?\"atomic\":\"\",",
1454 " (boq != -1)?\"rendez-vous\":\"\");",
1455 "#ifdef HAS_UNLESS",
1456 " if (t->e_trans)",
1457 " printf(\" (escapes to state %%d)\", t->st);",
1458 "#endif",
1459 " printf(\" %%saccepting [tau=%%d]\\n\",",
1460 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
1461 "#endif",
1462 "#ifdef HAS_UNLESS",
1463 " E_state = t->e_trans;",
1464 "#if SYNC>0",
1465 " if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
1466 " { fprintf(efd, \"error:\tthe use of rendezvous stmnt in the escape clause\\n\");",
1467 " fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
1468 " pan_exit(1);",
1469 " }",
1470 "#endif",
1471 "#endif",
1472 " if (t->st > 0) ((P0 *)this)->_p = t->st;",
1473 "",
1474 " /* ptr to pred: */ ntrpt->ostate = (struct H_el *) otrpt;",
1475 " ntrpt->st = tt;",
1476 " if (boq == -1 && (t->atom&2)) /* atomic */",
1477 " ntrpt->tau = 8; /* record for next move */",
1478 " else",
1479 " ntrpt->tau = 0;",
1480 "",
1481 " store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
1482 "#ifdef EVENT_TRACE",
1483 " now._event = trpt->o_event;",
1484 "#endif",
1485 "",
1486 " /* undo move and continue */",
1487 " trpt++; /* this is where ovals and ipt are set */",
1488 " do_reverse(t, II, _m); /* restore now. */",
1489 " trpt--;",
1490 "#ifdef CHECK",
1491 " #if NCORE>1",
1492 " enter_critical(GLOBAL_LOCK); /* in verbose mode only */",
1493 " printf(\"cpu%%d: \", core_id);",
1494 " #endif",
1495
1496 " printf(\"%%3d: proc %%d \", depth, II);",
1497 " printf(\"reverses %%d, %%d to %%d,\",",
1498 " t->forw, tt, t->st);",
1499 " printf(\" %%s [abit=%%d,adepth=%%d,\",",
1500 " t->tp, now._a_t, A_depth);",
1501 " printf(\"tau=%%d,%%d]\\n\",",
1502 " trpt->tau, (trpt-1)->tau);",
1503 " #if NCORE>1",
1504 " leave_critical(GLOBAL_LOCK);",
1505 " #endif",
1506 "#endif",
1507 " reached[ot][t->st] = 1;",
1508 " reached[ot][tt] = 1;",
1509 "",
1510 " ((P0 *)this)->_p = tt;",
1511 " _n |= _m;",
1512 " } }",
1513 /* PO */
1514 "#ifndef NOREDUCE",
1515 " /* preselected - no succ definitely outside stack */",
1516 " if ((trpt->tau&32) && !(trpt->tau&64))",
1517 " { From = now._nr_pr-1; To = BASE;",
1518 "#ifdef DEBUG",
1519 " cpu_printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
1520 " depth, II+1, (int) _n, trpt->tau);",
1521 "#endif",
1522 " _n = 0; trpt->tau &= ~32;",
1523 " if (II >= BASE)",
1524 " goto Pickup;",
1525 " goto MainLoop;",
1526 " }",
1527 " trpt->tau &= ~(32|64);",
1528 "#endif",
1529 /* PO */
1530 " if (_n != 0)",
1531 " continue;",
1532 "#ifdef DEBUG",
1533 " printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
1534 " depth, II, trpt->tau, boq, now._nr_pr);",
1535 "#endif",
1536 " if (boq != -1)",
1537 " { failedrv++;",
1538 " x = (Trail *) trpt->ostate; /* pre-rv state */",
1539 " if (!x) continue; /* root state */",
1540 " if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
1541 " { x->o_pm |= 8; /* mark failure */",
1542 " this = (((uchar *)&now)+proc_offset[otrpt->pr]);",
1543 "#ifdef VERBOSE",
1544 " printf(\"\\treset state of %%d from %%d to %%d\\n\",",
1545 " otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
1546 "#endif",
1547 " ((P0 *)this)->_p = otrpt->st;",
1548 " unsend(boq); /* retract rv offer */",
1549 " boq = -1;",
1550
1551 " push_bfs(x, x->o_tt);",
1552 "#ifdef VERBOSE",
1553 " printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
1554 "#endif",
1555 " }",
1556 "#ifdef VERBOSE",
1557 " else printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
1558 "#endif",
1559 " } else if (now._nr_pr > 0)",
1560 " {",
1561 " if ((trpt->tau&8)) /* atomic */",
1562 " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */",
1563 "#ifdef DEBUG",
1564 " printf(\"%%3d: atomic step proc %%d blocks\\n\",",
1565 " depth, II+1);",
1566 "#endif",
1567 " goto Repeat;",
1568 " }",
1569 "",
1570 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
1571 " { trpt->tau |= 1;",
1572 "#ifdef DEBUG",
1573 " printf(\"%%d: timeout\\n\", depth);",
1574 "#endif",
1575 " goto MainLoop;",
1576 " }",
1577 "#ifndef VERI",
1578 " if (!noends && !a_cycles && !endstate())",
1579 " uerror(\"invalid end state\");",
1580 "#endif",
1581 " } }",
1582 "}",
1583 "",
1584 "void",
1585 "putter(Trail *trpt, int fd)",
1586 "{ long j;",
1587 "",
1588 " if (!trpt) return;",
1589 "",
1590 " if (trpt != (Trail *) trpt->ostate)",
1591 " putter((Trail *) trpt->ostate, fd);",
1592 "",
1593 " if (trpt->o_t)",
1594 " { sprintf(snap, \"%%d:%%d:%%d\\n\",",
1595 " trcnt++, trpt->pr, trpt->o_t->t_id);",
1596 " j = strlen(snap);",
1597 " if (write(fd, snap, j) != j)",
1598 " { printf(\"pan: error writing %%s\\n\", fnm);",
1599 " pan_exit(1);",
1600 " } }",
1601 "}",
1602 "",
1603 "void",
1604 "nuerror(char *str)",
1605 "{ int fd = make_trail();",
1606 " int j;",
1607 "",
1608 " if (fd < 0) return;",
1609 "#ifdef VERI",
1610 " sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
1611 " write(fd, snap, strlen(snap));",
1612 "#endif",
1613 "#ifdef MERGED",
1614 " sprintf(snap, \"-4:-4:-4\\n\");",
1615 " write(fd, snap, strlen(snap));",
1616 "#endif",
1617 " trcnt = 1;",
1618 " putter(trpt, fd);",
1619 " if (ntrpt->o_t)", /* 4.2.8 -- Alex example, missing last transition */
1620 " { sprintf(snap, \"%%d:%%d:%%d\\n\",",
1621 " trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
1622 " j = strlen(snap);",
1623 " if (write(fd, snap, j) != j)",
1624 " { printf(\"pan: error writing %%s\\n\", fnm);",
1625 " pan_exit(1);",
1626 " } }",
1627 " close(fd);",
1628 " if (errors >= upto && upto != 0)",
1629 " { wrapup();",
1630 " }",
1631 "}",
1632 "#endif", /* BFS */
1633 0,
1634 };
1635
1636 static char *Code2d[] = {
1637 "clock_t start_time;",
1638 "#if NCORE>1",
1639 "clock_t crash_stamp;",
1640 "#endif",
1641 "#if !defined(WIN32) && !defined(WIN64)",
1642 "struct tms start_tm;",
1643 "#endif",
1644 "",
1645 "void",
1646 "start_timer(void)",
1647 "{",
1648 "#if defined(WIN32) || defined(WIN64)",
1649 " start_time = clock();",
1650 "#else",
1651 " start_time = times(&start_tm);",
1652 "#endif",
1653 "}",
1654 "",
1655 "void",
1656 "stop_timer(void)",
1657 "{ clock_t stop_time;",
1658 " double delta_time;",
1659 "#if !defined(WIN32) && !defined(WIN64)",
1660 " struct tms stop_tm;",
1661 " stop_time = times(&stop_tm);",
1662 " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
1663 "#else",
1664 " stop_time = clock();",
1665 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
1666 "#endif",
1667 " if (readtrail || delta_time < 0.00) return;",
1668 "#if NCORE>1",
1669 " if (core_id == 0 && nstates > (double) 0)",
1670 " { printf(\"\\ncpu%%d: elapsed time %%.3g seconds (%%g states visited)\\n\", core_id, delta_time, nstates);",
1671 " if (delta_time > 0.01)",
1672 " { printf(\"cpu%%d: rate %%g states/second\\n\", core_id, nstates/delta_time);",
1673 " }",
1674 " { void check_overkill(void);",
1675 " check_overkill();",
1676 " } }",
1677 "#else",
1678 " printf(\"\\npan: elapsed time %%.3g seconds\\n\", delta_time);",
1679 " if (delta_time > 0.01)",
1680 " { printf(\"pan: rate %%9.8g states/second\\n\", nstates/delta_time);",
1681 " if (verbose)",
1682 " { printf(\"pan: avg transition delay %%.5g usec\\n\",",
1683 " delta_time/(nstates+truncs));",
1684 " } }",
1685 "#endif",
1686 "}",
1687 "",
1688 "#if NCORE>1",
1689 "#ifdef T_ALERT",
1690 "double t_alerts[17];",
1691 "",
1692 "void",
1693 "crash_report(void)",
1694 "{ int i;",
1695 " printf(\"crash alert intervals:\\n\");",
1696 " for (i = 0; i < 17; i++)",
1697 " { printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);",
1698 "} }",
1699 "#endif",
1700 "",
1701 "void",
1702 "crash_reset(void)",
1703 "{ /* false alarm */",
1704 " if (crash_stamp != (clock_t) 0)",
1705 " {",
1706 "#ifdef T_ALERT",
1707 " double delta_time;",
1708 " int i;",
1709 "#if defined(WIN32) || defined(WIN64)",
1710 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1711 "#else",
1712 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1713 "#endif",
1714 " for (i = 0; i < 16; i++)",
1715 " { if (delta_time <= (i*30))",
1716 " { t_alerts[i] = delta_time;",
1717 " break;",
1718 " } }",
1719 " if (i == 16) t_alerts[i] = delta_time;",
1720 "#endif",
1721 " if (verbose)",
1722 " printf(\"cpu%%d: crash alert off\\n\", core_id);",
1723 " }",
1724 " crash_stamp = (clock_t) 0;",
1725 "}",
1726 "",
1727 "int",
1728 "crash_test(double maxtime)",
1729 "{ double delta_time;",
1730 " if (crash_stamp == (clock_t) 0)",
1731 " { /* start timing */",
1732 "#if defined(WIN32) || defined(WIN64)",
1733 " crash_stamp = clock();",
1734 "#else",
1735 " crash_stamp = times(&start_tm);",
1736 "#endif",
1737 " if (verbose)",
1738 " { printf(\"cpu%%d: crash detection\\n\", core_id);",
1739 " }",
1740 " return 0;",
1741 " }",
1742 "#if defined(WIN32) || defined(WIN64)",
1743 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1744 "#else",
1745 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1746 "#endif",
1747 " return (delta_time >= maxtime);",
1748 "}",
1749 "#endif",
1750 "",
1751 "void",
1752 "do_the_search(void)",
1753 "{ int i;",
1754 " depth = mreached = 0;",
1755 " trpt = &trail[0];",
1756 "#ifdef VERI",
1757 " trpt->tau |= 4; /* the claim moves first */",
1758 "#endif",
1759 " for (i = 0; i < (int) now._nr_pr; i++)",
1760 " { P0 *ptr = (P0 *) pptr(i);",
1761 "#ifndef NP",
1762 " if (!(trpt->o_pm&2)",
1763 " && accpstate[ptr->_t][ptr->_p])",
1764 " { trpt->o_pm |= 2;",
1765 " }",
1766 "#else",
1767 " if (!(trpt->o_pm&4)",
1768 " && progstate[ptr->_t][ptr->_p])",
1769 " { trpt->o_pm |= 4;",
1770 " }",
1771 "#endif",
1772 " }",
1773 "#ifdef EVENT_TRACE",
1774 "#ifndef NP",
1775 " if (accpstate[EVENT_TRACE][now._event])",
1776 " { trpt->o_pm |= 2;",
1777 " }",
1778 "#else",
1779 " if (progstate[EVENT_TRACE][now._event])",
1780 " { trpt->o_pm |= 4;",
1781 " }",
1782 "#endif",
1783 "#endif",
1784 "#ifndef NOCOMP",
1785 " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */",
1786 " if (!a_cycles)",
1787 " { i = &(now._a_t) - (uchar *) &now;",
1788 " Mask[i] = 1; /* _a_t */",
1789 " }",
1790 "#ifndef NOFAIR",
1791 " if (!fairness)",
1792 " { int j = 0;",
1793 " i = &(now._cnt[0]) - (uchar *) &now;",
1794 " while (j++ < NFAIR)",
1795 " Mask[i++] = 1; /* _cnt[] */",
1796 " }",
1797 "#endif",
1798 "#endif",
1799 "#ifndef NOFAIR",
1800 " if (fairness",
1801 " && (a_cycles && (trpt->o_pm&2)))",
1802 " { now._a_t = 2; /* set the A-bit */",
1803 " now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */
1804 "#ifdef VERBOSE",
1805 " printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
1806 " depth, now._cnt[now._a_t&1], now._a_t);",
1807 "#endif",
1808 " }",
1809 "#endif",
1810
1811 " c_stack_start = (char *) &i; /* meant to be read-only */",
1812
1813 "#if defined(HAS_CODE) && defined (C_INIT)",
1814 " C_INIT; /* initialization of data that must precede fork() */",
1815 " c_init_done++;",
1816 "#endif",
1817
1818 "#if defined(C_States) && (HAS_TRACK==1)",
1819 " /* capture initial state of tracked C objects */",
1820 " c_update((uchar *) &(now.c_state[0]));",
1821 "#endif",
1822
1823 "#ifdef HAS_CODE",
1824 " if (readtrail) getrail(); /* no return */",
1825 "#endif",
1826 " start_timer();",
1827 "#ifdef BFS",
1828 " bfs();",
1829 "#else",
1830 "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
1831 " /* initial state of tracked & unmatched objects */",
1832 " c_stack((uchar *) &(svtack->c_stack[0]));",
1833 "#endif",
1834 "#ifdef RANDOMIZE",
1835 " #if RANDOMIZE>0",
1836 " srand(RANDOMIZE);",
1837 " #else",
1838 " srand(123);",
1839 " #endif",
1840 "#endif",
1841 "#if NCORE>1",
1842 " mem_get();",
1843 "#else",
1844 " new_state(); /* start 1st DFS */",
1845 "#endif",
1846 "#endif",
1847 "}",
1848
1849 "#ifdef INLINE_REV",
1850 "uchar",
1851 "do_reverse(Trans *t, short II, uchar M)",
1852 "{ uchar _m = M;",
1853 " int tt = (int) ((P0 *)this)->_p;",
1854 "#include REVERSE_MOVES",
1855 "R999: return _m;",
1856 "}",
1857 "#endif",
1858
1859 "#ifndef INLINE",
1860 "#ifdef EVENT_TRACE",
1861 "static char _tp = 'n'; static int _qid = 0;",
1862 "#endif",
1863 "uchar",
1864 "do_transit(Trans *t, short II)",
1865 "{ uchar _m = 0;",
1866 " int tt = (int) ((P0 *)this)->_p;",
1867 "#ifdef M_LOSS",
1868 " uchar delta_m = 0;",
1869 "#endif",
1870 "#ifdef EVENT_TRACE",
1871 " short oboq = boq;",
1872 " uchar ot = (uchar) ((P0 *)this)->_t;",
1873 " if (ot == EVENT_TRACE) boq = -1;",
1874 "#define continue { boq = oboq; return 0; }",
1875 "#else",
1876 "#define continue return 0",
1877 "#ifdef SEPARATE",
1878 " uchar ot = (uchar) ((P0 *)this)->_t;",
1879 "#endif",
1880 "#endif",
1881 "#include FORWARD_MOVES",
1882 "P999:",
1883 "#ifdef EVENT_TRACE",
1884 " if (ot == EVENT_TRACE) boq = oboq;",
1885 "#endif",
1886 " return _m;",
1887 "#undef continue",
1888 "}",
1889
1890 "#ifdef EVENT_TRACE",
1891 "void",
1892 "require(char tp, int qid)",
1893 "{ Trans *t;",
1894 " _tp = tp; _qid = qid;",
1895 "",
1896 " if (now._event != endevent)",
1897 " for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
1898 " { if (do_transit(t, EVENT_TRACE))",
1899 " { now._event = t->st;",
1900 " reached[EVENT_TRACE][t->st] = 1;",
1901 "#ifdef VERBOSE",
1902 " printf(\" event_trace move to -> %%d\\n\", t->st);",
1903 "#endif",
1904 "#ifndef BFS",
1905 "#ifndef NP",
1906 " if (accpstate[EVENT_TRACE][now._event])",
1907 " (trpt+1)->o_pm |= 2;",
1908 "#else",
1909 " if (progstate[EVENT_TRACE][now._event])",
1910 " (trpt+1)->o_pm |= 4;",
1911 "#endif",
1912 "#endif",
1913 "#ifdef NEGATED_TRACE",
1914 " if (now._event == endevent)",
1915 " {",
1916 "#ifndef BFS",
1917 " depth++; trpt++;",
1918 "#endif",
1919 " uerror(\"event_trace error (all events matched)\");",
1920 "#ifndef BFS",
1921 " trpt--; depth--;",
1922 "#endif",
1923 " break;",
1924 " }",
1925 "#endif",
1926 " for (t = t->nxt; t; t = t->nxt)",
1927 " { if (do_transit(t, EVENT_TRACE))",
1928 " Uerror(\"non-determinism in event-trace\");",
1929 " }",
1930 " return;",
1931 " }",
1932 "#ifdef VERBOSE",
1933 " else",
1934 " printf(\" event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
1935 " tp, qid, now._event, t->forw);",
1936 "#endif",
1937 " }",
1938 "#ifdef NEGATED_TRACE",
1939 " now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
1940 "#else",
1941 "#ifndef BFS",
1942 " depth++; trpt++;",
1943 "#endif",
1944 " uerror(\"event_trace error (no matching event)\");",
1945 "#ifndef BFS",
1946 " trpt--; depth--;",
1947 "#endif",
1948 "#endif",
1949 "}",
1950 "#endif",
1951
1952 "int",
1953 "enabled(int iam, int pid)",
1954 "{ Trans *t; uchar *othis = this;",
1955 " int res = 0; int tt; uchar ot;",
1956 "#ifdef VERI",
1957 " /* if (pid > 0) */ pid++;",
1958 "#endif",
1959 " if (pid == iam)",
1960 " Uerror(\"used: enabled(pid=thisproc)\");",
1961 " if (pid < 0 || pid >= (int) now._nr_pr)",
1962 " return 0;",
1963 " this = pptr(pid);",
1964 " TstOnly = 1;",
1965 " tt = (int) ((P0 *)this)->_p;",
1966 " ot = (uchar) ((P0 *)this)->_t;",
1967 " for (t = trans[ot][tt]; t; t = t->nxt)",
1968 " if (do_transit(t, (short) pid))",
1969 " { res = 1;",
1970 " break;",
1971 " }",
1972 " TstOnly = 0;",
1973 " this = othis;",
1974 " return res;",
1975 "}",
1976 "#endif",
1977 "void",
1978 "snap_time(void)",
1979 "{ clock_t stop_time;",
1980 " double delta_time;",
1981 "#if !defined(WIN32) && !defined(WIN64)",
1982 " struct tms stop_tm;",
1983 " stop_time = times(&stop_tm);",
1984 " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
1985 "#else",
1986 " stop_time = clock();",
1987 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
1988 "#endif",
1989 " if (delta_time > 0.01)",
1990 " { printf(\"t= %%6.3g \", delta_time);",
1991 " printf(\"R= %%7.0g\", nstates/delta_time);",
1992 " }",
1993 " printf(\"\\n\");",
1994 " if (quota > 0.1 && delta_time > quota)",
1995 " { printf(\"Time limit of %%6.3g minutes exceeded\\n\", quota/60.0);",
1996 "#if NCORE>1",
1997 " fflush(stdout);",
1998 " leave_critical(GLOBAL_LOCK);",
1999 " sudden_stop(\"time-limit\");",
2000 " exit(1);",
2001 "#endif",
2002 " wrapup();",
2003 " }",
2004 "}",
2005 "void",
2006 "snapshot(void)",
2007 "{",
2008 "#if NCORE>1",
2009 " enter_critical(GLOBAL_LOCK); /* snapshot */",
2010 " printf(\"cpu%%d: \", core_id);",
2011 "#endif",
2012 " printf(\"Depth= %%7ld States= %%8.3g \",",
2013 "#if NCORE>1",
2014 " (long) (nr_handoffs * z_handoff) +",
2015 "#endif",
2016 " mreached, nstates);",
2017 " printf(\"Transitions= %%8.3g \", nstates+truncs);",
2018 "#ifdef MA",
2019 " printf(\"Nodes= %%7d \", nr_states);",
2020 "#endif",
2021 " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
2022 " snap_time();",
2023 " fflush(stdout);",
2024 "#if NCORE>1",
2025 " leave_critical(GLOBAL_LOCK);",
2026 "#endif",
2027 "}",
2028
2029 "#ifdef SC",
2030 "void",
2031 "stack2disk(void)",
2032 "{",
2033 " if (!stackwrite",
2034 " && (stackwrite = creat(stackfile, TMODE)) < 0)",
2035 " Uerror(\"cannot create stackfile\");",
2036 "",
2037 " if (write(stackwrite, trail, DDD*sizeof(Trail))",
2038 " != DDD*sizeof(Trail))",
2039 " Uerror(\"stackfile write error -- disk is full?\");",
2040 "",
2041 " memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
2042 " memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
2043 " CNT1++;",
2044 "}",
2045 "void",
2046 "disk2stack(void)",
2047 "{ long have;",
2048 "",
2049 " CNT2++;",
2050 " memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
2051 "",
2052 " if (!stackwrite",
2053 " || lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
2054 " Uerror(\"disk2stack lseek error\");",
2055 "",
2056 " if (!stackread",
2057 " && (stackread = open(stackfile, 0)) < 0)",
2058 " Uerror(\"cannot open stackfile\");",
2059 "",
2060 " if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
2061 " Uerror(\"disk2stack lseek error\");",
2062 "",
2063 " have = read(stackread, trail, DDD*sizeof(Trail));",
2064 " if (have != DDD*sizeof(Trail))",
2065 " Uerror(\"stackfile read error\");",
2066 "}",
2067 "#endif",
2068
2069 "uchar *",
2070 "Pptr(int x)", /* as a fct, to avoid a problem with the p9 compiler */
2071 "{ if (x < 0 || x >= MAXPROC || !proc_offset[x])", /* does not exist */
2072 " return noptr;",
2073 " else",
2074 " return (uchar *) pptr(x);",
2075 "}",
2076 "int qs_empty(void);",
2077
2078 "/*",
2079 " * new_state() is the main DFS search routine in the verifier",
2080 " * it has a lot of code ifdef-ed together to support",
2081 " * different search modes, which makes it quite unreadable.",
2082 " * if you are studying the code, first use the C preprocessor",
2083 " * to generate a specific version from the pan.c source,",
2084 " * e.g. by saying:",
2085 " * gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
2086 " * and then study the resulting file, rather than this one",
2087 " */",
2088 "#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
2089 "",
2090 "#ifdef NSUCC",
2091 "int N_succ[512];",
2092 "void",
2093 "tally_succ(int cnt)",
2094 "{ if (cnt < 512) N_succ[cnt]++;",
2095 " else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);",
2096 "}",
2097 "",
2098 "void",
2099 "dump_succ(void)",
2100 "{ int i; double sum = 0.0;",
2101 " double w_avg = 0.0;",
2102 " printf(\"Successor counts:\\n\");",
2103 " for (i = 0; i < 512; i++)",
2104 " { sum += (double) N_succ[i];",
2105 " }",
2106 " for (i = 0; i < 512; i++)",
2107 " { if (N_succ[i] > 0)",
2108 " { printf(\"%%3d\t%%10d\t(%%.4g %%%% of total)\\n\",",
2109 " i, N_succ[i], (100.0 * (double) N_succ[i])/sum);",
2110 " w_avg += (double) i * (double) N_succ[i];",
2111 " } }",
2112 " if (sum > N_succ[0])",
2113 " printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));",
2114 "}",
2115 "#endif",
2116 "",
2117 "void",
2118 "new_state(void)",
2119 "{ Trans *t;",
2120 " uchar _n, _m, ot;",
2121 "#ifdef RANDOMIZE",
2122 " short ooi, eoi;",
2123 "#endif",
2124 "#ifdef M_LOSS",
2125 " uchar delta_m = 0;",
2126 "#endif",
2127 " short II, JJ = 0, kk;",
2128 " int tt;",
2129 "#ifdef REVERSE",
2130 " short From = BASE, To = now._nr_pr-1;",
2131 "#else",
2132 " short From = now._nr_pr-1, To = BASE;",
2133 "#endif",
2134 "Down:",
2135 "#ifdef CHECK",
2136 " cpu_printf(\"%%d: Down - %%s %%saccepting [pids %%d-%%d]\\n\",",
2137 " depth, (trpt->tau&4)?\"claim\":\"program\",",
2138 " (trpt->o_pm&2)?\"\":\"non-\", From, To);",
2139 "#endif",
2140 "#ifdef SCHED",
2141 " if (depth > 0)",
2142 " { trpt->sched_limit = (trpt-1)->sched_limit;",
2143 " } else",
2144 " { trpt->sched_limit = 0;",
2145 " }",
2146 "#endif",
2147
2148 "#ifdef SC",
2149 " if (depth > hiwater)",
2150 " { stack2disk();",
2151 " maxdepth += DDD;",
2152 " hiwater += DDD;",
2153 " trpt -= DDD;",
2154 " if(verbose)",
2155 " printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",",
2156 " CNT1, hiwater, maxdepth);",
2157 " }",
2158 "#endif",
2159
2160 " trpt->tau &= ~(16|32|64); /* make sure these are off */",
2161 "#if defined(FULLSTACK) && defined(MA)",
2162 " trpt->proviso = 0;",
2163 "#endif",
2164 "#ifdef NSUCC",
2165 " trpt->n_succ = 0;",
2166 "#endif",
2167 "#if NCORE>1",
2168 " if (mem_hand_off())",
2169 " {",
2170 "#if SYNC",
2171 " (trpt+1)->o_n = 1; /* not a deadlock: as below */",
2172 "#endif",
2173 "#ifndef LOOPSTATE",
2174 " (trpt-1)->tau |= 16; /* worstcase guess: as below */",
2175 "#endif",
2176 "#if NCORE>1 && defined(FULL_TRAIL)",
2177 " if (upto > 0)",
2178 " { Pop_Stack_Tree();",
2179 " }",
2180 "#endif",
2181 " goto Up;",
2182 " }",
2183 "#endif",
2184
2185 " if (depth >= maxdepth)",
2186 " { if (!warned)",
2187 " { warned = 1;",
2188 " printf(\"error: max search depth too small\\n\");",
2189 " }",
2190 " if (bounded)",
2191 " { uerror(\"depth limit reached\");",
2192 " }",
2193 " truncs++;",
2194 "#if SYNC",
2195 " (trpt+1)->o_n = 1; /* not a deadlock */",
2196 "#endif",
2197 "#ifndef LOOPSTATE",
2198 " (trpt-1)->tau |= 16; /* worstcase guess */",
2199 "#endif",
2200
2201 "#if NCORE>1 && defined(FULL_TRAIL)",
2202 " if (upto > 0)",
2203 " { Pop_Stack_Tree();",
2204 " }",
2205 "#endif",
2206 " goto Up;",
2207 " }",
2208 "AllOver:",
2209 "#if (defined(FULLSTACK) && !defined(MA)) || NCORE>1",
2210 " /* if atomic or rv move, carry forward previous state */",
2211 " trpt->ostate = (trpt-1)->ostate;", /* was: = (struct H_el *) 0;*/
2212 "#endif",
2213 "#ifdef VERI",
2214 " if ((trpt->tau&4) || ((trpt-1)->tau&128))",
2215 "#endif",
2216 " if (boq == -1) { /* if not mid-rv */",
2217 "#ifndef SAFETY",
2218 " /* this check should now be redundant",
2219 " * because the seed state also appears",
2220 " * on the 1st dfs stack and would be",
2221 " * matched in hstore below",
2222 " */",
2223 " if ((now._a_t&1) && depth > A_depth)",
2224 " { if (!memcmp((char *)&A_Root, ",
2225 " (char *)&now, vsize))",
2226 " {",
2227 " depthfound = A_depth;",
2228 "#ifdef CHECK",
2229 " printf(\"matches seed\\n\");",
2230 "#endif",
2231 "#ifdef NP",
2232 " uerror(\"non-progress cycle\");",
2233 "#else",
2234 " uerror(\"acceptance cycle\");",
2235 "#endif",
2236 "#if NCORE>1 && defined(FULL_TRAIL)",
2237 " if (upto > 0)",
2238 " { Pop_Stack_Tree();",
2239 " }",
2240 "#endif",
2241 " goto Up;",
2242 " }",
2243 "#ifdef CHECK",
2244 " printf(\"not seed\\n\");",
2245 "#endif",
2246 " }",
2247 "#endif",
2248 " if (!(trpt->tau&8)) /* if no atomic move */",
2249 " {",
2250 "#ifdef BITSTATE",
2251 "#ifdef CNTRSTACK", /* -> bitstate, reduced, safety */
2252 " II = bstore((char *)&now, vsize);",
2253 " trpt->j6 = j1; trpt->j7 = j2;",
2254 " JJ = LL[j1] && LL[j2];",
2255 "#else",
2256 "#ifdef FULLSTACK",
2257 " JJ = onstack_now();", /* sets j1 */
2258 "#else",
2259 "#ifndef NOREDUCE",
2260 " JJ = II; /* worstcase guess for p.o. */",
2261 "#endif",
2262 "#endif",
2263 " II = bstore((char *)&now, vsize);", /* sets j1-j4 */
2264 "#endif",
2265 "#else",
2266 "#ifdef MA",
2267 " II = gstore((char *)&now, vsize, 0);",
2268 "#ifndef FULLSTACK",
2269 " JJ = II;",
2270 "#else",
2271 " JJ = (II == 2)?1:0;",
2272 "#endif",
2273 "#else",
2274 " II = hstore((char *)&now, vsize);",
2275 "#ifdef FULLSTACK",
2276 " JJ = (II == 2)?1:0;",
2277 "#endif",
2278 "#endif",
2279 "#endif",
2280 " kk = (II == 1 || II == 2);",
2281
2282 /* II==0 new state */
2283 /* II==1 old state */
2284 /* II==2 on current dfs stack */
2285 /* II==3 on 1st dfs stack */
2286 "#ifndef SAFETY",
2287
2288 "#if NCORE==1 || defined (SEP_STATE)", /* or else we don't know which stack its on */
2289 " if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
2290 " #ifndef NOFAIR",
2291 "#if 0",
2292 " if (!fairness || ((now._a_t&1) && now._cnt[1] == 1)) /* 5.1.4 */",
2293 "#else",
2294 " if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */",
2295 "#endif",
2296 " #endif",
2297 " {",
2298 " II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
2299 "#ifdef VERBOSE",
2300 " printf(\"state match on dfs stack\\n\");",
2301 "#endif",
2302 " goto same_case;",
2303 " }",
2304 "#endif",
2305
2306 "#if defined(FULLSTACK) && defined(BITSTATE)",
2307 " if (!JJ && (now._a_t&1) && depth > A_depth)",
2308 " { int oj1 = j1;",
2309 " uchar o_a_t = now._a_t;",
2310 " now._a_t &= ~(1|16|32);", /* 1st stack */
2311 " if (onstack_now())", /* changes j1 */
2312 " { II = 3;",
2313 "#ifdef VERBOSE",
2314 " printf(\"state match on 1st dfs stack\\n\");",
2315 "#endif",
2316 " }",
2317 " now._a_t = o_a_t;", /* restore */
2318 " j1 = oj1;",
2319 " }",
2320 "#endif",
2321 " if (II == 3 && a_cycles && (now._a_t&1))",
2322 " {",
2323 "#ifndef NOFAIR",
2324 " if (fairness && now._cnt[1] > 1) /* was != 0 */",
2325 " {",
2326 "#ifdef VERBOSE",
2327 " printf(\"\tfairness count non-zero\\n\");",
2328 "#endif",
2329 " II = 0;", /* treat as new state */
2330 " } else",
2331 "#endif",
2332 " {",
2333 "#ifndef BITSTATE",
2334 " nShadow--;",
2335 "#endif",
2336 "same_case: if (Lstate) depthfound = Lstate->D;",
2337 "#ifdef NP",
2338 " uerror(\"non-progress cycle\");",
2339 "#else",
2340 " uerror(\"acceptance cycle\");",
2341 "#endif",
2342 "#if NCORE>1 && defined(FULL_TRAIL)",
2343 " if (upto > 0)",
2344 " { Pop_Stack_Tree();",
2345 " }",
2346 "#endif",
2347 " goto Up;",
2348 " }",
2349 " }",
2350 "#endif",
2351
2352 "#ifndef NOREDUCE",
2353 "#ifndef SAFETY",
2354 "#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
2355 " if (II != 0 && (!Lstate || Lstate->cpu_id < core_id))",
2356 " { (trpt-1)->tau |= 16;", /* treat as a stack state */
2357 " }",
2358 "#endif",
2359 " if ((II && JJ) || (II == 3))",
2360 " { /* marker for liveness proviso */",
2361 "#ifndef LOOPSTATE",
2362 " (trpt-1)->tau |= 16;", /* truncated on stack */
2363 "#endif",
2364 " truncs2++;",
2365 " }",
2366 "#else",
2367 "#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
2368 " if (!(II != 0 && (!Lstate || Lstate->cpu_id < core_id)))",
2369 " { /* treat as stack state */",
2370 " (trpt-1)->tau |= 16;",
2371 " } else",
2372 " { /* treat as non-stack state */",
2373 " (trpt-1)->tau |= 64;",
2374 " }",
2375 "#endif",
2376 " if (!II || !JJ)",
2377 " { /* successor outside stack */",
2378 " (trpt-1)->tau |= 64;",
2379 " }",
2380 "#endif",
2381 "#endif",
2382 " if (II)",
2383 " { truncs++;",
2384 "#if NCORE>1 && defined(FULL_TRAIL)",
2385 " if (upto > 0)",
2386 " { Pop_Stack_Tree();",
2387 " if (depth == 0)",
2388 " { return;",
2389 " } }",
2390 "#endif",
2391 " goto Up;",
2392 " }",
2393 " if (!kk)",
2394 " { static long sdone = (long) 0; long ndone;",
2395 " nstates++;",
2396 "#if defined(ZAPH) && defined(BITSTATE)",
2397 " zstates += (double) hfns;",
2398 "#endif",
2399 " ndone = (unsigned long) (nstates/((double) FREQ));",
2400 " if (ndone != sdone)",
2401 " { snapshot();",
2402 " sdone = ndone;",
2403 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
2404 " if (nstates > ((double)(ONE_L<<(ssize+1))))",
2405 " { void resize_hashtable(void);",
2406 " resize_hashtable();",
2407 " }",
2408 "#endif",
2409 "#if defined(ZAPH) && defined(BITSTATE)",
2410 " if (zstates > ((double)(ONE_L<<(ssize-2))))",
2411 " { /* more than half the bits set */",
2412 " void zap_hashtable(void);",
2413 " zap_hashtable();",
2414 " zstates = 0;",
2415 " }",
2416 "#endif",
2417 " }",
2418 "#ifdef SVDUMP",
2419 " if (vprefix > 0)",
2420 " if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
2421 " { fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);",
2422 " wrapup();",
2423 " }",
2424 "#endif",
2425 "#if defined(MA) && defined(W_XPT)",
2426 " if ((unsigned long) nstates%%W_XPT == 0)",
2427 " { void w_xpoint(void);",
2428 " w_xpoint();",
2429 " }",
2430 "#endif",
2431 " }",
2432
2433 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
2434 " onstack_put();",
2435 "#ifdef DEBUG2",
2436 "#if defined(FULLSTACK) && !defined(MA)",
2437 " printf(\"%%d: putting %%u (%%d)\\n\", depth,",
2438 " trpt->ostate, ",
2439 " (trpt->ostate)?trpt->ostate->tagged:0);",
2440 "#else",
2441 " printf(\"%%d: putting\\n\", depth);",
2442 "#endif",
2443 "#endif",
2444 "#else",
2445 " #if NCORE>1",
2446 " trpt->ostate = Lstate;",
2447 " #endif",
2448 "#endif",
2449 " } }",
2450
2451
2452 " if (depth > mreached)",
2453 " mreached = depth;",
2454 "#ifdef VERI",
2455 " if (trpt->tau&4)",
2456 "#endif",
2457 " trpt->tau &= ~(1|2); /* timeout and -request off */",
2458 " _n = 0;",
2459 "#if SYNC",
2460 " (trpt+1)->o_n = 0;",
2461 "#endif",
2462 "#ifdef VERI",
2463 " if (now._nr_pr == 0) /* claim terminated */",
2464 " uerror(\"end state in claim reached\");",
2465 " check_claim(((P0 *)pptr(0))->_p);",
2466 "Stutter:",
2467 " if (trpt->tau&4) /* must make a claimmove */",
2468 " {",
2469
2470 "#ifndef NOFAIR",
2471 " if ((now._a_t&2) /* A-bit set */",
2472 " && now._cnt[now._a_t&1] == 1)",
2473 " { now._a_t &= ~2;",
2474 " now._cnt[now._a_t&1] = 0;",
2475 " trpt->o_pm |= 16;",
2476 "#ifdef DEBUG",
2477 " printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
2478 " depth, now._a_t);",
2479 "#endif",
2480 " }",
2481 "#endif",
2482
2483 " II = 0; /* never */",
2484 " goto Veri0;",
2485 " }",
2486 "#endif",
2487 "#ifndef NOREDUCE",
2488 " /* Look for a process with only safe transitions */",
2489 " /* (special rules apply in the 2nd dfs) */",
2490 " if (boq == -1 && From != To",
2491 "",
2492 "#ifdef SAFETY",
2493 " #if NCORE>1",
2494 " && (depth < z_handoff)", /* not for border states */
2495 " #endif",
2496 " )",
2497 "#else",
2498 " #if NCORE>1",
2499 " && ((a_cycles) || (!a_cycles && depth < z_handoff))",
2500 " #endif",
2501 " && (!(now._a_t&1)",
2502 " || (a_cycles &&",
2503 " #ifndef BITSTATE",
2504 "#ifdef MA",
2505 "#ifdef VERI",
2506 " !((trpt-1)->proviso))",
2507 "#else",
2508 " !(trpt->proviso))",
2509 "#endif",
2510 "#else",
2511 "#ifdef VERI",
2512 " (trpt-1)->ostate &&",
2513 " !(((char *)&((trpt-1)->ostate->state))[0] & 128))", /* proviso bit in _a_t */
2514 "#else",
2515 " !(((char *)&(trpt->ostate->state))[0] & 128))",
2516 "#endif",
2517 "#endif",
2518 " #else",
2519 "#ifdef VERI",
2520 " (trpt-1)->ostate &&",
2521 " (trpt-1)->ostate->proviso == 0)",
2522 "#else",
2523 " trpt->ostate->proviso == 0)",
2524 "#endif",
2525 " #endif",
2526 " ))",
2527 "#endif", /* SAFETY */
2528 "",
2529 "#ifdef REVERSE",
2530 " for (II = From; II <= To; II++)",
2531 "#else",
2532 " for (II = From; II >= To; II--)",
2533 "#endif",
2534 " {",
2535 "Resume: /* pick up here if preselect fails */",
2536 " this = pptr(II);",
2537 " tt = (int) ((P0 *)this)->_p;",
2538 " ot = (uchar) ((P0 *)this)->_t;",
2539 " if (trans[ot][tt]->atom & 8)",
2540 " { t = trans[ot][tt];",
2541 " if (t->qu[0] != 0)",
2542 " { Ccheck++;",
2543 " if (!q_cond(II, t))",
2544 " continue;",
2545 " Cholds++;",
2546 " }",
2547 " From = To = II; /* the process preselected */",
2548 "#ifdef NIBIS",
2549 " t->om = 0;",
2550 "#endif",
2551 " trpt->tau |= 32; /* preselect marker */",
2552 "#ifdef DEBUG",
2553 "#ifdef NIBIS",
2554 " printf(\"%%3d: proc %%d Pre\", depth, II);",
2555 " printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
2556 " t->om, trpt->tau);",
2557 "#else",
2558 " printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
2559 " depth, II, trpt->tau);",
2560 "#endif",
2561 "#endif",
2562 " goto Again;",
2563 " }",
2564 " }",
2565 " trpt->tau &= ~32;",
2566 "#endif",
2567 "#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
2568 "Again:",
2569 "#endif",
2570
2571 " /* The Main Expansion Loop over Processes */",
2572
2573 " trpt->o_pm &= ~(8|16|32|64); /* fairness-marks */",
2574 "#ifndef NOFAIR",
2575 " if (fairness && boq == -1",
2576 "#ifdef VERI",
2577 " && (!(trpt->tau&4) && !((trpt-1)->tau&128))",
2578 "#endif",
2579 " && !(trpt->tau&8))",
2580 " { /* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
2581 " if (!(now._a_t&2))", /* A-bit not set */
2582 " {",
2583 " if (a_cycles && (trpt->o_pm&2))",
2584 " { /* Accepting state */",
2585 " now._a_t |= 2;",
2586 " now._cnt[now._a_t&1] = now._nr_pr + 1;", /* NEW +1 */
2587 " trpt->o_pm |= 8;",
2588 "#ifdef DEBUG",
2589 " printf(\"%%3d: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
2590 " depth, now._cnt[now._a_t&1], now._a_t);",
2591 "#endif",
2592 " }",
2593 " } else", /* A-bit set */
2594 " { /* A_bit = 0 when Cnt 0 */",
2595 " if (now._cnt[now._a_t&1] == 1)",
2596 " { now._a_t &= ~2;", /* reset a-bit */
2597 " now._cnt[now._a_t&1] = 0;",
2598 " trpt->o_pm |= 16;",
2599 "#ifdef DEBUG",
2600 " printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
2601 " depth, now._a_t);",
2602 "#endif",
2603 " } } }",
2604 "#endif",
2605 "",
2606 "#ifdef REVERSE",
2607 " for (II = From; II <= To; II++)",
2608 "#else",
2609 " for (II = From; II >= To; II--)",
2610 "#endif",
2611 " {",
2612 "#if SYNC",
2613 " /* no rendezvous with same proc */",
2614 " if (boq != -1 && trpt->pr == II) continue;",
2615 "#endif",
2616 "#ifdef SCHED",
2617 " /* limit max nr of interleavings */",
2618 " if (From != To", /* not a PO or atomic move */
2619 " && depth > 0", /* there is a prior move */
2620 " #ifdef VERI",
2621 " && II != 0", /* never claim can always move */
2622 " #endif",
2623 " && (trpt-1)->pr != II", /* context switch */
2624 " && trpt->sched_limit >= sched_max)",
2625 " { continue;",
2626 " }",
2627 "#endif",
2628 "#ifdef VERI",
2629 "Veri0:",
2630 "#endif",
2631 " this = pptr(II);",
2632 " tt = (int) ((P0 *)this)->_p;",
2633 " ot = (uchar) ((P0 *)this)->_t;",
2634
2635 "#ifdef NIBIS",
2636 " /* don't repeat a previous preselected expansion */",
2637 " /* could hit this if reduction proviso was false */",
2638 " t = trans[ot][tt];",
2639 " if (!(trpt->tau&4)", /* not claim */
2640 " && !(trpt->tau&1)", /* not timeout */
2641 " && !(trpt->tau&32)", /* not preselected */
2642 " && (t->atom & 8)", /* local */
2643 " && boq == -1", /* not inside rendezvous */
2644 " && From != To)", /* not inside atomic seq */
2645 " { if (t->qu[0] == 0", /* unconditional */
2646 " || q_cond(II, t))", /* true condition */
2647 " { _m = t->om;",
2648 " if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
2649 " continue; /* did it before */",
2650 " } }",
2651 "#endif",
2652 " trpt->o_pm &= ~1; /* no move in this pid yet */",
2653 "#ifdef EVENT_TRACE",
2654 " (trpt+1)->o_event = now._event;",
2655 "#endif",
2656 " /* Fairness: Cnt++ when Cnt == II */",
2657 "#ifndef NOFAIR",
2658 " trpt->o_pm &= ~64; /* didn't apply rule 2 */",
2659 " if (fairness",
2660 " && boq == -1", /* not mid rv - except rcv - NEW 3.0.8 */
2661 " && !(trpt->o_pm&32)", /* Rule 2 not in effect */
2662 " && (now._a_t&2)", /* A-bit is set */
2663 " && now._cnt[now._a_t&1] == II+2)",
2664 " { now._cnt[now._a_t&1] -= 1;",
2665 "#ifdef VERI",
2666 " /* claim need not participate */",
2667 " if (II == 1)",
2668 " now._cnt[now._a_t&1] = 1;",
2669 "#endif",
2670 "#ifdef DEBUG",
2671 " printf(\"%%3d: proc %%d fairness \", depth, II);",
2672 " printf(\"Rule 2: --cnt to %%d (%%d)\\n\",",
2673 " now._cnt[now._a_t&1], now._a_t);",
2674 "#endif",
2675 " trpt->o_pm |= (32|64);",
2676 " }",
2677 "#endif",
2678 "#ifdef HAS_PROVIDED",
2679 " if (!provided(II, ot, tt, t)) continue;",
2680 "#endif",
2681 " /* check all trans of proc II - escapes first */",
2682 "#ifdef HAS_UNLESS",
2683 " trpt->e_state = 0;",
2684 "#endif",
2685 " (trpt+1)->pr = (uchar) II;", /* for uerror */
2686 " (trpt+1)->st = tt;",
2687
2688 "#ifdef RANDOMIZE",
2689 " for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
2690 " { if (strcmp(t->tp, \"else\") == 0)",
2691 " { eoi++;",
2692 " break;",
2693 " } }",
2694 " if (eoi > 0)",
2695 " { t = trans[ot][tt];",
2696 " #ifdef VERBOSE",
2697 " printf(\"randomizer: suppressed, saw else\\n\");",
2698 " #endif",
2699 " } else",
2700 " { eoi = rand()%%ooi;",
2701 " #ifdef VERBOSE",
2702 " printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
2703 " #endif",
2704 " for (t = trans[ot][tt]; t; t = t->nxt)",
2705 " if (eoi-- <= 0) break;",
2706 " }",
2707 "domore:",
2708 " for ( ; t && ooi > 0; t = t->nxt, ooi--)",
2709 "#else", /* ie dont randomize */
2710 " for (t = trans[ot][tt]; t; t = t->nxt)",
2711 "#endif",
2712 " {",
2713 "#ifdef HAS_UNLESS",
2714 " /* exploring all transitions from",
2715 " * a single escape state suffices",
2716 " */",
2717 " if (trpt->e_state > 0",
2718 " && trpt->e_state != t->e_trans)",
2719 " {",
2720 "#ifdef DEBUG",
2721 " printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
2722 " t->e_trans, trpt->e_state);",
2723 "#endif",
2724 " break;",
2725 " }",
2726 "#endif",
2727 " (trpt+1)->o_t = t;", /* for uerror */
2728 "#ifdef INLINE",
2729 "#include FORWARD_MOVES",
2730 "P999: /* jumps here when move succeeds */",
2731 "#else",
2732 " if (!(_m = do_transit(t, II))) continue;",
2733 "#endif",
2734 "#ifdef SCHED",
2735 " if (depth > 0",
2736 " #ifdef VERI",
2737 " && II != 0",
2738 " #endif",
2739 " && (trpt-1)->pr != II)",
2740 " { trpt->sched_limit = 1 + (trpt-1)->sched_limit;",
2741 " }",
2742 "#endif",
2743 " if (boq == -1)",
2744 "#ifdef CTL",
2745 " /* for branching-time, can accept reduction only if */",
2746 " /* the persistent set contains just 1 transition */",
2747 " { if ((trpt->tau&32) && (trpt->o_pm&1))",
2748 " trpt->tau |= 16;", /* CTL */
2749 " trpt->o_pm |= 1; /* we moved */",
2750 " }",
2751 "#else",
2752 " trpt->o_pm |= 1; /* we moved */",
2753 "#endif",
2754
2755 "#ifdef LOOPSTATE",
2756 " if (loopstate[ot][tt])",
2757 " {",
2758 "#ifdef VERBOSE",
2759 " printf(\"exiting from loopstate:\\n\");",
2760 "#endif",
2761 " trpt->tau |= 16;", /* exiting loopstate */
2762 " cnt_loops++;",
2763 " }",
2764 "#endif",
2765
2766 "#ifdef PEG",
2767 " peg[t->forw]++;",
2768 "#endif",
2769 "#if defined(VERBOSE) || defined(CHECK)",
2770 "#if defined(SVDUMP)",
2771 " cpu_printf(\"%%3d: proc %%d exec %%d \\n\", depth, II, t->t_id);",
2772 "#else",
2773 " cpu_printf(\"%%3d: proc %%d exec %%d, %%d to %%d, %%s %%s %%s %%saccepting [tau=%%d]\\n\", ",
2774 " depth, II, t->forw, tt, t->st, t->tp,",
2775 " (t->atom&2)?\"atomic\":\"\",",
2776 " (boq != -1)?\"rendez-vous\":\"\",",
2777 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
2778 "#ifdef HAS_UNLESS",
2779 " if (t->e_trans)",
2780 " cpu_printf(\"\\t(escape to state %%d)\\n\", t->st);",
2781 "#endif",
2782 "#endif",
2783 "#ifdef RANDOMIZE",
2784 " cpu_printf(\"\\t(randomizer %%d)\\n\", ooi);",
2785 "#endif",
2786 "#endif",
2787
2788 "#ifdef HAS_LAST",
2789 "#ifdef VERI",
2790 " if (II != 0)",
2791 "#endif",
2792 " now._last = II - BASE;",
2793 "#endif",
2794 "#ifdef HAS_UNLESS",
2795 " trpt->e_state = t->e_trans;",
2796 "#endif",
2797
2798 " depth++; trpt++;",
2799 " trpt->pr = (uchar) II;",
2800 " trpt->st = tt;",
2801 " trpt->o_pm &= ~(2|4);",
2802 " if (t->st > 0)",
2803 " { ((P0 *)this)->_p = t->st;",
2804 "/* moved down reached[ot][t->st] = 1; */",
2805 " }",
2806 "#ifndef SAFETY",
2807 " if (a_cycles)",
2808 " {",
2809 "#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
2810 " int ii;",
2811 "#endif",
2812 "#define P__Q ((P0 *)pptr(ii))",
2813 "#if ACCEPT_LAB>0",
2814 "#ifdef NP",
2815 " /* state 1 of np_ claim is accepting */",
2816 " if (((P0 *)pptr(0))->_p == 1)",
2817 " trpt->o_pm |= 2;",
2818 "#else",
2819 " for (ii = 0; ii < (int) now._nr_pr; ii++)",
2820 " { if (accpstate[P__Q->_t][P__Q->_p])",
2821 " { trpt->o_pm |= 2;",
2822 " break;",
2823 " } }",
2824 "#endif",
2825 "#endif",
2826 "#if defined(HAS_NP) && PROG_LAB>0",
2827 " for (ii = 0; ii < (int) now._nr_pr; ii++)",
2828 " { if (progstate[P__Q->_t][P__Q->_p])",
2829 " { trpt->o_pm |= 4;",
2830 " break;",
2831 " } }",
2832 "#endif",
2833 "#undef P__Q",
2834 " }",
2835 "#endif",
2836 " trpt->o_t = t; trpt->o_n = _n;",
2837 " trpt->o_ot = ot; trpt->o_tt = tt;",
2838 " trpt->o_To = To; trpt->o_m = _m;",
2839 " trpt->tau = 0;",
2840 "#ifdef RANDOMIZE",
2841 " trpt->oo_i = ooi;",
2842 "#endif",
2843 " if (boq != -1 || (t->atom&2))",
2844 " { trpt->tau |= 8;",
2845 "#ifdef VERI",
2846 " /* atomic sequence in claim */",
2847 " if((trpt-1)->tau&4)",
2848 " trpt->tau |= 4;",
2849 " else",
2850 " trpt->tau &= ~4;",
2851 " } else",
2852 " { if ((trpt-1)->tau&4)",
2853 " trpt->tau &= ~4;",
2854 " else",
2855 " trpt->tau |= 4;",
2856 " }",
2857 " /* if claim allowed timeout, so */",
2858 " /* does the next program-step: */",
2859 " if (((trpt-1)->tau&1) && !(trpt->tau&4))",
2860 " trpt->tau |= 1;",
2861 "#else",
2862 " } else",
2863 " trpt->tau &= ~8;",
2864 "#endif",
2865 " if (boq == -1 && (t->atom&2))",
2866 " { From = To = II; nlinks++;",
2867 " } else",
2868 "#ifdef REVERSE",
2869 " { From = BASE; To = now._nr_pr-1;",
2870 "#else",
2871 " { From = now._nr_pr-1; To = BASE;",
2872 "#endif",
2873 " }",
2874 "#if NCORE>1 && defined(FULL_TRAIL)",
2875 " if (upto > 0)",
2876 " { Push_Stack_Tree(II, t->t_id);",
2877 " }",
2878 "#endif",
2879 " goto Down; /* pseudo-recursion */",
2880 "Up:",
2881 "#ifdef CHECK",
2882 " cpu_printf(\"%%d: Up - %%s\\n\", depth,",
2883 " (trpt->tau&4)?\"claim\":\"program\");",
2884 "#endif",
2885 "#if NCORE>1",
2886 " iam_alive();",
2887 " #ifdef USE_DISK",
2888 " mem_drain();",
2889 " #endif",
2890 "#endif",
2891 "#if defined(MA) || NCORE>1",
2892 " if (depth <= 0) return;",
2893 " /* e.g., if first state is old, after a restart */",
2894 "#endif",
2895
2896 "#ifdef SC",
2897 " if (CNT1 > CNT2",
2898 " && depth < hiwater - (HHH-DDD) + 2)",
2899 " {",
2900 " trpt += DDD;",
2901 " disk2stack();",
2902 " maxdepth -= DDD;",
2903 " hiwater -= DDD;",
2904 " if(verbose)",
2905 " printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
2906 " }",
2907 "#endif",
2908
2909 "#ifndef NOFAIR",
2910 " if (trpt->o_pm&128) /* fairness alg */",
2911 " { now._cnt[now._a_t&1] = trpt->bup.oval;",
2912 " _n = 1; trpt->o_pm &= ~128;",
2913 " depth--; trpt--;",
2914 "#if defined(VERBOSE) || defined(CHECK)",
2915 " printf(\"%%3d: reversed fairness default move\\n\", depth);",
2916 "#endif",
2917 " goto Q999;",
2918 " }",
2919 "#endif",
2920
2921 "#ifdef HAS_LAST",
2922 "#ifdef VERI",
2923 " { int d; Trail *trl;",
2924 " now._last = 0;",
2925 " for (d = 1; d < depth; d++)",
2926 " { trl = getframe(depth-d); /* was (trpt-d) */",
2927 " if (trl->pr != 0)",
2928 " { now._last = trl->pr - BASE;",
2929 " break;",
2930 " } } }",
2931 "#else",
2932 " now._last = (depth<1)?0:(trpt-1)->pr;",
2933 "#endif",
2934 "#endif",
2935 "#ifdef EVENT_TRACE",
2936 " now._event = trpt->o_event;",
2937 "#endif",
2938 "#ifndef SAFETY",
2939 " if ((now._a_t&1) && depth <= A_depth)",
2940 " return; /* to checkcycles() */",
2941 "#endif",
2942 " t = trpt->o_t; _n = trpt->o_n;",
2943 " ot = trpt->o_ot; II = trpt->pr;",
2944 " tt = trpt->o_tt; this = pptr(II);",
2945 " To = trpt->o_To; _m = trpt->o_m;",
2946 "#ifdef RANDOMIZE",
2947 " ooi = trpt->oo_i;",
2948 "#endif",
2949 "#ifdef INLINE_REV",
2950 " _m = do_reverse(t, II, _m);",
2951 "#else",
2952 "#include REVERSE_MOVES",
2953 "R999: /* jumps here when done */",
2954 "#endif",
2955
2956 "#ifdef VERBOSE",
2957 " cpu_printf(\"%%3d: proc %%d reverses %%d, %%d to %%d\\n\",",
2958 " depth, II, t->forw, tt, t->st);",
2959 " cpu_printf(\"\\t%%s [abit=%%d,adepth=%%d,tau=%%d,%%d]\\n\", ",
2960 " t->tp, now._a_t, A_depth, trpt->tau, (trpt-1)->tau);",
2961 "#endif",
2962 "#ifndef NOREDUCE",
2963 " /* pass the proviso tags */",
2964 " if ((trpt->tau&8) /* rv or atomic */",
2965 " && (trpt->tau&16))",
2966 " (trpt-1)->tau |= 16;", /* pass upward */
2967 "#ifdef SAFETY",
2968 " if ((trpt->tau&8) /* rv or atomic */",
2969 " && (trpt->tau&64))",
2970 " (trpt-1)->tau |= 64;",
2971 "#endif",
2972 "#endif",
2973 " depth--; trpt--;",
2974 "",
2975 "#ifdef NSUCC",
2976 " trpt->n_succ++;",
2977 "#endif",
2978 "#ifdef NIBIS",
2979 " (trans[ot][tt])->om = _m; /* head of list */",
2980 "#endif",
2981
2982 " /* i.e., not set if rv fails */",
2983 " if (_m)",
2984 " {",
2985 "#if defined(VERI) && !defined(NP)",
2986 " if (II == 0 && verbose && !reached[ot][t->st])",
2987 " {",
2988 " printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
2989 " depth, t->st, src_claim [t->st]);",
2990 " fflush(stdout);",
2991 " }",
2992 "#endif",
2993 " reached[ot][t->st] = 1;",
2994 " reached[ot][tt] = 1;",
2995 " }",
2996 "#ifdef HAS_UNLESS",
2997 " else trpt->e_state = 0; /* undo */",
2998 "#endif",
2999
3000 " if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
3001 " ((P0 *)this)->_p = tt;",
3002 " } /* all options */",
3003
3004 "#ifdef RANDOMIZE",
3005 " if (!t && ooi > 0)", /* means we skipped some initial options */
3006 " { t = trans[ot][tt];",
3007 " #ifdef VERBOSE",
3008 " printf(\"randomizer: continue for %%d more\\n\", ooi);",
3009 " #endif",
3010 " goto domore;",
3011 " }",
3012 " #ifdef VERBOSE",
3013 " else",
3014 " printf(\"randomizer: done\\n\");",
3015 " #endif",
3016 "#endif",
3017
3018 "#ifndef NOFAIR",
3019 " /* Fairness: undo Rule 2 */",
3020 " if ((trpt->o_pm&32)",/* rule 2 was applied */
3021 " && (trpt->o_pm&64))",/* by this process II */
3022 " { if (trpt->o_pm&1)",/* it didn't block */
3023 " {",
3024 "#ifdef VERI",
3025 " if (now._cnt[now._a_t&1] == 1)",
3026 " now._cnt[now._a_t&1] = 2;",
3027 "#endif",
3028 " now._cnt[now._a_t&1] += 1;",
3029 "#ifdef VERBOSE",
3030 " printf(\"%%3d: proc %%d fairness \", depth, II);",
3031 " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
3032 " now._cnt[now._a_t&1], now._a_t);",
3033 "#endif",
3034 " trpt->o_pm &= ~(32|64);",
3035 " } else", /* process blocked */
3036 " { if (_n > 0)", /* a prev proc didn't */
3037 " {", /* start over */
3038 " trpt->o_pm &= ~64;",
3039 "#ifdef REVERSE",
3040 " II = From-1;", /* after loop incr II == From */
3041 "#else",
3042 " II = From+1;", /* after loop decr II == From */
3043 "#endif",
3044 " } } }",
3045 "#endif",
3046
3047 "#ifdef VERI",
3048 " if (II == 0) break; /* never claim */",
3049 "#endif",
3050 " } /* all processes */",
3051
3052 "#ifdef NSUCC",
3053 " tally_succ(trpt->n_succ);",
3054 "#endif",
3055
3056 "#ifdef SCHED",
3057 " if (_n == 0 /* no process could move */",
3058 " #ifdef VERI",
3059 " && II != 0",
3060 " #endif",
3061 " && depth > 0",
3062 " && trpt->sched_limit >= sched_max)",
3063 " { _n = 1; /* not a deadlock */",
3064 " }",
3065 "#endif",
3066
3067 "#ifndef NOFAIR",
3068 " /* Fairness: undo Rule 2 */",
3069 " if (trpt->o_pm&32) /* remains if proc blocked */",
3070 " {",
3071 "#ifdef VERI",
3072 " if (now._cnt[now._a_t&1] == 1)",
3073 " now._cnt[now._a_t&1] = 2;",
3074 "#endif",
3075 " now._cnt[now._a_t&1] += 1;",
3076 "#ifdef VERBOSE",
3077 " printf(\"%%3d: proc -- fairness \", depth);",
3078 " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
3079 " now._cnt[now._a_t&1], now._a_t);",
3080 "#endif",
3081 " trpt->o_pm &= ~32;",
3082 " }",
3083 "#ifndef NP",
3084 /* 12/97 non-progress cycles cannot be created
3085 * by stuttering extension, here or elsewhere
3086 */
3087 " if (fairness",
3088 " && _n == 0 /* nobody moved */",
3089 "#ifdef VERI",
3090 " && !(trpt->tau&4) /* in program move */",
3091 "#endif",
3092 " && !(trpt->tau&8) /* not an atomic one */",
3093 "#ifdef OTIM",
3094 " && ((trpt->tau&1) || endstate())",
3095 "#else",
3096 "#ifdef ETIM",
3097 " && (trpt->tau&1) /* already tried timeout */",
3098 "#endif",
3099 "#endif",
3100 "#ifndef NOREDUCE",
3101 " /* see below */",
3102 " && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3103 "#endif",
3104 " && now._cnt[now._a_t&1] > 0) /* needed more procs */",
3105 " { depth++; trpt++;",
3106 " trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
3107 " trpt->bup.oval = now._cnt[now._a_t&1];",
3108 " now._cnt[now._a_t&1] = 1;",
3109 "#ifdef VERI",
3110 " trpt->tau = 4;",
3111 "#else",
3112 " trpt->tau = 0;",
3113 "#endif",
3114 "#ifdef REVERSE",
3115 " From = BASE; To = now._nr_pr-1;",
3116 "#else",
3117 " From = now._nr_pr-1; To = BASE;",
3118 "#endif",
3119 "#if defined(VERBOSE) || defined(CHECK)",
3120 " printf(\"%%3d: fairness default move \", depth);",
3121 " printf(\"(all procs block)\\n\");",
3122 "#endif",
3123 " goto Down;",
3124 " }",
3125 "#endif",
3126 "Q999: /* returns here with _n>0 when done */;",
3127
3128 " if (trpt->o_pm&8)",
3129 " { now._a_t &= ~2;",
3130 " now._cnt[now._a_t&1] = 0;",
3131 " trpt->o_pm &= ~8;",
3132 "#ifdef VERBOSE",
3133 " printf(\"%%3d: fairness undo Rule 1, _a_t=%%d\\n\",",
3134 " depth, now._a_t);",
3135 "#endif",
3136 " }",
3137 " if (trpt->o_pm&16)",
3138 " { now._a_t |= 2;", /* restore a-bit */
3139 " now._cnt[now._a_t&1] = 1;", /* NEW: restore cnt */
3140 " trpt->o_pm &= ~16;",
3141 "#ifdef VERBOSE",
3142 " printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
3143 " depth, now._a_t);",
3144 "#endif",
3145 " }",
3146 "#endif",
3147
3148 "#ifndef NOREDUCE",
3149 "#ifdef SAFETY",
3150 "#ifdef LOOPSTATE",
3151 " /* at least one move that was preselected at this */",
3152 " /* level, blocked or was a loop control flow point */",
3153 " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3154 "#else",
3155 " /* preselected move - no successors outside stack */",
3156 " if ((trpt->tau&32) && !(trpt->tau&64))",
3157 "#endif",
3158 "#ifdef REVERSE",
3159 " { From = BASE; To = now._nr_pr-1;",
3160 "#else",
3161 " { From = now._nr_pr-1; To = BASE;",
3162 "#endif",
3163 "#ifdef DEBUG",
3164 " printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3165 " depth, II+1, _n, trpt->tau);",
3166 "#endif",
3167 " _n = 0; trpt->tau &= ~(16|32|64);",
3168 "#ifdef REVERSE",
3169 " if (II <= To) /* II already decremented */",
3170 "#else",
3171 " if (II >= BASE) /* II already decremented */",
3172 "#endif",
3173 " goto Resume;",
3174 " else",
3175 " goto Again;",
3176 " }",
3177 "#else",
3178 " /* at least one move that was preselected at this */",
3179 " /* level, blocked or truncated at the next level */",
3180 "/* implied: #ifdef FULLSTACK */",
3181 " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3182 " {",
3183 "#ifdef DEBUG",
3184 " printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3185 " depth, II+1, (int) _n, trpt->tau);",
3186 "#endif",
3187 " if (a_cycles && (trpt->tau&16))",
3188 " { if (!(now._a_t&1))",
3189 " {",
3190 "#ifdef DEBUG",
3191 " printf(\"%%3d: setting proviso bit\\n\", depth);",
3192 "#endif",
3193 "#ifndef BITSTATE",
3194 "#ifdef MA",
3195 "#ifdef VERI",
3196 " (trpt-1)->proviso = 1;",
3197 "#else",
3198 " trpt->proviso = 1;",
3199 "#endif",
3200 "#else",
3201 "#ifdef VERI",
3202 " if ((trpt-1)->ostate)",
3203 " ((char *)&((trpt-1)->ostate->state))[0] |= 128;",
3204 "#else",
3205 " ((char *)&(trpt->ostate->state))[0] |= 128;",
3206 "#endif",
3207 "#endif",
3208 "#else",
3209 "#ifdef VERI",
3210 " if ((trpt-1)->ostate)",
3211 " (trpt-1)->ostate->proviso = 1;",
3212 "#else",
3213 " trpt->ostate->proviso = 1;",
3214 "#endif",
3215 "#endif",
3216 "#ifdef REVERSE",
3217 " From = BASE; To = now._nr_pr-1;",
3218 "#else",
3219 " From = now._nr_pr-1; To = BASE;",
3220 "#endif",
3221 " _n = 0; trpt->tau &= ~(16|32|64);",
3222 " goto Again; /* do full search */",
3223 " } /* else accept reduction */",
3224 " } else",
3225 "#ifdef REVERSE",
3226 " { From = BASE; To = now._nr_pr-1;",
3227 "#else",
3228 " { From = now._nr_pr-1; To = BASE;",
3229 "#endif",
3230 " _n = 0; trpt->tau &= ~(16|32|64);",
3231 "#ifdef REVERSE",
3232 " if (II <= To) /* already decremented */",
3233 "#else",
3234 " if (II >= BASE) /* already decremented */",
3235 "#endif",
3236 " goto Resume;",
3237 " else",
3238 " goto Again;",
3239 " } }",
3240 "/* #endif */",
3241 "#endif",
3242 "#endif",
3243
3244 " if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
3245 " {",
3246 "#ifdef DEBUG",
3247 " cpu_printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
3248 " depth, II, trpt->tau, boq);",
3249 "#endif",
3250 "#if SYNC",
3251 " /* ok if a rendez-vous fails: */",
3252 " if (boq != -1) goto Done;",
3253 "#endif",
3254 " /* ok if no procs or we're at maxdepth */",
3255 " if ((now._nr_pr == 0 && (!strict || qs_empty()))",
3256 "#ifdef OTIM",
3257 " || endstate()",
3258 "#endif",
3259 " || depth >= maxdepth-1) goto Done;",
3260
3261 " if ((trpt->tau&8) && !(trpt->tau&4))",
3262 " { trpt->tau &= ~(1|8);",
3263 " /* 1=timeout, 8=atomic */",
3264 "#ifdef REVERSE",
3265 " From = BASE; To = now._nr_pr-1;",
3266 "#else",
3267 " From = now._nr_pr-1; To = BASE;",
3268 "#endif",
3269 "#ifdef DEBUG",
3270 " cpu_printf(\"%%3d: atomic step proc %%d unexecutable\\n\", depth, II+1);",
3271 "#endif",
3272 "#ifdef VERI",
3273 " trpt->tau |= 4; /* switch to claim */",
3274 "#endif",
3275 " goto AllOver;",
3276 " }",
3277
3278 "#ifdef ETIM",
3279 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
3280 " {",
3281 "#ifdef VERI",
3282 " if (trpt->tau&4)",
3283 " {",
3284 "#ifndef NTIM",
3285 " if (trpt->tau&2) /* requested */",
3286 "#endif",
3287 " { trpt->tau |= 1;",
3288 " trpt->tau &= ~2;",
3289 "#ifdef DEBUG",
3290 " cpu_printf(\"%%d: timeout\\n\", depth);",
3291 "#endif",
3292 " goto Stutter;",
3293 " } }",
3294 " else",
3295 " { /* only claim can enable timeout */",
3296 " if ((trpt->tau&8)",
3297 " && !((trpt-1)->tau&4))",
3298 "/* blocks inside an atomic */ goto BreakOut;",
3299 "#ifdef DEBUG",
3300 " cpu_printf(\"%%d: req timeout\\n\",",
3301 " depth);",
3302 "#endif",
3303 " (trpt-1)->tau |= 2; /* request */",
3304 "#if NCORE>1 && defined(FULL_TRAIL)",
3305 " if (upto > 0)",
3306 " { Pop_Stack_Tree();",
3307 " }",
3308 "#endif",
3309 " goto Up;",
3310 " }",
3311 "#else",
3312
3313 "#ifdef DEBUG",
3314 " cpu_printf(\"%%d: timeout\\n\", depth);",
3315 "#endif",
3316 " trpt->tau |= 1;",
3317 " goto Again;",
3318 "#endif",
3319 " }",
3320 "#endif",
3321
3322 /* old location of atomic block code */
3323 "#ifdef VERI",
3324 "BreakOut:",
3325 "#ifndef NOSTUTTER",
3326 " if (!(trpt->tau&4))",
3327 " { trpt->tau |= 4; /* claim stuttering */",
3328 " trpt->tau |= 128; /* stutter mark */",
3329 "#ifdef DEBUG",
3330 " cpu_printf(\"%%d: claim stutter\\n\", depth);",
3331 "#endif",
3332 " goto Stutter;",
3333 " }",
3334 "#else",
3335 " ;",
3336 "#endif",
3337 "#else",
3338 " if (!noends && !a_cycles && !endstate())",
3339 " { depth--; trpt--; /* new 4.2.3 */",
3340 " uerror(\"invalid end state\");",
3341 " depth++; trpt++;",
3342 " }",
3343 "#ifndef NOSTUTTER",
3344 " else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */",
3345 " { depth--; trpt--;",
3346 " uerror(\"accept stutter\");",
3347 " depth++; trpt++;",
3348 " }",
3349 "#endif",
3350 "#endif",
3351 " }",
3352 "Done:",
3353 " if (!(trpt->tau&8)) /* not in atomic seqs */",
3354 " {",
3355 "#ifndef SAFETY",
3356 " if (_n != 0", /* we made a move */
3357 "#ifdef VERI",
3358 " /* --after-- a program-step, i.e., */",
3359 " /* after backtracking a claim-step */",
3360 " && (trpt->tau&4)",
3361 " /* with at least one running process */",
3362 " /* unless in a stuttered accept state */",
3363 " && ((now._nr_pr > 1) || (trpt->o_pm&2))",
3364 "#endif",
3365 " && !(now._a_t&1))", /* not in 2nd DFS */
3366 " {",
3367 "#ifndef NOFAIR",
3368 " if (fairness)", /* implies a_cycles */
3369 " {",
3370 "#ifdef VERBOSE",
3371 " cpu_printf(\"Consider check %%d %%d...\\n\",",
3372 " now._a_t, now._cnt[0]);",
3373 "#endif",
3374 #if 0
3375 the a-bit is set, which means that the fairness
3376 counter is running -- it was started in an accepting state.
3377 we check that the counter reached 1, which means that all
3378 processes moved least once.
3379 this means we can start the search for cycles -
3380 to be able to return to this state, we should be able to
3381 run down the counter to 1 again -- which implies a visit to
3382 the accepting state -- even though the Seed state for this
3383 search is itself not necessarily accepting
3384 #endif
3385 " if ((now._a_t&2) /* A-bit */",
3386 " && (now._cnt[0] == 1))",
3387 " checkcycles();",
3388 " } else",
3389 "#endif",
3390 " if (a_cycles && (trpt->o_pm&2))",
3391 " checkcycles();",
3392 " }",
3393 "#endif",
3394 "#ifndef MA",
3395 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
3396 "#ifdef VERI",
3397 " if (boq == -1",
3398 " && (((trpt->tau&4) && !(trpt->tau&128))",
3399 " || ( (trpt-1)->tau&128)))",
3400 "#else",
3401 " if (boq == -1)",
3402 "#endif",
3403 " {",
3404 "#ifdef DEBUG2",
3405 "#if defined(FULLSTACK)",
3406 " printf(\"%%d: zapping %%u (%%d)\\n\",",
3407 " depth, trpt->ostate,",
3408 " (trpt->ostate)?trpt->ostate->tagged:0);",
3409 "#endif",
3410 "#endif",
3411 " onstack_zap();",
3412 " }",
3413 "#endif",
3414 "#else",
3415 "#ifdef VERI",
3416 " if (boq == -1",
3417 " && (((trpt->tau&4) && !(trpt->tau&128))",
3418 " || ( (trpt-1)->tau&128)))",
3419 "#else",
3420 " if (boq == -1)",
3421 "#endif",
3422 " {",
3423 "#ifdef DEBUG",
3424 " printf(\"%%d: zapping\\n\", depth);",
3425 "#endif",
3426 " onstack_zap();",
3427 "#ifndef NOREDUCE",
3428 " if (trpt->proviso)",
3429 " gstore((char *) &now, vsize, 1);",
3430 "#endif",
3431 " }",
3432 "#endif",
3433 " }",
3434 " if (depth > 0)",
3435 " {",
3436 "#if NCORE>1 && defined(FULL_TRAIL)",
3437 " if (upto > 0)",
3438 " { Pop_Stack_Tree();",
3439 " }",
3440 "#endif",
3441 " goto Up;",
3442 " }",
3443 "}\n",
3444 "#else",
3445 "void new_state(void) { /* place holder */ }",
3446 "#endif", /* BFS */
3447 "",
3448 "void",
3449 "assert(int a, char *s, int ii, int tt, Trans *t)",
3450 "{",
3451 " if (!a && !noasserts)",
3452 " { char bad[1024];",
3453 " strcpy(bad, \"assertion violated \");",
3454 " if (strlen(s) > 1000)",
3455 " { strncpy(&bad[19], (const char *) s, 1000);",
3456 " bad[1019] = '\\0';",
3457 " } else",
3458 " strcpy(&bad[19], s);",
3459 " uerror(bad);",
3460 " }",
3461 "}",
3462 "#ifndef NOBOUNDCHECK",
3463 "int",
3464 "Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
3465 "{",
3466 " assert((x >= 0 && x < y), \"- invalid array index\",",
3467 " a1, a2, a3);",
3468 " return x;",
3469 "}",
3470 "#endif",
3471 "void",
3472 "wrap_stats(void)",
3473 "{",
3474 " if (nShadow>0)",
3475 " printf(\"%%9.8g states, stored (%%g visited)\\n\",",
3476 " nstates - nShadow, nstates);",
3477 " else",
3478 " printf(\"%%9.8g states, stored\\n\", nstates);",
3479 "#ifdef BFS",
3480 "#if SYNC",
3481 " printf(\" %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
3482 " printf(\" %%8g rvs succeeded\\n\", midrv-failedrv);",
3483 "#else",
3484 " printf(\" %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
3485 "#endif",
3486 "#ifdef DEBUG",
3487 " printf(\" %%8g midrv\\n\", midrv);",
3488 " printf(\" %%8g failedrv\\n\", failedrv);",
3489 " printf(\" %%8g revrv\\n\", revrv);",
3490 "#endif",
3491 "#endif",
3492 " printf(\"%%9.8g states, matched\\n\", truncs);",
3493 "#ifdef CHECK",
3494 " printf(\"%%9.8g matches within stack\\n\",truncs2);",
3495 "#endif",
3496 " if (nShadow>0)",
3497 " printf(\"%%9.8g transitions (= visited+matched)\\n\",",
3498 " nstates+truncs);",
3499 " else",
3500 " printf(\"%%9.8g transitions (= stored+matched)\\n\",",
3501 " nstates+truncs);",
3502 " printf(\"%%9.8g atomic steps\\n\", nlinks);",
3503 " if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);",
3504 "",
3505 "#ifndef BITSTATE",
3506 " printf(\"hash conflicts: %%9.8g (resolved)\\n\", hcmp);",
3507 " #ifndef AUTO_RESIZE",
3508 " if (hcmp > (double) (1<<ssize))",
3509 " { printf(\"hint: increase hashtable-size (-w) to reduce runtime\\n\");",
3510 " } /* in multi-core: also reduces lock delays on access to hashtable */",
3511 " #endif",
3512 "#else",
3513 "#ifdef CHECK",
3514 " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
3515 "#endif",
3516 " if (udmem)",
3517 " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
3518 " (double)(((double) udmem) * 8.0) / (double) nstates);",
3519 " else",
3520 " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
3521 " (double)(1<<(ssize-8)) / (double) nstates * 256.0);",
3522 " printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);",
3523 " #if 0",
3524 #ifndef POWOW
3525 " if (udmem)",
3526 " { printf(\"total bits available: %%8g (-M%%ld)\\n\",",
3527 " ((double) udmem) * 8.0, udmem/(1024L*1024L));",
3528 " } else",
3529 #endif
3530 " printf(\"total bits available: %%8g (-w%%d)\\n\",",
3531 " ((double) (ONE_L << (ssize-4)) * 16.0), ssize);",
3532 " #endif",
3533 "#endif",
3534 "#ifdef BFS_DISK",
3535 " printf(\"bfs disk reads: %%ld writes %%ld -- diff %%ld\\n\",",
3536 " bfs_dsk_reads, bfs_dsk_writes, bfs_dsk_writes-bfs_dsk_reads);",
3537 " if (bfs_dsk_read >= 0) (void) close(bfs_dsk_read);",
3538 " if (bfs_dsk_write >= 0) (void) close(bfs_dsk_write);",
3539 " (void) unlink(\"pan_bfs_dsk.tmp\");",
3540 "#endif",
3541 "}",
3542 "",
3543 "void",
3544 "wrapup(void)",
3545 "{",
3546 "#if defined(BITSTATE) || !defined(NOCOMP)",
3547 " double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;",
3548 " #if !defined(MA) && (defined(MEMCNT) || defined(MEMLIM))",
3549 " int mverbose = 1;",
3550 " #else",
3551 " int mverbose = verbose;",
3552 " #endif",
3553 "#endif",
3554 "#if NCORE>1",
3555 " if (verbose) cpu_printf(\"wrapup -- %%d error(s)\\n\", errors);",
3556 " if (core_id != 0)",
3557 " {",
3558 "#ifdef USE_DISK",
3559 " void dsk_stats(void);",
3560 " dsk_stats();",
3561 "#endif",
3562 " if (search_terminated != NULL)",
3563 " { *search_terminated |= 2; /* wrapup */",
3564 " }",
3565 " exit(0); /* normal termination, not an error */",
3566 " }",
3567 "#endif",
3568 "#if !defined(WIN32) && !defined(WIN64)",
3569 " signal(SIGINT, SIG_DFL);",
3570 "#endif",
3571 " printf(\"\\n(%%s)\\n\", SpinVersion);",
3572 " if (!done) printf(\"Warning: Search not completed\\n\");",
3573 "#ifdef SC",
3574 " (void) unlink((const char *)stackfile);",
3575 "#endif",
3576 "#if NCORE>1",
3577 " if (a_cycles)",
3578 " { printf(\" + Multi-Core (NCORE=%%d)\\n\", NCORE);",
3579 " } else",
3580 " { printf(\" + Multi-Core (NCORE=%%d -z%%d)\\n\", NCORE, z_handoff);",
3581 " }",
3582 "#endif",
3583 "#ifdef BFS",
3584 " printf(\" + Using Breadth-First Search\\n\");",
3585 "#endif",
3586 "#ifndef NOREDUCE",
3587 " printf(\" + Partial Order Reduction\\n\");",
3588 "#endif",
3589 "#ifdef REVERSE",
3590 " printf(\" + Reverse Depth-First Search Order\\n\");",
3591 "#endif",
3592 "#ifdef T_REVERSE",
3593 " printf(\" + Reverse Transition Ordering\\n\");",
3594 "#endif",
3595 "#ifdef RANDOMIZE",
3596 " printf(\" + Randomized Transition Ordering\\n\");",
3597 "#endif",
3598 "#ifdef SCHED",
3599 " printf(\" + Scheduling Restriction (-DSCHED=%%d)\\n\", sched_max);",
3600 "#endif",
3601 #if 0
3602 "#ifdef Q_PROVISO",
3603 " printf(\" + Queue Proviso\\n\");",
3604 "#endif",
3605 #endif
3606 "#ifdef COLLAPSE",
3607 " printf(\" + Compression\\n\");",
3608 "#endif",
3609 "#ifdef MA",
3610 " printf(\" + Graph Encoding (-DMA=%%d)\\n\", MA);",
3611 " #ifdef R_XPT",
3612 " printf(\" Restarted from checkpoint %%s.xpt\\n\", PanSource);",
3613 " #endif",
3614 "#endif",
3615 "#ifdef CHECK",
3616 " #ifdef FULLSTACK",
3617 " printf(\" + FullStack Matching\\n\");",
3618 " #endif",
3619 " #ifdef CNTRSTACK",
3620 " printf(\" + CntrStack Matching\\n\");",
3621 " #endif",
3622 "#endif",
3623 "#ifdef BITSTATE",
3624 " printf(\"\\nBit statespace search for:\\n\");",
3625 "#else",
3626 "#ifdef HC",
3627 " printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
3628 "#else",
3629 " printf(\"\\nFull statespace search for:\\n\");",
3630 "#endif",
3631 "#endif",
3632 "#ifdef EVENT_TRACE",
3633 "#ifdef NEGATED_TRACE",
3634 " printf(\"\tnotrace assertion \t+\\n\");",
3635 "#else",
3636 " printf(\"\ttrace assertion \t+\\n\");",
3637 "#endif",
3638 "#endif",
3639 "#ifdef VERI",
3640 " printf(\"\tnever claim \t+\\n\");",
3641 " printf(\"\tassertion violations\t\");",
3642 " if (noasserts)",
3643 " printf(\"- (disabled by -A flag)\\n\");",
3644 " else",
3645 " printf(\"+ (if within scope of claim)\\n\");",
3646 "#else",
3647 "#ifdef NOCLAIM",
3648 " printf(\"\tnever claim \t- (not selected)\\n\");",
3649 "#else",
3650 " printf(\"\tnever claim \t- (none specified)\\n\");",
3651 "#endif",
3652 " printf(\"\tassertion violations\t\");",
3653 " if (noasserts)",
3654 " printf(\"- (disabled by -A flag)\\n\");",
3655 " else",
3656 " printf(\"+\\n\");",
3657 "#endif",
3658 "#ifndef SAFETY",
3659 "#ifdef NP",
3660 " printf(\"\tnon-progress cycles \t\");",
3661 "#else",
3662 " printf(\"\tacceptance cycles \t\");",
3663 "#endif",
3664 " if (a_cycles)",
3665 " printf(\"+ (fairness %%sabled)\\n\",",
3666 " fairness?\"en\":\"dis\");",
3667 " else printf(\"- (not selected)\\n\");",
3668 "#else",
3669 " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");",
3670 "#endif",
3671 "#ifdef VERI",
3672 " printf(\"\tinvalid end states\t- \");",
3673 " printf(\"(disabled by \");",
3674 " if (noends)",
3675 " printf(\"-E flag)\\n\\n\");",
3676 " else",
3677 " printf(\"never claim)\\n\\n\");",
3678 "#else",
3679 " printf(\"\tinvalid end states\t\");",
3680 " if (noends)",
3681 " printf(\"- (disabled by -E flag)\\n\\n\");",
3682 " else",
3683 " printf(\"+\\n\\n\");",
3684 "#endif",
3685 " printf(\"State-vector %%d byte, depth reached %%ld\", hmax,",
3686 "#if NCORE>1",
3687 " (nr_handoffs * z_handoff) +",
3688 "#endif",
3689 " mreached);",
3690 " printf(\", errors: %%d\\n\", errors);",
3691 " fflush(stdout);",
3692 "#ifdef MA",
3693 " if (done)",
3694 " { extern void dfa_stats(void);",
3695 " if (maxgs+a_cycles+2 < MA)",
3696 " printf(\"MA stats: -DMA=%%d is sufficient\\n\",",
3697 " maxgs+a_cycles+2);",
3698 " dfa_stats();",
3699 " }",
3700 "#endif",
3701 " wrap_stats();",
3702 "#ifdef CHECK",
3703 " printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);",
3704 " printf(\"stats: fa %%d, fh %%d, zh %%d, zn %%d - \",",
3705 " Fa, Fh, Zh, Zn);",
3706 " printf(\"check %%d holds %%d\\n\", Ccheck, Cholds);",
3707 " printf(\"stack stats: puts %%d, probes %%d, zaps %%d\\n\",",
3708 " PUT, PROBE, ZAPS);",
3709 "#else",
3710 " printf(\"\\n\");",
3711 "#endif",
3712 "",
3713 "#if defined(BITSTATE) || !defined(NOCOMP)",
3714 " nr1 = (nstates-nShadow)*",
3715 " (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
3716 "#ifdef BFS",
3717 " nr2 = 0.0;",
3718 "#else",
3719 " nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
3720 "#endif",
3721
3722 "#ifndef BITSTATE",
3723 "#if !defined(MA) || defined(COLLAPSE)",
3724 " nr3 = (double) (ONE_L<<ssize)*sizeof(struct H_el *);",
3725 "#endif",
3726 "#else",
3727 #ifndef POWOW
3728 " if (udmem)",
3729 " nr3 = (double) (udmem);",
3730 " else",
3731 #endif
3732 " nr3 = (double) (ONE_L<<(ssize-3));",
3733 "#ifdef CNTRSTACK",
3734 " nr5 = (double) (ONE_L<<(ssize-3));",
3735 "#endif",
3736 "#ifdef FULLSTACK",
3737 " nr5 = (double) (maxdepth*sizeof(struct H_el *));",
3738 "#endif",
3739 "#endif",
3740 " nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
3741 " + (double) (smax * (sizeof(Stack) + Maxbody));",
3742 "#ifndef MA",
3743 " if (mverbose || memcnt < nr1+nr2+nr3+nr4+nr5)",
3744 "#endif",
3745 " { double remainder = memcnt;",
3746 " double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;",
3747 "#if NCORE>1 && !defined(SEP_STATE)",
3748 " tmp_nr -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
3749 "#endif",
3750 " if (tmp_nr < 0.0) tmp_nr = 0.;",
3751 " printf(\"Stats on memory usage (in Megabytes):\\n\");",
3752 " printf(\"%%9.3f\tequivalent memory usage for states\",",
3753 " nr1/1048576.); /* 1024*1024=1048576 */",
3754 " printf(\" (stored*(State-vector + overhead))\\n\");",
3755 " #if NCORE>1 && !defined(WIN32) && !defined(WIN64)",
3756 " printf(\"%%9.3f\tshared memory reserved for state storage\\n\",",
3757 " mem_reserved/1048576.);",
3758 " #ifdef SEP_HEAP",
3759 " printf(\"\t\tin %%d local heaps of %%7.3f MB each\\n\",",
3760 " NCORE, mem_reserved/(NCORE*1048576.));",
3761 " #endif",
3762 " printf(\"\\n\");",
3763 " #endif",
3764 "#ifdef BITSTATE",
3765 #ifndef POWOW
3766 " if (udmem)",
3767 " printf(\"%%9.3f\tmemory used for hash array (-M%%ld)\\n\",",
3768 " nr3/1048576., udmem/(1024L*1024L));",
3769 " else",
3770 #endif
3771 " printf(\"%%9.3f\tmemory used for hash array (-w%%d)\\n\",",
3772 " nr3/1048576., ssize);",
3773 " if (nr5 > 0.0)",
3774 " printf(\"%%9.3f\tmemory used for bit stack\\n\",",
3775 " nr5/1048576.);",
3776 " remainder = remainder - nr3 - nr5;",
3777 "#else",
3778 " printf(\"%%9.3f\tactual memory usage for states\",",
3779 " tmp_nr/1048576.);",
3780 " remainder -= tmp_nr;",
3781 " printf(\" (\");",
3782 " if (tmp_nr > 0.)",
3783 " { if (tmp_nr > nr1) printf(\"unsuccessful \");",
3784 " printf(\"compression: %%.2f%%%%)\\n\",",
3785 " (100.0*tmp_nr)/nr1);",
3786 " } else",
3787 " printf(\"less than 1k)\\n\");",
3788 "#ifndef MA",
3789 " if (tmp_nr > 0.)",
3790 " { printf(\" \tstate-vector as stored = %%.0f byte\",",
3791 " (tmp_nr)/(nstates-nShadow) -",
3792 " (double) (sizeof(struct H_el) - sizeof(unsigned)));",
3793 " printf(\" + %%ld byte overhead\\n\",",
3794 " (long int) sizeof(struct H_el)-sizeof(unsigned));",
3795 " }",
3796 "#endif",
3797 "#if !defined(MA) || defined(COLLAPSE)",
3798 " printf(\"%%9.3f\tmemory used for hash table (-w%%d)\\n\",",
3799 " nr3/1048576., ssize);",
3800 " remainder -= nr3;",
3801 "#endif",
3802 "#endif",
3803 "#ifndef BFS",
3804 " printf(\"%%9.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
3805 " nr2/1048576., maxdepth);",
3806 " remainder -= nr2;",
3807 "#endif",
3808 "#if NCORE>1",
3809 " remainder -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
3810 " printf(\"%%9.3f\tshared memory used for work-queues\\n\",",
3811 " (GWQ_SIZE + (double) NCORE * LWQ_SIZE) /1048576.);",
3812 " printf(\"\t\tin %%d queues of %%7.3f MB each\",",
3813 " NCORE, (double) LWQ_SIZE /1048576.);",
3814 " #ifndef NGQ",
3815 " printf(\" + a global q of %%7.3f MB\\n\",",
3816 " (double) GWQ_SIZE / 1048576.);",
3817 " #else",
3818 " printf(\"\\n\");",
3819 " #endif",
3820 " #endif",
3821 " if (remainder - fragment > 1048576.)",
3822 " printf(\"%%9.3f\tother (proc and chan stacks)\\n\",",
3823 " (remainder-fragment)/1048576.);",
3824 " if (fragment > 1048576.)",
3825 " printf(\"%%9.3f\tmemory lost to fragmentation\\n\",",
3826 " fragment/1048576.);",
3827 " printf(\"%%9.3f\ttotal actual memory usage\\n\\n\",",
3828 " memcnt/1048576.);",
3829 " }",
3830 "#ifndef MA",
3831 " else",
3832 "#endif",
3833 "#endif",
3834 "#ifndef MA",
3835 " printf(\"%%9.3f\tmemory usage (Mbyte)\\n\\n\",",
3836 " memcnt/1048576.);",
3837 "#endif",
3838 "#ifdef COLLAPSE",
3839 " printf(\"nr of templates: [ globals chans procs ]\\n\");",
3840 " printf(\"collapse counts: [ \");",
3841 " { int i; for (i = 0; i < 256+2; i++)",
3842 " if (ncomps[i] != 0)",
3843 " printf(\"%%d \", ncomps[i]);",
3844 " printf(\"]\\n\");",
3845 " }",
3846 "#endif",
3847
3848 " if ((done || verbose) && !no_rck) do_reach();",
3849 "#ifdef PEG",
3850 " { int i;",
3851 " printf(\"\\nPeg Counts (transitions executed):\\n\");",
3852 " for (i = 1; i < NTRANS; i++)",
3853 " { if (peg[i]) putpeg(i, peg[i]);",
3854 " } }",
3855 "#endif",
3856 "#ifdef VAR_RANGES",
3857 " dumpranges();",
3858 "#endif",
3859 "#ifdef SVDUMP",
3860 " if (vprefix > 0) close(svfd);",
3861 "#endif",
3862 "#ifdef LOOPSTATE",
3863 " printf(\"%%g loopstates hit\\n\", cnt_loops);",
3864 "#endif",
3865 "#ifdef NSUCC",
3866 " dump_succ();",
3867 "#endif",
3868 "#if NCORE>1 && defined(T_ALERT)",
3869 " crash_report();",
3870 "#endif",
3871 " pan_exit(0);",
3872 "}\n",
3873 "void",
3874 "stopped(int arg)",
3875 "{ printf(\"Interrupted\\n\");",
3876 "#if NCORE>1",
3877 " was_interrupted = 1;",
3878 "#endif",
3879 " wrapup();",
3880 " pan_exit(0);",
3881 "}",
3882 "",
3883 "#ifdef SFH",
3884 "/*",
3885 " * super fast hash, based on Paul Hsieh's function",
3886 " * http://www.azillionmonkeys.com/qed/hash.html",
3887 " */",
3888 "#include <stdint.h>", /* for uint32_t etc */
3889 " #undef get16bits",
3890 " #if (defined(__GNUC__) && defined(__i386__)) || defined(__WATCOMC__) \\",
3891 " || defined(_MSC_VER) || defined (__BORLANDC__) || defined (__TURBOC__)",
3892 " #define get16bits(d) (*((const uint16_t *) (d)))",
3893 " #endif",
3894 "",
3895 " #ifndef get16bits",
3896 " #define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\",
3897 " +(uint32_t)(((const uint8_t *)(d))[0]) )",
3898 " #endif",
3899 "",
3900 "void",
3901 "d_sfh(const char *s, int len)",
3902 "{ uint32_t h = len, tmp;",
3903 " int rem;",
3904 "",
3905 " rem = len & 3;",
3906 " len >>= 2;",
3907 "",
3908 " for ( ; len > 0; len--)",
3909 " { h += get16bits(s);",
3910 " tmp = (get16bits(s+2) << 11) ^ h;",
3911 " h = (h << 16) ^ tmp;",
3912 " s += 2*sizeof(uint16_t);",
3913 " h += h >> 11;",
3914 " }",
3915 " switch (rem) {",
3916 " case 3: h += get16bits(s);",
3917 " h ^= h << 16;",
3918 " h ^= s[sizeof(uint16_t)] << 18;",
3919 " h += h >> 11;",
3920 " break;",
3921 " case 2: h += get16bits(s);",
3922 " h ^= h << 11;",
3923 " h += h >> 17;",
3924 " break;",
3925 " case 1: h += *s;",
3926 " h ^= h << 10;",
3927 " h += h >> 1;",
3928 " break;",
3929 " }",
3930 " h ^= h << 3;",
3931 " h += h >> 5;",
3932 " h ^= h << 4;",
3933 " h += h >> 17;",
3934 " h ^= h << 25;",
3935 " h += h >> 6;",
3936 "",
3937 " K1 = h;",
3938 "}",
3939 "#endif", /* SFH */
3940 "",
3941 "#include <stdint.h>", /* uint32_t etc. */
3942 "#if defined(HASH64) || defined(WIN64)",
3943 "/* 64-bit Jenkins hash, 1997",
3944 " * http://burtleburtle.net/bob/c/lookup8.c",
3945 " */",
3946 "#define mix(a,b,c) \\",
3947 "{ a -= b; a -= c; a ^= (c>>43); \\",
3948 " b -= c; b -= a; b ^= (a<<9); \\",
3949 " c -= a; c -= b; c ^= (b>>8); \\",
3950 " a -= b; a -= c; a ^= (c>>38); \\",
3951 " b -= c; b -= a; b ^= (a<<23); \\",
3952 " c -= a; c -= b; c ^= (b>>5); \\",
3953 " a -= b; a -= c; a ^= (c>>35); \\",
3954 " b -= c; b -= a; b ^= (a<<49); \\",
3955 " c -= a; c -= b; c ^= (b>>11); \\",
3956 " a -= b; a -= c; a ^= (c>>12); \\",
3957 " b -= c; b -= a; b ^= (a<<18); \\",
3958 " c -= a; c -= b; c ^= (b>>22); \\",
3959 "}",
3960 "#else",
3961 "/* 32-bit Jenkins hash, 2006",
3962 " * http://burtleburtle.net/bob/c/lookup3.c",
3963 " */",
3964 "#define rot(x,k) (((x)<<(k))|((x)>>(32-(k))))",
3965 "",
3966 "#define mix(a,b,c) \\",
3967 "{ a -= c; a ^= rot(c, 4); c += b; \\",
3968 " b -= a; b ^= rot(a, 6); a += c; \\",
3969 " c -= b; c ^= rot(b, 8); b += a; \\",
3970 " a -= c; a ^= rot(c,16); c += b; \\",
3971 " b -= a; b ^= rot(a,19); a += c; \\",
3972 " c -= b; c ^= rot(b, 4); b += a; \\",
3973 "}",
3974 "",
3975 "#define final(a,b,c) \\",
3976 "{ c ^= b; c -= rot(b,14); \\",
3977 " a ^= c; a -= rot(c,11); \\",
3978 " b ^= a; b -= rot(a,25); \\",
3979 " c ^= b; c -= rot(b,16); \\",
3980 " a ^= c; a -= rot(c,4); \\",
3981 " b ^= a; b -= rot(a,14); \\",
3982 " c ^= b; c -= rot(b,24); \\",
3983 "}",
3984 "#endif",
3985 "",
3986 "void",
3987 "d_hash(uchar *kb, int nbytes)",
3988 "{ uint8_t *bp;",
3989 "#if defined(HASH64) || defined(WIN64)",
3990 " uint64_t a = 0, b, c, n;",
3991 " uint64_t *k = (uint64_t *) kb;",
3992 "#else",
3993 " uint32_t a, b, c, n;",
3994 " uint32_t *k = (uint32_t *) kb;",
3995 "#endif",
3996 " /* extend to multiple of words, if needed */",
3997 " n = nbytes/WS; /* nr of words */",
3998 " a = nbytes - (n*WS);",
3999 " if (a > 0)",
4000 " { n++;",
4001 " bp = kb + nbytes;",
4002 " switch (a) {",
4003 " case 3: *bp++ = 0; /* fall thru */",
4004 " case 2: *bp++ = 0; /* fall thru */",
4005 " case 1: *bp = 0;",
4006 " case 0: break;",
4007 " } }",
4008 "#if defined(HASH64) || defined(WIN64)",
4009 " b = HASH_CONST[HASH_NR];",
4010 " c = 0x9e3779b97f4a7c13LL; /* arbitrary value */",
4011 " while (n >= 3)",
4012 " { a += k[0];",
4013 " b += k[1];",
4014 " c += k[2];",
4015 " mix(a,b,c);",
4016 " n -= 3;",
4017 " k += 3;",
4018 " }",
4019 " c += (((uint64_t) nbytes)<<3);",
4020 " switch (n) {",
4021 " case 2: b += k[1];",
4022 " case 1: a += k[0];",
4023 " case 0: break;",
4024 " }",
4025 " mix(a,b,c);",
4026 "#else", /* 32 bit version: */
4027 " a = c = 0xdeadbeef + (n<<2);",
4028 " b = HASH_CONST[HASH_NR];",
4029 " while (n > 3)",
4030 " { a += k[0];",
4031 " b += k[1];",
4032 " c += k[2];",
4033 " mix(a,b,c);",
4034 " n -= 3;",
4035 " k += 3;",
4036 " }",
4037 " switch (n) { ",
4038 " case 3: c += k[2];",
4039 " case 2: b += k[1];",
4040 " case 1: a += k[0];",
4041 " case 0: break;",
4042 " }",
4043 " final(a,b,c);",
4044 "#endif",
4045 " j1 = c&nmask; j3 = a&7; /* 1st bit */",
4046 " j2 = b&nmask; j4 = (a>>3)&7; /* 2nd bit */",
4047 " K1 = c; K2 = b;",
4048 "}",
4049 "",
4050 "void",
4051 "s_hash(uchar *cp, int om)",
4052 "{",
4053 "#if defined(SFH)",
4054 " d_sfh((const char *) cp, om); /* sets K1 */",
4055 "#else",
4056 " d_hash(cp, om); /* sets K1 etc */",
4057 "#endif",
4058 "#ifdef BITSTATE",
4059 " if (S_Tab == H_tab)", /* state stack in bitstate search */
4060 " j1 = K1 %% omaxdepth;",
4061 " else",
4062 "#endif", /* if (S_Tab != H_Tab) */
4063 " if (ssize < 8*WS)",
4064 " j1 = K1&mask;",
4065 " else",
4066 " j1 = K1;",
4067 "}",
4068 "#ifndef RANDSTOR",
4069 "int *prerand;",
4070 "void",
4071 "inirand(void)",
4072 "{ int i;",
4073 " srand(123); /* fixed startpoint */",
4074 " prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));",
4075 " for (i = 0; i < omaxdepth+3; i++)",
4076 " prerand[i] = rand();",
4077 "}",
4078 "int",
4079 "pan_rand(void)",
4080 "{ if (!prerand) inirand();",
4081 " return prerand[depth];",
4082 "}",
4083 "#endif",
4084 "",
4085 "void",
4086 "set_masks(void) /* 4.2.5 */",
4087 "{",
4088 " if (WS == 4 && ssize >= 32)",
4089 " { mask = 0xffffffff;",
4090 "#ifdef BITSTATE",
4091 " switch (ssize) {",
4092 " case 34: nmask = (mask>>1); break;",
4093 " case 33: nmask = (mask>>2); break;",
4094 " default: nmask = (mask>>3); break;",
4095 " }",
4096 "#else",
4097 " nmask = mask;",
4098 "#endif",
4099 " } else if (WS == 8)",
4100 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
4101 "#ifdef BITSTATE",
4102 " nmask = mask>>3;",
4103 "#else",
4104 " nmask = mask;",
4105 "#endif",
4106 " } else if (WS != 4)",
4107 " { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", (long int) WS);",
4108 " exit(1);",
4109 " } else /* WS == 4 and ssize < 32 */",
4110 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
4111 " nmask = (mask>>3);",
4112 " }",
4113 "}",
4114 "",
4115 "static long reclaim_size;",
4116 "static char *reclaim_mem;",
4117 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
4118 "#if NCORE>1",
4119 " #error cannot combine AUTO_RESIZE with NCORE>1 yet",
4120 "#endif",
4121 "static struct H_el **N_tab;",
4122 "void",
4123 "reverse_capture(struct H_el *p)",
4124 "{ if (!p) return;",
4125 " reverse_capture(p->nxt);",
4126 " /* last element of list moves first */",
4127 " /* to preserve list-order */",
4128 " j2 = p->m_K1;",
4129 " if (ssize < 8*WS) /* probably always true */",
4130 " { j2 &= mask;",
4131 " }",
4132 " p->nxt = N_tab[j2];",
4133 " N_tab[j2] = p;",
4134 "}",
4135 "void",
4136 "resize_hashtable(void)",
4137 "{",
4138 " if (WS == 4 && ssize >= 27 - 1)",
4139 " { return; /* canot increase further */",
4140 " }",
4141 "",
4142 " ssize += 2; /* 4x size */",
4143 "",
4144 " printf(\"pan: resizing hashtable to -w%%d.. \", ssize);",
4145 "",
4146 " N_tab = (struct H_el **)",
4147 " emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
4148 "",
4149 " set_masks(); /* they changed */",
4150 "",
4151 " for (j1 = 0; j1 < (ONE_L << (ssize - 2)); j1++)",
4152 " { reverse_capture(H_tab[j1]);",
4153 " }",
4154 " reclaim_mem = (char *) H_tab;",
4155 " reclaim_size = (ONE_L << (ssize - 2));",
4156 " H_tab = N_tab;",
4157 "",
4158 " printf(\" done\\n\");",
4159 "}",
4160 "#endif",
4161 "#if defined(ZAPH) && defined(BITSTATE)",
4162 "void",
4163 "zap_hashtable(void)",
4164 "{ cpu_printf(\"pan: resetting hashtable\\n\");",
4165 " if (udmem)",
4166 " { memset(SS, 0, udmem);",
4167 " } else",
4168 " { memset(SS, 0, ONE_L<<(ssize-3));",
4169 " }",
4170 "}",
4171 "#endif",
4172 "",
4173 "int",
4174 "main(int argc, char *argv[])",
4175 "{ void to_compile(void);\n",
4176 " efd = stderr; /* default */",
4177 "#ifdef BITSTATE",
4178 " bstore = bstore_reg; /* default */",
4179 "#endif",
4180 "#if NCORE>1",
4181 " { int i, j;",
4182 " strcpy(o_cmdline, \"\");",
4183 " for (j = 1; j < argc; j++)",
4184 " { strcat(o_cmdline, argv[j]);",
4185 " strcat(o_cmdline, \" \");",
4186 " }",
4187 " /* printf(\"Command Line: %%s\\n\", o_cmdline); */",
4188 " if (strlen(o_cmdline) >= sizeof(o_cmdline))",
4189 " { Uerror(\"option list too long\");",
4190 " } }",
4191 "#endif",
4192 " while (argc > 1 && argv[1][0] == '-')",
4193 " { switch (argv[1][1]) {",
4194 "#ifndef SAFETY",
4195 "#ifdef NP",
4196 " case 'a': fprintf(efd, \"error: -a disabled\");",
4197 " usage(efd); break;",
4198 "#else",
4199 " case 'a': a_cycles = 1; break;",
4200 "#endif",
4201 "#endif",
4202 " case 'A': noasserts = 1; break;",
4203 " case 'b': bounded = 1; break;",
4204 "#ifdef HAS_CODE",
4205 " case 'C': coltrace = 1; goto samething;",
4206 "#endif",
4207 " case 'c': upto = atoi(&argv[1][2]); break;",
4208 " case 'd': state_tables++; break;",
4209 " case 'e': every_error = 1; Nr_Trails = 1; break;",
4210 " case 'E': noends = 1; break;",
4211 "#ifdef SC",
4212 " case 'F': if (strlen(argv[1]) > 2)",
4213 " stackfile = &argv[1][2];",
4214 " break;",
4215 "#endif",
4216 "#if !defined(SAFETY) && !defined(NOFAIR)",
4217 " case 'f': fairness = 1; break;",
4218 "#endif",
4219 "#ifdef HAS_CODE",
4220 " case 'g': gui = 1; goto samething;",
4221 "#endif",
4222 " case 'h': if (!argv[1][2]) usage(efd); else",
4223 " HASH_NR = atoi(&argv[1][2])%%33; break;",
4224 " case 'I': iterative = 2; every_error = 1; break;",
4225 " case 'i': iterative = 1; every_error = 1; break;",
4226 " case 'J': like_java = 1; break; /* Klaus Havelund */",
4227 "#ifdef BITSTATE",
4228 " case 'k': hfns = atoi(&argv[1][2]); break;",
4229 "#endif",
4230 "#ifdef SCHED",
4231 " case 'L': sched_max = atoi(&argv[1][2]); break;",
4232 "#endif",
4233 "#ifndef SAFETY",
4234 "#ifdef NP",
4235 " case 'l': a_cycles = 1; break;",
4236 "#else",
4237 " case 'l': fprintf(efd, \"error: -l disabled\");",
4238 " usage(efd); break;",
4239 "#endif",
4240 "#endif",
4241 #ifndef POWOW
4242 "#ifdef BITSTATE",
4243 " case 'M': udmem = atoi(&argv[1][2]); break;",
4244 " case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
4245 "#else",
4246 " case 'M': case 'G':",
4247 " fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
4248 " break;",
4249 "#endif",
4250 #endif
4251 " case 'm': maxdepth = atoi(&argv[1][2]); break;",
4252 " case 'n': no_rck = 1; break;",
4253 " case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]);",
4254 " if (argv[2][0] != '-') /* check next arg */",
4255 " { trailfilename = argv[2];",
4256 " argc--; argv++; /* skip next arg */",
4257 " }",
4258 " break;",
4259 "#ifdef SVDUMP",
4260 " case 'p': vprefix = atoi(&argv[1][2]); break;",
4261 "#endif",
4262 "#if NCORE==1",
4263 " case 'Q': quota = (double) 60.0 * (double) atoi(&argv[1][2]); break;",
4264 "#endif",
4265 " case 'q': strict = 1; break;",
4266 " case 'R': Nrun = atoi(&argv[1][2]); break;",
4267 "#ifdef HAS_CODE",
4268 " case 'r':",
4269 "samething: readtrail = 1;",
4270 " if (isdigit(argv[1][2]))",
4271 " whichtrail = atoi(&argv[1][2]);",
4272 " else if (argc > 2 && argv[2][0] != '-') /* check next arg */",
4273 " { trailfilename = argv[2];",
4274 " argc--; argv++; /* skip next arg */",
4275 " }",
4276 " break;",
4277 " case 'S': silent = 1; goto samething;",
4278 "#endif",
4279 "#ifdef BITSTATE",
4280 " case 's': hfns = 1; break;",
4281 "#endif",
4282 " case 'T': TMODE = 0444; break;",
4283 " case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;",
4284 " case 'V': start_timer(); printf(\"Generated by %%s\\n\", SpinVersion);",
4285 " to_compile(); pan_exit(2); break;",
4286 " case 'v': verbose++; break;",
4287 " case 'w': ssize = atoi(&argv[1][2]); break;",
4288 " case 'Y': signoff = 1; break;",
4289 " case 'X': efd = stdout; break;",
4290 " case 'x': exclusive = 1; break;",
4291 "#if NCORE>1",
4292 " /* -B ip is passthru to proxy of remote ip address: */",
4293 " case 'B': argc--; argv++; break;",
4294 " case 'Q': worker_pids[0] = atoi(&argv[1][2]); break;",
4295 " /* -Un means that the nth worker should be instantiated as a proxy */",
4296 " case 'U': proxy_pid = atoi(&argv[1][2]); break;",
4297 " /* -W means that this copy is started by a cluster-server as a remote */",
4298 " /* this flag is passed to ./pan_proxy, which interprets it */",
4299 " case 'W': remote_party++; break;",
4300 " case 'Z': core_id = atoi(&argv[1][2]);",
4301 " if (verbose)",
4302 " { printf(\"cpu%%d: pid %%d parent %%d\\n\",",
4303 " core_id, getpid(), worker_pids[0]);",
4304 " }",
4305 " break;",
4306 " case 'z': z_handoff = atoi(&argv[1][2]); break;",
4307 "#else",
4308 " case 'z': break; /* ignored for single-core */",
4309 "#endif",
4310 " default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
4311 " }",
4312 " argc--; argv++;",
4313 " }",
4314 " if (iterative && TMODE != 0666)",
4315 " { TMODE = 0666;",
4316 " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
4317 " }",
4318 "#if defined(HASH32) && !defined(SFH)",
4319 " if (WS > 4)",
4320 " { fprintf(efd, \"strong warning: compiling -DHASH32 on a 64-bit machine\\n\");",
4321 " fprintf(efd, \" without -DSFH can slow down performance a lot\\n\");",
4322 " }",
4323 "#endif",
4324 "#if defined(WIN32) || defined(WIN64)",
4325 " if (TMODE == 0666)",
4326 " TMODE = _S_IWRITE | _S_IREAD;",
4327 " else",
4328 " TMODE = _S_IREAD;",
4329 "#endif",
4330 "#if NCORE>1",
4331 " store_proxy_pid = proxy_pid; /* for checks in mem_file() and someone_crashed() */",
4332 " if (core_id != 0) { proxy_pid = 0; }",
4333 " #ifndef SEP_STATE",
4334 " if (core_id == 0 && a_cycles)",
4335 " { fprintf(efd, \"hint: this search may be more efficient \");",
4336 " fprintf(efd, \"if pan.c is compiled -DSEP_STATE\\n\");",
4337 " }",
4338 " #endif",
4339 " if (z_handoff < 0)",
4340 " { z_handoff = 20; /* conservative default - for non-liveness checks */",
4341 " }",
4342 "#if defined(NGQ) || defined(LWQ_FIXED)",
4343 " LWQ_SIZE = (double) (128.*1048576.);",
4344 "#else",
4345 " LWQ_SIZE = (double) ( z_handoff + 2.) * (double) sizeof(SM_frame);",
4346 /* the added margin of +2 is not really necessary */
4347 "#endif",
4348 " #if NCORE>2",
4349 " if (a_cycles)",
4350 " { fprintf(efd, \"warning: the intended nr of cores to be used in liveness mode is 2\\n\");",
4351 " #ifndef SEP_STATE",
4352 " fprintf(efd, \"warning: without -DSEP_STATE there is no guarantee that all liveness violations are found\\n\");",
4353 " #endif",
4354 " }", /* it still works though, the later cores get states from the global q */
4355 " #endif",
4356 " #ifdef HAS_HIDDEN",
4357 " #error cannot use hidden variables when compiling multi-core",
4358 " #endif",
4359 "#endif",
4360 "#ifdef BITSTATE",
4361 " if (hfns <= 0)",
4362 " { hfns = 1;",
4363 " fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
4364 " }",
4365 "#endif",
4366 " omaxdepth = maxdepth;",
4367 "#ifdef BITSTATE",
4368 " if (WS == 4 && ssize > 34)", /* 32-bit word size */
4369 " { ssize = 34;",
4370 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
4371 "/*",
4372 " * -w35 would not work: 35-3 = 32 but 1^31 is the largest",
4373 " * power of 2 that can be represented in an unsigned long",
4374 " */",
4375 " }",
4376 "#else",
4377 " if (WS == 4 && ssize > 27)",
4378 " { ssize = 27;",
4379 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
4380 "/*",
4381 " * for emalloc, the lookup table size multiplies by 4 for the pointers",
4382 " * the largest power of 2 that can be represented in a ulong is 1^31",
4383 " * hence the largest number of lookup table slots is 31-4 = 27",
4384 " */",
4385 " }",
4386
4387 "#endif",
4388 "#ifdef SC",
4389 " hiwater = HHH = maxdepth-10;",
4390 " DDD = HHH/2;",
4391 " if (!stackfile)",
4392 " { stackfile = (char *) emalloc(strlen(PanSource)+4+1);",
4393 " sprintf(stackfile, \"%%s._s_\", PanSource);",
4394 " }",
4395 " if (iterative)",
4396 " { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
4397 " pan_exit(1);",
4398 " }",
4399 "#endif",
4400
4401 "#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
4402 " #warning -DR_XPT and -DW_XPT assume -DMA (ignored)",
4403 "#endif",
4404
4405 " if (iterative && a_cycles)",
4406 " fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",
4407
4408 "#ifdef BFS",
4409 " #ifdef SC",
4410 " #error -DBFS not compatible with -DSC",
4411 " #endif",
4412 " #ifdef HAS_LAST",
4413 " #error -DBFS not compatible with _last",
4414 " #endif",
4415 " #ifdef HAS_STACK",
4416 " #error cannot use c_track UnMatched with BFS",
4417 " #endif",
4418 " #ifdef REACH",
4419 " #warning -DREACH is redundant when -DBFS is used",
4420 " #endif",
4421 "#endif",
4422 "#if defined(MERGED) && defined(PEG)",
4423 " #error to use -DPEG use: spin -o3 -a",
4424 "#endif",
4425 "#ifdef HC",
4426 " #ifdef SFH", /* cannot happen -- undef-ed in this case */
4427 " #error cannot combine -DHC and -DSFH",
4428 " /* use of NOCOMP is the real reason */",
4429 " #else",
4430 " #ifdef NOCOMP",
4431 " #error cannot combine -DHC and -DNOCOMP",
4432 " #endif",
4433 " #endif",
4434 " #ifdef BITSTATE",
4435 " #error cannot combine -DHC and -DBITSTATE",
4436 " #endif",
4437 "#endif",
4438 "#if defined(SAFETY) && defined(NP)",
4439 " #error cannot combine -DNP and -DBFS or -DSAFETY",
4440 "#endif",
4441 "#ifdef MA",
4442 " #ifdef BITSTATE",
4443 " #error cannot combine -DMA and -DBITSTATE",
4444 " #endif",
4445 " #if MA <= 0",
4446 " #error usage: -DMA=N with N > 0 and N < VECTORSZ",
4447 " #endif",
4448 "#endif",
4449 "#ifdef COLLAPSE",
4450 " #ifdef BITSTATE",
4451 " #error cannot combine -DBITSTATE and -DCOLLAPSE",
4452 " #endif",
4453 " #ifdef SFH",
4454 " #error cannot combine -DCOLLAPSE and -DSFH",
4455 " /* use of NOCOMP is the real reason */",
4456 " #else",
4457 " #ifdef NOCOMP",
4458 " #error cannot combine -DCOLLAPSE and -DNOCOMP",
4459 " #endif",
4460 " #endif",
4461 "#endif",
4462 " if (maxdepth <= 0 || ssize <= 1) usage(efd);",
4463 "#if SYNC>0 && !defined(NOREDUCE)",
4464 " if (a_cycles && fairness)",
4465 " { fprintf(efd, \"error: p.o. reduction not compatible with \");",
4466 " fprintf(efd, \"fairness (-f) in models\\n\");",
4467 " fprintf(efd, \" with rendezvous operations: \");",
4468 " fprintf(efd, \"recompile with -DNOREDUCE\\n\");",
4469 " pan_exit(1);",
4470 " }",
4471 "#endif",
4472 "#if defined(REM_VARS) && !defined(NOREDUCE)",
4473 " #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)",
4474 "#endif",
4475 "#if defined(NOCOMP) && !defined(BITSTATE)",
4476 " if (a_cycles)",
4477 " { fprintf(efd, \"error: use of -DNOCOMP voids -l and -a\\n\");",
4478 " pan_exit(1);",
4479 " }",
4480 "#endif",
4481
4482 "#ifdef MEMLIM",
4483 " memlim = ((double) MEMLIM) * (double) (1<<20); /* size in Mbyte */",
4484 "#endif",
4485
4486 "#ifndef BITSTATE",
4487 " if (Nrun > 1) HASH_NR = Nrun - 1;",
4488 "#endif",
4489 " if (Nrun < 1 || Nrun > 32)",
4490 " { fprintf(efd, \"error: invalid arg for -R\\n\");",
4491 " usage(efd);",
4492 " }",
4493 "#ifndef SAFETY",
4494 " if (fairness && !a_cycles)",
4495 " { fprintf(efd, \"error: -f requires -a or -l\\n\");",
4496 " usage(efd);",
4497 " }",
4498 " #if ACCEPT_LAB==0",
4499 " if (a_cycles)",
4500 " { fprintf(efd, \"error: no accept labels defined \");",
4501 " fprintf(efd, \"in model (for option -a)\\n\");",
4502 " usage(efd);",
4503 " }",
4504 " #endif",
4505 "#endif",
4506 "#ifndef NOREDUCE",
4507 " #ifdef HAS_ENABLED",
4508 " #error use of enabled() requires -DNOREDUCE",
4509 " #endif",
4510 " #ifdef HAS_PCVALUE",
4511 " #error use of pcvalue() requires -DNOREDUCE",
4512 " #endif",
4513 " #ifdef HAS_BADELSE",
4514 " #error use of 'else' combined with i/o stmnts requires -DNOREDUCE",
4515 " #endif",
4516 " #ifdef HAS_LAST",
4517 " #error use of _last requires -DNOREDUCE",
4518 " #endif",
4519 "#endif",
4520
4521 "#if SYNC>0 && !defined(NOREDUCE)",
4522 " #ifdef HAS_UNLESS",
4523 " fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
4524 " fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
4525 " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
4526 " #ifdef BFS",
4527 " fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
4528 " #endif",
4529 " #endif",
4530 "#endif",
4531 "#if SYNC>0 && defined(BFS)",
4532 " #warning use of rendezvous with BFS does not preserve all invalid endstates",
4533 "#endif",
4534 "#if !defined(REACH) && !defined(BITSTATE)",
4535 " if (iterative != 0 && a_cycles == 0)",
4536 " { fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
4537 " }",
4538 "#endif",
4539 "#if defined(BITSTATE) && defined(REACH)",
4540 " #warning -DREACH is voided by -DBITSTATE",
4541 "#endif",
4542 "#if defined(MA) && defined(REACH)",
4543 " #warning -DREACH is voided by -DMA",
4544 "#endif",
4545 "#if defined(FULLSTACK) && defined(CNTRSTACK)",
4546 " #error cannot combine -DFULLSTACK and -DCNTRSTACK",
4547 "#endif",
4548 "#if defined(VERI)",
4549 " #if ACCEPT_LAB>0",
4550 " #ifndef BFS",
4551 " if (!a_cycles",
4552 " #ifdef HAS_CODE",
4553 " && !readtrail",
4554 " #endif",
4555 " #if NCORE>1",
4556 " && core_id == 0",
4557 " #endif",
4558 " && !state_tables)",
4559 " { fprintf(efd, \"warning: never claim + accept labels \");",
4560 " fprintf(efd, \"requires -a flag to fully verify\\n\");",
4561 " }",
4562 " #else",
4563 " if (!state_tables",
4564 " #ifdef HAS_CODE",
4565 " && !readtrail",
4566 " #endif",
4567 " )",
4568 " { fprintf(efd, \"warning: verification in BFS mode \");",
4569 " fprintf(efd, \"is restricted to safety properties\\n\");",
4570 " }",
4571 " #endif",
4572 " #endif",
4573 "#endif",
4574 "#ifndef SAFETY",
4575 " if (!a_cycles",
4576 " #ifdef HAS_CODE",
4577 " && !readtrail",
4578 " #endif",
4579 " #if NCORE>1",
4580 " && core_id == 0",
4581 " #endif",
4582 " && !state_tables)",
4583 " { fprintf(efd, \"hint: this search is more efficient \");",
4584 " fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
4585 " }",
4586 " #ifndef NOCOMP",
4587 " if (!a_cycles)",
4588 " { S_A = 0;",
4589 " } else",
4590 " { if (!fairness)",
4591 " { S_A = 1; /* _a_t */",
4592 " #ifndef NOFAIR",
4593 " } else /* _a_t and _cnt[NFAIR] */",
4594 " { S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;",
4595 " /* -2 because first two uchars in now are masked */",
4596 " #endif",
4597 " } }",
4598 " #endif",
4599 "#endif",
4600 " signal(SIGINT, stopped);",
4601 " set_masks();",
4602 "#ifdef BFS",
4603 " trail = (Trail *) emalloc(6*sizeof(Trail));",
4604 " trail += 3;",
4605 "#else",
4606 " trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
4607 " trail++; /* protect trpt-1 refs at depth 0 */",
4608 "#endif",
4609 "#ifdef SVDUMP",
4610 " if (vprefix > 0)",
4611 " { char nm[64];",
4612 " sprintf(nm, \"%%s.svd\", PanSource);",
4613 " if ((svfd = creat(nm, TMODE)) < 0)",
4614 " { fprintf(efd, \"couldn't create %%s\\n\", nm);",
4615 " vprefix = 0;",
4616 " } }",
4617 "#endif",
4618 "#ifdef RANDSTOR",
4619 " srand(123);",
4620 "#endif",
4621 "#if SYNC>0 && ASYNC==0",
4622 " set_recvs();",
4623 "#endif",
4624 " run();",
4625 " done = 1;",
4626 " wrapup();",
4627 " return 0;",
4628 "}", /* end of main() */
4629 "",
4630 "void",
4631 "usage(FILE *fd)",
4632 "{",
4633 " fprintf(fd, \"%%s\\n\", SpinVersion);",
4634 " fprintf(fd, \"Valid Options are:\\n\");",
4635 "#ifndef SAFETY",
4636 "#ifdef NP",
4637 " fprintf(fd, \"\t-a -> is disabled by -DNP \");",
4638 " fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
4639 "#else",
4640 " fprintf(fd, \"\t-a find acceptance cycles\\n\");",
4641 "#endif",
4642 "#else",
4643 " fprintf(fd, \"\t-a,-l,-f -> are disabled by -DSAFETY\\n\");",
4644 "#endif",
4645 " fprintf(fd, \"\t-A ignore assert() violations\\n\");",
4646 " fprintf(fd, \"\t-b consider it an error to exceed the depth-limit\\n\");",
4647 " fprintf(fd, \"\t-cN stop at Nth error \");",
4648 " fprintf(fd, \"(defaults to -c1)\\n\");",
4649 " fprintf(fd, \"\t-d print state tables and stop\\n\");",
4650 " fprintf(fd, \"\t-e create trails for all errors\\n\");",
4651 " fprintf(fd, \"\t-E ignore invalid end states\\n\");",
4652 "#ifdef SC",
4653 " fprintf(fd, \"\t-Ffile use 'file' to store disk-stack\\n\");",
4654 "#endif",
4655 "#ifndef NOFAIR",
4656 " fprintf(fd, \"\t-f add weak fairness (to -a or -l)\\n\");",
4657 "#endif",
4658 " fprintf(fd, \"\t-hN use different hash-seed N:1..32\\n\");",
4659 " fprintf(fd, \"\t-i search for shortest path to error\\n\");",
4660 " fprintf(fd, \"\t-I like -i, but approximate and faster\\n\");",
4661 " fprintf(fd, \"\t-J reverse eval order of nested unlesses\\n\");",
4662 "#ifdef BITSTATE",
4663 " fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
4664 "#endif",
4665 "#ifdef SCHED",
4666 " fprintf(fd, \"\t-LN set scheduling restriction to N (default 10)\\n\");",
4667 "#endif",
4668 "#ifndef SAFETY",
4669 "#ifdef NP",
4670 " fprintf(fd, \"\t-l find non-progress cycles\\n\");",
4671 "#else",
4672 " fprintf(fd, \"\t-l find non-progress cycles -> \");",
4673 " fprintf(fd, \"disabled, requires \");",
4674 " fprintf(fd, \"compilation with -DNP\\n\");",
4675 "#endif",
4676 "#endif",
4677 #ifndef POWOW
4678 "#ifdef BITSTATE",
4679 " fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");",
4680 " fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");",
4681 "#endif",
4682 #endif
4683 " fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
4684 " fprintf(fd, \"\t-n no listing of unreached states\\n\");",
4685 "#ifdef SVDUMP",
4686 " fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
4687 "#endif",
4688 " fprintf(fd, \"\t-QN set time-limit on execution of N minutes\\n\");",
4689 " fprintf(fd, \"\t-q require empty chans in valid end states\\n\");",
4690 "#ifdef HAS_CODE",
4691 " fprintf(fd, \"\t-r read and execute trail - can add -v,-n,-PN,-g,-C\\n\");",
4692 " fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");",
4693 " fprintf(fd, \"\t-C read and execute trail - columnated output (can add -v,-n)\\n\");",
4694 " fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");",
4695 " fprintf(fd, \"\t-g read and execute trail + msc gui support\\n\");",
4696 " fprintf(fd, \"\t-S silent replay: only user defined printfs show\\n\");",
4697 "#endif",
4698 "#ifdef BITSTATE",
4699 " fprintf(fd, \"\t-RN repeat run Nx with N \");",
4700 " fprintf(fd, \"[1..32] independent hash functions\\n\");",
4701 " fprintf(fd, \"\t-s same as -k1 (single bit per state)\\n\");",
4702 "#endif",
4703 " fprintf(fd, \"\t-T create trail files in read-only mode\\n\");",
4704 " fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
4705 " fprintf(fd, \"\t-V print SPIN version number\\n\");",
4706 " fprintf(fd, \"\t-v verbose -- filenames in unreached state listing\\n\");",
4707 " fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
4708 " fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
4709 " fprintf(fd, \"\t-x do not overwrite an existing trail file\\n\");",
4710 "#if NCORE>1",
4711 " fprintf(fd, \"\t-zN handoff states below depth N to 2nd cpu (multi_core)\\n\");",
4712 "#endif",
4713 "#ifdef HAS_CODE",
4714 " fprintf(fd, \"\\n\toptions -r, -C, -PN, -g, and -S can optionally be followed by\\n\");",
4715 " fprintf(fd, \"\ta filename argument, as in \'-r filename\', naming the trailfile\\n\");",
4716 "#endif",
4717 "#if NCORE>1",
4718 " multi_usage(fd);",
4719 "#endif",
4720 " exit(1);",
4721 "}",
4722 "",
4723 "char *",
4724 "Malloc(unsigned long n)",
4725 "{ char *tmp;",
4726 "#ifdef MEMLIM",
4727 " if (memcnt+ (double) n > memlim) goto err;",
4728 "#endif",
4729 "#if 1",
4730 " tmp = (char *) malloc(n);",
4731 " if (!tmp)",
4732 "#else",
4733 /* on linux machines, a large amount of memory is set aside
4734 * for malloc, whether it is used or not
4735 * using sbrk would make this memory arena inaccessible
4736 * the reason for using sbrk was originally to provide a
4737 * small additional speedup (since this memory is never released)
4738 */
4739 " tmp = (char *) sbrk(n);",
4740 " if (tmp == (char *) -ONE_L)",
4741 "#endif",
4742 " {",
4743 "#ifdef MEMLIM",
4744 "err:",
4745 "#endif",
4746 " printf(\"pan: out of memory\\n\");",
4747 "#ifdef MEMLIM",
4748 " printf(\"\t%%g bytes used\\n\", memcnt);",
4749 " printf(\"\t%%g bytes more needed\\n\", (double) n);",
4750 " printf(\"\t%%g bytes limit\\n\",",
4751 " memlim);",
4752 "#endif",
4753 "#ifdef COLLAPSE",
4754 " printf(\"hint: to reduce memory, recompile with\\n\");",
4755 "#ifndef MA",
4756 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
4757 "#endif",
4758 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
4759 "#else",
4760 "#ifndef BITSTATE",
4761 " printf(\"hint: to reduce memory, recompile with\\n\");",
4762 "#ifndef HC",
4763 " printf(\" -DCOLLAPSE # good, fast compression, or\\n\");",
4764 "#ifndef MA",
4765 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
4766 "#endif",
4767 " printf(\" -DHC # hash-compaction, approximation\\n\");",
4768 "#endif",
4769 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
4770 "#endif",
4771 "#endif",
4772 "#if NCORE>1",
4773 " #ifdef FULL_TRAIL",
4774 " printf(\" omit -DFULL_TRAIL or use pan -c0 to reduce memory\\n\");",
4775 " #endif",
4776 " #ifdef SEP_STATE",
4777 " printf(\"hint: to reduce memory, recompile without\\n\");",
4778 " printf(\" -DSEP_STATE # may be faster, but uses more memory\\n\");",
4779 " #endif",
4780 "#endif",
4781 " wrapup();",
4782 " }",
4783 " memcnt += (double) n;",
4784 " return tmp;",
4785 "}",
4786 "",
4787 "#define CHUNK (100*VECTORSZ)",
4788 "",
4789 "char *",
4790 "emalloc(unsigned long n) /* never released or reallocated */",
4791 "{ char *tmp;",
4792 " if (n == 0)",
4793 " return (char *) NULL;",
4794 " if (n&(sizeof(void *)-1)) /* for proper alignment */",
4795 " n += sizeof(void *)-(n&(sizeof(void *)-1));",
4796 " if ((unsigned long) left < n)", /* was: (left < (long)n) */
4797 " { grow = (n < CHUNK) ? CHUNK : n;",
4798 #if 1
4799 " have = Malloc(grow);",
4800 #else
4801 " /* gcc's sbrk can give non-aligned result */",
4802 " grow += sizeof(void *); /* allow realignment */",
4803 " have = Malloc(grow);",
4804 " if (((unsigned) have)&(sizeof(void *)-1))",
4805 " { have += (long) (sizeof(void *) ",
4806 " - (((unsigned) have)&(sizeof(void *)-1)));",
4807 " grow -= sizeof(void *);",
4808 " }",
4809 #endif
4810 " fragment += (double) left;",
4811 " left = grow;",
4812 " }",
4813 " tmp = have;",
4814 " have += (long) n;",
4815 " left -= (long) n;",
4816 " memset(tmp, 0, n);",
4817 " return tmp;",
4818 "}",
4819
4820 "void",
4821 "Uerror(char *str)",
4822 "{ /* always fatal */",
4823 " uerror(str);",
4824 "#if NCORE>1",
4825 " sudden_stop(\"Uerror\");",
4826 "#endif",
4827 " wrapup();",
4828 "}\n",
4829 "#if defined(MA) && !defined(SAFETY)",
4830 "int",
4831 "Unwind(void)",
4832 "{ Trans *t; uchar ot, _m; int tt; short II;",
4833 "#ifdef VERBOSE",
4834 " int i;",
4835 "#endif",
4836 " uchar oat = now._a_t;",
4837 " now._a_t &= ~(1|16|32);",
4838 " memcpy((char *) &comp_now, (char *) &now, vsize);",
4839 " now._a_t = oat;",
4840 "Up:",
4841 "#ifdef SC",
4842 " trpt = getframe(depth);",
4843 "#endif",
4844 "#ifdef VERBOSE",
4845 " printf(\"%%d State: \", depth);",
4846 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
4847 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
4848 " printf(\"\\n\");",
4849 "#endif",
4850 "#ifndef NOFAIR",
4851 " if (trpt->o_pm&128) /* fairness alg */",
4852 " { now._cnt[now._a_t&1] = trpt->bup.oval;",
4853 " depth--;",
4854 "#ifdef SC",
4855 " trpt = getframe(depth);",
4856 "#else",
4857 " trpt--;",
4858 "#endif",
4859 " goto Q999;",
4860 " }",
4861 "#endif",
4862 "#ifdef HAS_LAST",
4863 "#ifdef VERI",
4864 " { int d; Trail *trl;",
4865 " now._last = 0;",
4866 " for (d = 1; d < depth; d++)",
4867 " { trl = getframe(depth-d); /* was trl = (trpt-d); */",
4868 " if (trl->pr != 0)",
4869 " { now._last = trl->pr - BASE;",
4870 " break;",
4871 " } } }",
4872 "#else",
4873 " now._last = (depth<1)?0:(trpt-1)->pr;",
4874 "#endif",
4875 "#endif",
4876 "#ifdef EVENT_TRACE",
4877 " now._event = trpt->o_event;",
4878 "#endif",
4879 " if ((now._a_t&1) && depth <= A_depth)",
4880 " { now._a_t &= ~(1|16|32);",
4881 " if (fairness) now._a_t |= 2; /* ? */",
4882 " A_depth = 0;",
4883 " goto CameFromHere; /* checkcycles() */",
4884 " }",
4885 " t = trpt->o_t;",
4886 " ot = trpt->o_ot; II = trpt->pr;",
4887 " tt = trpt->o_tt; this = pptr(II);",
4888 " _m = do_reverse(t, II, trpt->o_m);",
4889 "#ifdef VERBOSE",
4890 " printf(\"%%3d: proc %%d \", depth, II);",
4891 " printf(\"reverses %%d, %%d to %%d,\",",
4892 " t->forw, tt, t->st);",
4893 " printf(\" %%s [abit=%%d,adepth=%%d,\", ",
4894 " t->tp, now._a_t, A_depth);",
4895 " printf(\"tau=%%d,%%d] <unwind>\\n\", ",
4896 " trpt->tau, (trpt-1)->tau);",
4897 "#endif",
4898 " depth--;",
4899 "#ifdef SC",
4900 " trpt = getframe(depth);",
4901 "#else",
4902 " trpt--;",
4903 "#endif",
4904 " /* reached[ot][t->st] = 1; 3.4.13 */",
4905 " ((P0 *)this)->_p = tt;",
4906 "#ifndef NOFAIR",
4907 " if ((trpt->o_pm&32))",
4908 " {",
4909 "#ifdef VERI",
4910 " if (now._cnt[now._a_t&1] == 0)",
4911 " now._cnt[now._a_t&1] = 1;",
4912 "#endif",
4913 " now._cnt[now._a_t&1] += 1;",
4914 " }",
4915 "Q999:",
4916 " if (trpt->o_pm&8)",
4917 " { now._a_t &= ~2;",
4918 " now._cnt[now._a_t&1] = 0;",
4919 " }",
4920 " if (trpt->o_pm&16)",
4921 " now._a_t |= 2;",
4922 "#endif",
4923 "CameFromHere:",
4924 " if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)",
4925 " return depth;",
4926 " if (depth > 0) goto Up;",
4927 " return 0;",
4928 "}",
4929 "#endif",
4930 "static char unwinding;",
4931 "void",
4932 "uerror(char *str)",
4933 "{ static char laststr[256];",
4934 " int is_cycle;",
4935 "",
4936 " if (unwinding) return; /* 1.4.2 */",
4937 " if (strncmp(str, laststr, 254))",
4938 "#if NCORE>1",
4939 " cpu_printf(\"pan: %%s (at depth %%ld)\\n\", str,",
4940 "#else",
4941 " printf(\"pan: %%s (at depth %%ld)\\n\", str,",
4942 "#endif",
4943 "#if NCORE>1",
4944 " (nr_handoffs * z_handoff) + ",
4945 "#endif",
4946 " ((depthfound==-1)?depth:depthfound));",
4947 " strncpy(laststr, str, 254);",
4948 " errors++;",
4949 "#ifdef HAS_CODE",
4950 " if (readtrail) { wrap_trail(); return; }",
4951 "#endif",
4952 " is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
4953 " if (!is_cycle)",
4954 " { depth++; trpt++;", /* include failed step */
4955 " }",
4956 " if ((every_error != 0)",
4957 " || errors == upto)",
4958 " {",
4959 "#if defined(MA) && !defined(SAFETY)",
4960 " if (is_cycle)",
4961 " { int od = depth;",
4962 " unwinding = 1;",
4963 " depthfound = Unwind();",
4964 " unwinding = 0;",
4965 " depth = od;",
4966 " }",
4967 "#endif",
4968 "#if NCORE>1",
4969 " writing_trail = 1;",
4970 "#endif",
4971 "#ifdef BFS",
4972 " if (depth > 1) trpt--;",
4973 " nuerror(str);",
4974 " if (depth > 1) trpt++;",
4975 "#else",
4976 " putrail();",
4977 "#endif",
4978 "#if defined(MA) && !defined(SAFETY)",
4979 " if (strstr(str, \" cycle\"))",
4980 " { if (every_error)",
4981 " printf(\"sorry: MA writes 1 trail max\\n\");",
4982 " wrapup(); /* no recovery from unwind */",
4983 " }",
4984 "#endif",
4985 "#if NCORE>1",
4986 " if (search_terminated != NULL)",
4987 " { *search_terminated |= 4; /* uerror */",
4988 " }",
4989 " writing_trail = 0;",
4990 "#endif",
4991 " }",
4992 " if (!is_cycle)",
4993 " { depth--; trpt--; /* undo */",
4994 " }",
4995 "#ifndef BFS",
4996 " if (iterative != 0 && maxdepth > 0)",
4997 " { maxdepth = (iterative == 1)?(depth-1):(depth/2);",
4998 " warned = 1;",
4999 " printf(\"pan: reducing search depth to %%ld\\n\",",
5000 " maxdepth);",
5001 " } else",
5002 "#endif",
5003 " if (errors >= upto && upto != 0)",
5004 " {",
5005 "#if NCORE>1",
5006 " sudden_stop(\"uerror\");",
5007 "#endif",
5008 " wrapup();",
5009 " }",
5010 " depthfound = -1;",
5011 "}\n",
5012 "int",
5013 "xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
5014 "{ Trans *T; int j, retval=1;",
5015 " for (T = trans[M][i]; T; T = T->nxt)",
5016 " if (T && T->tp)",
5017 " { if (strcmp(T->tp, \".(goto)\") == 0",
5018 " || strncmp(T->tp, \"goto :\", 6) == 0)",
5019 " return 1; /* not reported */",
5020 "",
5021 " printf(\"\\tline %%d\", lno);",
5022 " if (verbose)",
5023 " for (j = 0; j < sizeof(mp); j++)",
5024 " if (i >= mp[j].from && i <= mp[j].upto)",
5025 " { printf(\", \\\"%%s\\\"\", mp[j].fnm);",
5026 " break;",
5027 " }",
5028 " printf(\", state %%d\", i);",
5029 " if (strcmp(T->tp, \"\") != 0)",
5030 " { char *q;",
5031 " q = transmognify(T->tp);",
5032 " printf(\", \\\"%%s\\\"\", q?q:\"\");",
5033 " } else if (stopstate[M][i])",
5034 " printf(\", -end state-\");",
5035 " printf(\"\\n\");",
5036 " retval = 0; /* reported */",
5037 " }",
5038 " return retval;",
5039 "}\n",
5040 "void",
5041 "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
5042 "{ int i, m=0;\n",
5043 "#ifdef VERI",
5044 " if (M == VERI && !verbose) return;",
5045 "#endif",
5046 " printf(\"unreached in proctype %%s\\n\", procname[M]);",
5047 " for (i = 1; i < N; i++)",
5048 #if 0
5049 " if (which[i] == 0 /* && trans[M][i] */)",
5050 #else
5051 " if (which[i] == 0",
5052 " && (mapstate[M][i] == 0",
5053 " || which[mapstate[M][i]] == 0))",
5054 #endif
5055 " m += xrefsrc((int) src[i], mp, M, i);",
5056 " else",
5057 " m++;",
5058 " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
5059 "}",
5060 "#if NCORE>1 && !defined(SEP_STATE)",
5061 "static long rev_trail_cnt;",
5062 "",
5063 "#ifdef FULL_TRAIL",
5064 "void",
5065 "rev_trail(int fd, volatile Stack_Tree *st_tr)",
5066 "{ long j; char snap[64];",
5067 "",
5068 " if (!st_tr)",
5069 " { return;",
5070 " }",
5071 " rev_trail(fd, st_tr->prv);",
5072 "#ifdef VERBOSE",
5073 " printf(\"%%d (%%d) LRT [%%d,%%d] -- %%9u (root %%9u)\\n\",",
5074 " depth, rev_trail_cnt, st_tr->pr, st_tr->t_id, st_tr, stack_last[core_id]);",
5075 "#endif",
5076 " if (st_tr->pr != 255)", /* still needed? */
5077 " { sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
5078 " rev_trail_cnt++, st_tr->pr, st_tr->t_id);",
5079 " j = strlen(snap);",
5080 " if (write(fd, snap, j) != j)",
5081 " { printf(\"pan: error writing trailfile\\n\");",
5082 " close(fd);",
5083 " wrapup();",
5084 " return;",
5085 " }",
5086 " } else /* handoff point */",
5087 " { if (a_cycles)",
5088 " { write(fd, \"-1:-1:-1\\n\", 9);",
5089 " } }",
5090 "}",
5091 "#endif", /* FULL_TRAIL */
5092 "#endif", /* NCORE>1 */
5093 "",
5094 "void",
5095 "putrail(void)",
5096 "{ int fd;",
5097 "#if defined VERI || defined(MERGED)",
5098 " char snap[64];",
5099 "#endif",
5100 "#if NCORE==1 || defined(SEP_STATE) || !defined(FULL_TRAIL)",
5101 " long i, j;",
5102 " Trail *trl;",
5103 "#endif",
5104 " fd = make_trail();",
5105 " if (fd < 0) return;",
5106 "#ifdef VERI",
5107 " sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
5108 " write(fd, snap, strlen(snap));",
5109 "#endif",
5110 "#ifdef MERGED",
5111 " sprintf(snap, \"-4:-4:-4\\n\");",
5112 " write(fd, snap, strlen(snap));",
5113 "#endif",
5114 "#if NCORE>1 && !defined(SEP_STATE) && defined(FULL_TRAIL)",
5115 " rev_trail_cnt = 1;",
5116 " enter_critical(GLOBAL_LOCK);",
5117 " rev_trail(fd, stack_last[core_id]);",
5118 " leave_critical(GLOBAL_LOCK);",
5119 "#else",
5120 " i = 1; /* trail starts at position 1 */",
5121 " #if NCORE>1 && defined(SEP_STATE)",
5122 " if (cur_Root.m_vsize > 0) { i++; depth++; }",
5123 " #endif",
5124 " for ( ; i <= depth; i++)",
5125 " { if (i == depthfound+1)",
5126 " write(fd, \"-1:-1:-1\\n\", 9);",
5127 " trl = getframe(i);",
5128 " if (!trl->o_t) continue;",
5129 " if (trl->o_pm&128) continue;",
5130 " sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
5131 " i, trl->pr, trl->o_t->t_id);",
5132 " j = strlen(snap);",
5133 " if (write(fd, snap, j) != j)",
5134 " { printf(\"pan: error writing trailfile\\n\");",
5135 " close(fd);",
5136 " wrapup();",
5137 " } }",
5138 "#endif",
5139 " close(fd);",
5140 "#if NCORE>1",
5141 " cpu_printf(\"pan: wrote trailfile\\n\");",
5142 "#endif",
5143 "}\n",
5144 "void",
5145 "sv_save(void) /* push state vector onto save stack */",
5146 "{ if (!svtack->nxt)",
5147 " { svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));",
5148 " svtack->nxt->body = emalloc(vsize*sizeof(char));",
5149 " svtack->nxt->lst = svtack;",
5150 " svtack->nxt->m_delta = vsize;",
5151 " svmax++;",
5152 " } else if (vsize > svtack->nxt->m_delta)",
5153 " { svtack->nxt->body = emalloc(vsize*sizeof(char));",
5154 " svtack->nxt->lst = svtack;",
5155 " svtack->nxt->m_delta = vsize;",
5156 " svmax++;",
5157 " }",
5158 " svtack = svtack->nxt;",
5159 "#if SYNC",
5160 " svtack->o_boq = boq;",
5161 "#endif",
5162 " svtack->o_delta = vsize; /* don't compress */",
5163 " memcpy((char *)(svtack->body), (char *) &now, vsize);",
5164 "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
5165 " c_stack((uchar *) &(svtack->c_stack[0]));",
5166 "#endif",
5167 "#ifdef DEBUG",
5168 " cpu_printf(\"%%d: sv_save\\n\", depth);",
5169 "#endif",
5170 "}\n",
5171 "void",
5172 "sv_restor(void) /* pop state vector from save stack */",
5173 "{",
5174 " memcpy((char *)&now, svtack->body, svtack->o_delta);",
5175 "#if SYNC",
5176 " boq = svtack->o_boq;",
5177 "#endif",
5178
5179 "#if defined(C_States) && (HAS_TRACK==1)",
5180 "#ifdef HAS_STACK",
5181 " c_unstack((uchar *) &(svtack->c_stack[0]));",
5182 "#endif",
5183 " c_revert((uchar *) &(now.c_state[0]));",
5184 "#endif",
5185
5186 " if (vsize != svtack->o_delta)",
5187 " Uerror(\"sv_restor\");",
5188 " if (!svtack->lst)",
5189 " Uerror(\"error: v_restor\");",
5190 " svtack = svtack->lst;",
5191 "#ifdef DEBUG",
5192 " cpu_printf(\" sv_restor\\n\");",
5193 "#endif",
5194 "}\n",
5195 "void",
5196 "p_restor(int h)",
5197 "{ int i; char *z = (char *) &now;\n",
5198 " proc_offset[h] = stack->o_offset;",
5199 " proc_skip[h] = (uchar) stack->o_skip;",
5200 "#ifndef XUSAFE",
5201 " p_name[h] = stack->o_name;",
5202 "#endif",
5203 "#ifndef NOCOMP",
5204 " for (i = vsize + stack->o_skip; i > vsize; i--)",
5205 " Mask[i-1] = 1; /* align */",
5206 "#endif",
5207 " vsize += stack->o_skip;",
5208 " memcpy(z+vsize, stack->body, stack->o_delta);",
5209 " vsize += stack->o_delta;",
5210 "#ifndef NOVSZ",
5211 " now._vsz = vsize;",
5212 "#endif",
5213 "#ifndef NOCOMP",
5214 " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
5215 " Mask[vsize - i] = 1; /* pad */",
5216 " Mask[proc_offset[h]] = 1; /* _pid */",
5217 "#endif",
5218 " if (BASE > 0 && h > 0)",
5219 " ((P0 *)pptr(h))->_pid = h-BASE;",
5220 " else",
5221 " ((P0 *)pptr(h))->_pid = h;",
5222 " i = stack->o_delqs;",
5223 " now._nr_pr += 1;",
5224 " if (!stack->lst) /* debugging */",
5225 " Uerror(\"error: p_restor\");",
5226 " stack = stack->lst;",
5227 " this = pptr(h);",
5228 " while (i-- > 0)",
5229 " q_restor();",
5230 "}\n",
5231 "void",
5232 "q_restor(void)",
5233 "{ char *z = (char *) &now;",
5234 "#ifndef NOCOMP",
5235 " int k, k_end;",
5236 "#endif",
5237 " q_offset[now._nr_qs] = stack->o_offset;",
5238 " q_skip[now._nr_qs] = (uchar) stack->o_skip;",
5239 "#ifndef XUSAFE",
5240 " q_name[now._nr_qs] = stack->o_name;",
5241 "#endif",
5242 " vsize += stack->o_skip;",
5243 " memcpy(z+vsize, stack->body, stack->o_delta);",
5244 " vsize += stack->o_delta;",
5245 "#ifndef NOVSZ",
5246 " now._vsz = vsize;",
5247 "#endif",
5248 " now._nr_qs += 1;",
5249 "#ifndef NOCOMP",
5250 " k_end = stack->o_offset;",
5251 " k = k_end - stack->o_skip;",
5252 "#if SYNC",
5253 "#ifndef BFS",
5254 " if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
5255 "#endif",
5256 "#endif",
5257 " for ( ; k < k_end; k++)",
5258 " Mask[k] = 1;",
5259 "#endif",
5260 " if (!stack->lst) /* debugging */",
5261 " Uerror(\"error: q_restor\");",
5262 " stack = stack->lst;",
5263 "}",
5264
5265 "typedef struct IntChunks {",
5266 " int *ptr;",
5267 " struct IntChunks *nxt;",
5268 "} IntChunks;",
5269 "IntChunks *filled_chunks[512];",
5270 "IntChunks *empty_chunks[512];",
5271
5272 "int *",
5273 "grab_ints(int nr)",
5274 "{ IntChunks *z;",
5275 " if (nr >= 512) Uerror(\"cannot happen grab_int\");",
5276 " if (filled_chunks[nr])",
5277 " { z = filled_chunks[nr];",
5278 " filled_chunks[nr] = filled_chunks[nr]->nxt;",
5279 " } else ",
5280 " { z = (IntChunks *) emalloc(sizeof(IntChunks));",
5281 " z->ptr = (int *) emalloc(nr * sizeof(int));",
5282 " }",
5283 " z->nxt = empty_chunks[nr];",
5284 " empty_chunks[nr] = z;",
5285 " return z->ptr;",
5286 "}",
5287 "void",
5288 "ungrab_ints(int *p, int nr)",
5289 "{ IntChunks *z;",
5290 " if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");",
5291 " z = empty_chunks[nr];",
5292 " empty_chunks[nr] = empty_chunks[nr]->nxt;",
5293 " z->ptr = p;",
5294 " z->nxt = filled_chunks[nr];",
5295 " filled_chunks[nr] = z;",
5296 "}",
5297 "int",
5298 "delproc(int sav, int h)",
5299 "{ int d, i=0;",
5300 "#ifndef NOCOMP",
5301 " int o_vsize = vsize;",
5302 "#endif",
5303 " if (h+1 != (int) now._nr_pr) return 0;\n",
5304 " while (now._nr_qs",
5305 " && q_offset[now._nr_qs-1] > proc_offset[h])",
5306 " { delq(sav);",
5307 " i++;",
5308 " }",
5309 " d = vsize - proc_offset[h];",
5310 " if (sav)",
5311 " { if (!stack->nxt)",
5312 " { stack->nxt = (Stack *)",
5313 " emalloc(sizeof(Stack));",
5314 " stack->nxt->body = ",
5315 " emalloc(Maxbody*sizeof(char));",
5316 " stack->nxt->lst = stack;",
5317 " smax++;",
5318 " }",
5319 " stack = stack->nxt;",
5320 " stack->o_offset = proc_offset[h];",
5321 "#if VECTORSZ>32000",
5322 " stack->o_skip = (int) proc_skip[h];",
5323 "#else",
5324 " stack->o_skip = (short) proc_skip[h];",
5325 "#endif",
5326 "#ifndef XUSAFE",
5327 " stack->o_name = p_name[h];",
5328 "#endif",
5329 " stack->o_delta = d;",
5330 " stack->o_delqs = i;",
5331 " memcpy(stack->body, (char *)pptr(h), d);",
5332 " }",
5333 " vsize = proc_offset[h];",
5334 " now._nr_pr = now._nr_pr - 1;",
5335 " memset((char *)pptr(h), 0, d);",
5336 " vsize -= (int) proc_skip[h];",
5337 "#ifndef NOVSZ",
5338 " now._vsz = vsize;",
5339 "#endif",
5340 "#ifndef NOCOMP",
5341 " for (i = vsize; i < o_vsize; i++)",
5342 " Mask[i] = 0; /* reset */",
5343 "#endif",
5344 " return 1;",
5345 "}\n",
5346 "void",
5347 "delq(int sav)",
5348 "{ int h = now._nr_qs - 1;",
5349 " int d = vsize - q_offset[now._nr_qs - 1];",
5350 "#ifndef NOCOMP",
5351 " int k, o_vsize = vsize;",
5352 "#endif",
5353 " if (sav)",
5354 " { if (!stack->nxt)",
5355 " { stack->nxt = (Stack *)",
5356 " emalloc(sizeof(Stack));",
5357 " stack->nxt->body = ",
5358 " emalloc(Maxbody*sizeof(char));",
5359 " stack->nxt->lst = stack;",
5360 " smax++;",
5361 " }",
5362 " stack = stack->nxt;",
5363 " stack->o_offset = q_offset[h];",
5364 "#if VECTORSZ>32000",
5365 " stack->o_skip = (int) q_skip[h];",
5366 "#else",
5367 " stack->o_skip = (short) q_skip[h];",
5368 "#endif",
5369 "#ifndef XUSAFE",
5370 " stack->o_name = q_name[h];",
5371 "#endif",
5372 " stack->o_delta = d;",
5373 " memcpy(stack->body, (char *)qptr(h), d);",
5374 " }",
5375 " vsize = q_offset[h];",
5376 " now._nr_qs = now._nr_qs - 1;",
5377 " memset((char *)qptr(h), 0, d);",
5378 " vsize -= (int) q_skip[h];",
5379 "#ifndef NOVSZ",
5380 " now._vsz = vsize;",
5381 "#endif",
5382 "#ifndef NOCOMP",
5383 " for (k = vsize; k < o_vsize; k++)",
5384 " Mask[k] = 0; /* reset */",
5385 "#endif",
5386 "}\n",
5387 "int",
5388 "qs_empty(void)",
5389 "{ int i;",
5390 " for (i = 0; i < (int) now._nr_qs; i++)",
5391 " { if (q_sz(i) > 0)",
5392 " return 0;",
5393 " }",
5394 " return 1;",
5395 "}\n",
5396 "int",
5397 "endstate(void)",
5398 "{ int i; P0 *ptr;",
5399 " for (i = BASE; i < (int) now._nr_pr; i++)",
5400 " { ptr = (P0 *) pptr(i);",
5401 " if (!stopstate[ptr->_t][ptr->_p])",
5402 " return 0;",
5403 " }",
5404 " if (strict) return qs_empty();",
5405 "#if defined(EVENT_TRACE) && !defined(OTIM)",
5406 " if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
5407 " { printf(\"pan: event_trace not completed\\n\");",
5408 " return 0;",
5409 " }",
5410 "#endif",
5411 " return 1;",
5412 "}\n",
5413 "#ifndef SAFETY",
5414 "void",
5415 "checkcycles(void)",
5416 "{ uchar o_a_t = now._a_t;",
5417 "#ifdef SCHED",
5418 " int o_limit;",
5419 "#endif",
5420 "#ifndef NOFAIR",
5421 " uchar o_cnt = now._cnt[1];",
5422 "#endif",
5423 "#ifdef FULLSTACK",
5424 "#ifndef MA",
5425 " struct H_el *sv = trpt->ostate; /* save */",
5426 "#else",
5427 " uchar prov = trpt->proviso; /* save */",
5428 "#endif",
5429 "#endif",
5430 "#ifdef DEBUG",
5431 " { int i; uchar *v = (uchar *) &now;",
5432 " printf(\" set Seed state \");",
5433 "#ifndef NOFAIR",
5434 " if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
5435 " now._cnt[0], now._cnt[1], now._nr_pr);",
5436 "#endif",
5437 " /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */",
5438 " printf(\"\\n\");",
5439 " }",
5440 " printf(\"%%d: cycle check starts\\n\", depth);",
5441 "#endif",
5442 " now._a_t |= (1|16|32);",
5443 " /* 1 = 2nd DFS; (16|32) to help hasher */",
5444 "#ifndef NOFAIR",
5445 #if 0
5446 " if (fairness)",
5447 " { now._a_t &= ~2; /* pre-apply Rule 3 */",
5448 " now._cnt[1] = 0;", /* reset both a-bit and cnt=0 */
5449 " /* avoid matching seed on claim stutter on this state */",
5450 " }",
5451 #else
5452 " now._cnt[1] = now._cnt[0];",
5453 #endif
5454 "#endif",
5455 " memcpy((char *)&A_Root, (char *)&now, vsize);",
5456 " A_depth = depthfound = depth;",
5457
5458 "#if NCORE>1",
5459 " mem_put_acc();", /* handoff accept states */
5460 "#else",
5461 " #ifdef SCHED",
5462 " o_limit = trpt->sched_limit;",
5463 " trpt->sched_limit = 0;",
5464 " #endif",
5465 " new_state(); /* start 2nd DFS */",
5466 " #ifdef SCHED",
5467 " trpt->sched_limit = o_limit;",
5468 " #endif",
5469 "#endif",
5470
5471 " now._a_t = o_a_t;",
5472 "#ifndef NOFAIR",
5473 " now._cnt[1] = o_cnt;",
5474 "#endif",
5475 " A_depth = 0; depthfound = -1;",
5476 "#ifdef DEBUG",
5477 " printf(\"%%d: cycle check returns\\n\", depth);",
5478 "#endif",
5479 "#ifdef FULLSTACK",
5480 "#ifndef MA",
5481 " trpt->ostate = sv; /* restore */",
5482 "#else",
5483 " trpt->proviso = prov;",
5484 "#endif",
5485 "#endif",
5486 "}",
5487 "#endif\n",
5488 "#if defined(FULLSTACK) && defined(BITSTATE)",
5489 "struct H_el *Free_list = (struct H_el *) 0;",
5490 "void",
5491 "onstack_init(void) /* to store stack states in a bitstate search */",
5492 "{ S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));",
5493 "}",
5494 "struct H_el *",
5495 "grab_state(int n)",
5496 "{ struct H_el *v, *last = 0;",
5497 " if (H_tab == S_Tab)",
5498 " { for (v = Free_list; v && ((int) v->tagged >= n); v=v->nxt)",
5499 " { if ((int) v->tagged == n)",
5500 " { if (last)",
5501 " last->nxt = v->nxt;",
5502 " else",
5503 "gotcha: Free_list = v->nxt;",
5504 " v->tagged = 0;",
5505 " v->nxt = 0;",
5506 "#ifdef COLLAPSE",
5507 " v->ln = 0;",
5508 "#endif",
5509 " return v;",
5510 " }",
5511 " Fh++; last=v;",
5512 " }",
5513 " /* new: second try */",
5514 " v = Free_list;", /* try to avoid emalloc */
5515 " if (v && ((int) v->tagged >= n))",
5516 " goto gotcha;",
5517 " ngrabs++;",
5518 " }",
5519 " return (struct H_el *)",
5520 " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
5521 "}\n",
5522 "#else",
5523
5524 "#if NCORE>1",
5525 "struct H_el *",
5526 "grab_state(int n)",
5527 "{ struct H_el *grab_shared(int);",
5528 " return grab_shared(sizeof(struct H_el)+n-sizeof(unsigned));",
5529 "}",
5530 "#else",
5531 " #ifndef AUTO_RESIZE",
5532 " #define grab_state(n) (struct H_el *) \\",
5533 " emalloc(sizeof(struct H_el)+n-sizeof(unsigned long));",
5534 " #else",
5535 " struct H_el *",
5536 " grab_state(int n)",
5537 " { struct H_el *p;",
5538 " int cnt = sizeof(struct H_el)+n-sizeof(unsigned long);",
5539 "",
5540 " if (reclaim_size >= cnt+WS)",
5541 " { if ((cnt & (WS-1)) != 0) /* alignment */",
5542 " { cnt += WS - (cnt & (WS-1));",
5543 " }",
5544 " p = (struct H_el *) reclaim_mem;",
5545 " reclaim_mem += cnt;",
5546 " reclaim_size -= cnt;",
5547 " memset(p, 0, cnt);",
5548 " } else",
5549 " { p = (struct H_el *) emalloc(cnt);",
5550 " }",
5551 " return p;",
5552 " }",
5553 " #endif",
5554 "#endif",
5555
5556 "#endif",
5557 "#ifdef COLLAPSE",
5558 "unsigned long",
5559 "ordinal(char *v, long n, short tp)",
5560 "{ struct H_el *tmp, *ntmp; long m;",
5561 " struct H_el *olst = (struct H_el *) 0;",
5562 " s_hash((uchar *)v, n);",
5563
5564 "#if NCORE>1 && !defined(SEP_STATE)",
5565 " enter_critical(CS_ID); /* uses spinlock - 1..128 */",
5566 "#endif",
5567
5568 " tmp = H_tab[j1];",
5569 " if (!tmp)",
5570 " { tmp = grab_state(n);",
5571 " H_tab[j1] = tmp;",
5572 " } else",
5573 " for ( ;; olst = tmp, tmp = tmp->nxt)",
5574 " { m = memcmp(((char *)&(tmp->state)), v, n);",
5575 " if (n == tmp->ln)",
5576 " {",
5577 " if (m == 0)",
5578 " goto done;",
5579 " if (m < 0)",
5580 " {",
5581 "Insert: ntmp = grab_state(n);",
5582 " ntmp->nxt = tmp;",
5583 " if (!olst)",
5584 " H_tab[j1] = ntmp;",
5585 " else",
5586 " olst->nxt = ntmp;",
5587 " tmp = ntmp;",
5588 " break;",
5589 " } else if (!tmp->nxt)",
5590 " {",
5591 "Append: tmp->nxt = grab_state(n);",
5592 " tmp = tmp->nxt;",
5593 " break;",
5594 " }",
5595 " continue;",
5596 " }",
5597 " if (n < tmp->ln)",
5598 " goto Insert;",
5599 " else if (!tmp->nxt)",
5600 " goto Append;",
5601 " }",
5602 " m = ++ncomps[tp];",
5603 "#ifdef FULLSTACK",
5604 " tmp->tagged = m;",
5605 "#else",
5606 " tmp->st_id = m;",
5607 "#endif",
5608 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
5609 " tmp->m_K1 = K1;",
5610 "#endif",
5611 " memcpy(((char *)&(tmp->state)), v, n);",
5612 " tmp->ln = n;",
5613 "done:",
5614
5615 "#if NCORE>1 && !defined(SEP_STATE)",
5616 " leave_critical(CS_ID); /* uses spinlock */",
5617 "#endif",
5618
5619 "#ifdef FULLSTACK",
5620 " return tmp->tagged;",
5621 "#else",
5622 " return tmp->st_id;",
5623 "#endif",
5624 "}",
5625 "",
5626 "int",
5627 "compress(char *vin, int nin) /* collapse compression */",
5628 "{ char *w, *v = (char *) &comp_now;",
5629 " int i, j;",
5630 " unsigned long n;",
5631 " static char *x;",
5632 " static uchar nbytes[513]; /* 1 + 256 + 256 */",
5633 " static unsigned short nbytelen;",
5634 " long col_q(int, char *);",
5635 " long col_p(int, char *);",
5636 "#ifndef SAFETY",
5637 " if (a_cycles)",
5638 " *v++ = now._a_t;",
5639 "#ifndef NOFAIR",
5640 " if (fairness)",
5641 " for (i = 0; i < NFAIR; i++)",
5642 " *v++ = now._cnt[i];",
5643 "#endif",
5644 "#endif",
5645 " nbytelen = 0;",
5646
5647 "#ifndef JOINPROCS",
5648 " for (i = 0; i < (int) now._nr_pr; i++)",
5649 " { n = col_p(i, (char *) 0);",
5650 "#ifdef NOFIX",
5651 " nbytes[nbytelen] = 0;",
5652 "#else",
5653 " nbytes[nbytelen] = 1;",
5654 " *v++ = ((P0 *) pptr(i))->_t;",
5655 "#endif",
5656 " *v++ = n&255;",
5657 " if (n >= (1<<8))",
5658 " { nbytes[nbytelen]++;",
5659 " *v++ = (n>>8)&255;",
5660 " }",
5661 " if (n >= (1<<16))",
5662 " { nbytes[nbytelen]++;",
5663 " *v++ = (n>>16)&255;",
5664 " }",
5665 " if (n >= (1<<24))",
5666 " { nbytes[nbytelen]++;",
5667 " *v++ = (n>>24)&255;",
5668 " }",
5669 " nbytelen++;",
5670 " }",
5671 "#else",
5672 " x = scratch;",
5673 " for (i = 0; i < (int) now._nr_pr; i++)",
5674 " x += col_p(i, x);",
5675 " n = ordinal(scratch, x-scratch, 2); /* procs */",
5676 " *v++ = n&255;",
5677 " nbytes[nbytelen] = 0;",
5678 " if (n >= (1<<8))",
5679 " { nbytes[nbytelen]++;",
5680 " *v++ = (n>>8)&255;",
5681 " }",
5682 " if (n >= (1<<16))",
5683 " { nbytes[nbytelen]++;",
5684 " *v++ = (n>>16)&255;",
5685 " }",
5686 " if (n >= (1<<24))",
5687 " { nbytes[nbytelen]++;",
5688 " *v++ = (n>>24)&255;",
5689 " }",
5690 " nbytelen++;",
5691 "#endif",
5692 "#ifdef SEPQS",
5693 " for (i = 0; i < (int) now._nr_qs; i++)",
5694 " { n = col_q(i, (char *) 0);",
5695 " nbytes[nbytelen] = 0;",
5696 " *v++ = n&255;",
5697 " if (n >= (1<<8))",
5698 " { nbytes[nbytelen]++;",
5699 " *v++ = (n>>8)&255;",
5700 " }",
5701 " if (n >= (1<<16))",
5702 " { nbytes[nbytelen]++;",
5703 " *v++ = (n>>16)&255;",
5704 " }",
5705 " if (n >= (1<<24))",
5706 " { nbytes[nbytelen]++;",
5707 " *v++ = (n>>24)&255;",
5708 " }",
5709 " nbytelen++;",
5710 " }",
5711 "#endif",
5712
5713 "#ifdef NOVSZ",
5714 " /* 3 = _a_t, _nr_pr, _nr_qs */",
5715 " w = (char *) &now + 3 * sizeof(uchar);",
5716 "#ifndef NOFAIR",
5717 " w += NFAIR;",
5718 "#endif",
5719 "#else",
5720 "#if VECTORSZ<65536",
5721 " w = (char *) &(now._vsz) + sizeof(unsigned short);",
5722 "#else",
5723 " w = (char *) &(now._vsz) + sizeof(unsigned long);",
5724 "#endif",
5725 "#endif",
5726 " x = scratch;",
5727 " *x++ = now._nr_pr;",
5728 " *x++ = now._nr_qs;",
5729
5730 " if (now._nr_qs > 0 && qptr(0) < pptr(0))",
5731 " n = qptr(0) - (uchar *) w;",
5732 " else",
5733 " n = pptr(0) - (uchar *) w;",
5734 " j = w - (char *) &now;",
5735 " for (i = 0; i < (int) n; i++, w++)",
5736 " if (!Mask[j++]) *x++ = *w;",
5737 "#ifndef SEPQS",
5738 " for (i = 0; i < (int) now._nr_qs; i++)",
5739 " x += col_q(i, x);",
5740 "#endif",
5741
5742 " x--;",
5743 " for (i = 0, j = 6; i < nbytelen; i++)",
5744 " { if (j == 6)",
5745 " { j = 0;",
5746 " *(++x) = 0;",
5747 " } else",
5748 " j += 2;",
5749 " *x |= (nbytes[i] << j);",
5750 " }",
5751 " x++;",
5752 " for (j = 0; j < WS-1; j++)",
5753 " *x++ = 0;",
5754 " x -= j; j = 0;",
5755 " n = ordinal(scratch, x-scratch, 0); /* globals */",
5756 " *v++ = n&255;",
5757 " if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
5758 " if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
5759 " if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
5760 " *v++ = j; /* add last count as a byte */",
5761
5762 " for (i = 0; i < WS-1; i++)",
5763 " *v++ = 0;",
5764 " v -= i;",
5765 "#if 0",
5766 " printf(\"collapse %%d -> %%d\\n\",",
5767 " vsize, v - (char *)&comp_now);",
5768 "#endif",
5769 " return v - (char *)&comp_now;",
5770 "}",
5771
5772 "#else",
5773 "#if !defined(NOCOMP)",
5774 "int",
5775 "compress(char *vin, int n) /* default compression */",
5776 "{",
5777 "#ifdef HC",
5778 " int delta = 0;",
5779 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
5780 "#ifndef SAFETY",
5781 " if (S_A)",
5782 " { delta++; /* _a_t */",
5783 "#ifndef NOFAIR",
5784 " if (S_A > NFAIR)",
5785 " delta += NFAIR; /* _cnt[] */",
5786 "#endif",
5787 " }",
5788 "#endif",
5789 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
5790 " delta += WS;",
5791 "#if HC>0",
5792 " memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
5793 " delta += HC;",
5794 "#endif",
5795 " return delta;",
5796 "#else",
5797 " char *vv = vin;",
5798 " char *v = (char *) &comp_now;",
5799 " int i;",
5800 " #ifndef NO_FAST_C", /* disable faster compress */
5801 " int r = 0, unroll = n/8;", /* most sv are much longer */
5802 " if (unroll > 0)",
5803 " { i = 0;",
5804 " while (r++ < unroll)",
5805 " { /* unroll 8 times, avoid ifs */",
5806 " /* 1 */ *v = *vv++;",
5807 " v += 1 - Mask[i++];",
5808 " /* 2 */ *v = *vv++;",
5809 " v += 1 - Mask[i++];",
5810 " /* 3 */ *v = *vv++;",
5811 " v += 1 - Mask[i++];",
5812 " /* 4 */ *v = *vv++;",
5813 " v += 1 - Mask[i++];",
5814 " /* 5 */ *v = *vv++;",
5815 " v += 1 - Mask[i++];",
5816 " /* 6 */ *v = *vv++;",
5817 " v += 1 - Mask[i++];",
5818 " /* 7 */ *v = *vv++;",
5819 " v += 1 - Mask[i++];",
5820 " /* 8 */ *v = *vv++;",
5821 " v += 1 - Mask[i++];",
5822 " }",
5823 " r = n - i; /* the rest, at most 7 */",
5824 " switch (r) {",
5825 " case 7: *v = *vv++; v += 1 - Mask[i++];",
5826 " case 6: *v = *vv++; v += 1 - Mask[i++];",
5827 " case 5: *v = *vv++; v += 1 - Mask[i++];",
5828 " case 4: *v = *vv++; v += 1 - Mask[i++];",
5829 " case 3: *v = *vv++; v += 1 - Mask[i++];",
5830 " case 2: *v = *vv++; v += 1 - Mask[i++];",
5831 " case 1: *v = *vv++; v += 1 - Mask[i++];",
5832 " case 0: break;",
5833 " }",
5834 " r = (n+WS-1)/WS; /* words rounded up */",
5835 " r *= WS; /* bytes */",
5836 " i = r - i; /* remainder */",
5837 " switch (i) {", /* fill word */
5838 " case 7: *v++ = 0; /* fall thru */",
5839 " case 6: *v++ = 0;",
5840 " case 5: *v++ = 0;",
5841 " case 4: *v++ = 0;",
5842 " case 3: *v++ = 0;",
5843 " case 2: *v++ = 0;",
5844 " case 1: *v++ = 0;",
5845 " case 0: break;",
5846 " default: Uerror(\"unexpected wordsize\");",
5847 " }",
5848 " v -= i;",
5849 " } else",
5850 " #endif",
5851 " { for (i = 0; i < n; i++, vv++)",
5852 " if (!Mask[i]) *v++ = *vv;",
5853 " for (i = 0; i < WS-1; i++)",
5854 " *v++ = 0;",
5855 " v -= i;",
5856 " }",
5857 "#if 0",
5858 " printf(\"compress %%d -> %%d\\n\",",
5859 " n, v - (char *)&comp_now);",
5860 "#endif",
5861 " return v - (char *)&comp_now;",
5862 "#endif",
5863 "}",
5864 "#endif",
5865 "#endif",
5866 "#if defined(FULLSTACK) && defined(BITSTATE)",
5867 "#if defined(MA)",
5868 "#if !defined(onstack_now)",
5869 "int onstack_now(void) {}", /* to suppress compiler errors */
5870 "#endif",
5871 "#if !defined(onstack_put)",
5872 "void onstack_put(void) {}", /* for this invalid combination */
5873 "#endif",
5874 "#if !defined(onstack_zap)",
5875 "void onstack_zap(void) {}", /* of directives */
5876 "#endif",
5877 "#else",
5878 "void",
5879 "onstack_zap(void)",
5880 "{ struct H_el *v, *w, *last = 0;",
5881 " struct H_el **tmp = H_tab;",
5882 " char *nv; int n, m;\n",
5883 " static char warned = 0;",
5884 "",
5885 " H_tab = S_Tab;",
5886 "#ifndef NOCOMP",
5887 " nv = (char *) &comp_now;",
5888 " n = compress((char *)&now, vsize);",
5889 "#else",
5890 "#if defined(BITSTATE) && defined(LC)",
5891 " nv = (char *) &comp_now;",
5892 " n = compact_stack((char *)&now, vsize);",
5893 "#else",
5894 " nv = (char *) &now;",
5895 " n = vsize;",
5896 "#endif",
5897 "#endif",
5898 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
5899 " s_hash((uchar *)nv, n);",
5900 "#endif",
5901 " H_tab = tmp;",
5902 " for (v = S_Tab[j1]; v; Zh++, last=v, v=v->nxt)",
5903 " { m = memcmp(&(v->state), nv, n);",
5904 " if (m == 0)",
5905 " goto Found;",
5906 " if (m < 0)",
5907 " break;",
5908 " }",
5909 "/* NotFound: */",
5910 "#ifndef ZAPH",
5911 " #if defined(BITSTATE) && NCORE>1",
5912 " /* seen this happen, likely harmless, but not yet understood */",
5913 " if (warned == 0)",
5914 " #endif",
5915 " { /* Uerror(\"stack out of wack - zap\"); */",
5916 " cpu_printf(\"pan: warning, stack incomplete\\n\");",
5917 " warned = 1;",
5918 " }",
5919 "#endif",
5920 " return;",
5921 "Found:",
5922 " ZAPS++;",
5923 " if (last)",
5924 " last->nxt = v->nxt;",
5925 " else",
5926 " S_Tab[j1] = v->nxt;",
5927 " v->tagged = (unsigned) n;",
5928 "#if !defined(NOREDUCE) && !defined(SAFETY)",
5929 " v->proviso = 0;",
5930 "#endif",
5931 " v->nxt = last = (struct H_el *) 0;",
5932 " for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
5933 " { if ((int) w->tagged <= n)",
5934 " { if (last)",
5935 " { v->nxt = w;",
5936 " last->nxt = v;",
5937 " } else",
5938 " { v->nxt = Free_list;",
5939 " Free_list = v;",
5940 " }",
5941 " return;",
5942 " }",
5943 " if (!w->nxt)",
5944 " { w->nxt = v;",
5945 " return;",
5946 " } }",
5947 " Free_list = v;",
5948 "}",
5949 "void",
5950 "onstack_put(void)",
5951 "{ struct H_el **tmp = H_tab;",
5952 " H_tab = S_Tab;",
5953 " if (hstore((char *)&now, vsize) != 0)",
5954 "#if defined(BITSTATE) && defined(LC)",
5955 " printf(\"pan: warning, double stack entry\\n\");",
5956 "#else",
5957 " #ifndef ZAPH",
5958 " Uerror(\"cannot happen - unstack_put\");",
5959 " #endif",
5960 "#endif",
5961 " H_tab = tmp;",
5962 " trpt->ostate = Lstate;",
5963 " PUT++;",
5964 "}",
5965 "int",
5966 "onstack_now(void)",
5967 "{ struct H_el *tmp;",
5968 " struct H_el **tmp2 = H_tab;",
5969 " char *v; int n, m = 1;\n",
5970 " H_tab = S_Tab;",
5971 "#ifdef NOCOMP",
5972 "#if defined(BITSTATE) && defined(LC)",
5973 " v = (char *) &comp_now;",
5974 " n = compact_stack((char *)&now, vsize);",
5975 "#else",
5976 " v = (char *) &now;",
5977 " n = vsize;",
5978 "#endif",
5979 "#else",
5980 " v = (char *) &comp_now;",
5981 " n = compress((char *)&now, vsize);",
5982 "#endif",
5983 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
5984 " s_hash((uchar *)v, n);",
5985 "#endif",
5986 " H_tab = tmp2;",
5987 " for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
5988 " { m = memcmp(((char *)&(tmp->state)),v,n);",
5989 " if (m <= 0)",
5990 " { Lstate = (struct H_el *) tmp;",
5991 " break;",
5992 " } }",
5993 " PROBE++;",
5994 " return (m == 0);",
5995 "}",
5996 "#endif",
5997 "#endif",
5998
5999 "#ifndef BITSTATE",
6000 "void",
6001 "hinit(void)",
6002 "{",
6003 " #ifdef MA",
6004 "#ifdef R_XPT",
6005 " { void r_xpoint(void);",
6006 " r_xpoint();",
6007 " }",
6008 "#else",
6009 " dfa_init((unsigned short) (MA+a_cycles));",
6010 "#if NCORE>1 && !defined(COLLAPSE)",
6011 " if (!readtrail)",
6012 " { void init_HT(unsigned long);",
6013 " init_HT(0L);",
6014 " }",
6015 "#endif",
6016 "#endif",
6017 " #endif",
6018 " #if !defined(MA) || defined(COLLAPSE)",
6019 "#if NCORE>1",
6020 " if (!readtrail)",
6021 " { void init_HT(unsigned long);",
6022 " init_HT((unsigned long) (ONE_L<<ssize)*sizeof(struct H_el *));",
6023 " } else",
6024 "#endif",
6025 " H_tab = (struct H_el **)",
6026 " emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
6027 " #endif",
6028 "}",
6029 "#endif\n",
6030
6031 "#if !defined(BITSTATE) || defined(FULLSTACK)",
6032
6033 "#ifdef DEBUG",
6034 "void",
6035 "dumpstate(int wasnew, char *v, int n, int tag)",
6036 "{ int i;",
6037 "#ifndef SAFETY",
6038 " if (S_A)",
6039 " { printf(\"\tstate tags %%d (%%d::%%d): \",",
6040 " V_A, wasnew, v[0]);",
6041 "#ifdef FULLSTACK",
6042 " printf(\" %%d \", tag);",
6043 "#endif",
6044 " printf(\"\\n\");",
6045 " }",
6046 "#endif",
6047 "#ifdef SDUMP",
6048 "#ifndef NOCOMP",
6049 " printf(\"\t State: \");",
6050 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
6051 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
6052 "#endif",
6053 " printf(\"\\n\tVector: \");",
6054 " for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
6055 " printf(\"\\n\");",
6056 "#endif",
6057 "}",
6058 "#endif",
6059
6060 "#ifdef MA",
6061 "int",
6062 "gstore(char *vin, int nin, uchar pbit)",
6063 "{ int n, i;",
6064 " int ret_val = 1;",
6065 " uchar *v;",
6066 " static uchar Info[MA+1];",
6067 "#ifndef NOCOMP",
6068 " n = compress(vin, nin);",
6069 " v = (uchar *) &comp_now;",
6070 "#else",
6071 " n = nin;",
6072 " v = vin;",
6073 "#endif",
6074 " if (n >= MA)",
6075 " { printf(\"pan: error, MA too small, recompile pan.c\");",
6076 " printf(\" with -DMA=N with N>%%d\\n\", n);",
6077 " Uerror(\"aborting\");",
6078 " }",
6079 " if (n > (int) maxgs)",
6080 " { maxgs = (unsigned int) n;",
6081 " }",
6082 " for (i = 0; i < n; i++)",
6083 " { Info[i] = v[i];",
6084 " }",
6085 " for ( ; i < MA-1; i++)",
6086 " { Info[i] = 0;",
6087 " }",
6088 " Info[MA-1] = pbit;",
6089 " if (a_cycles) /* place _a_t at the end */",
6090 " { Info[MA] = Info[0];",
6091 " Info[0] = 0;",
6092 " }",
6093 "",
6094 "#if NCORE>1 && !defined(SEP_STATE)",
6095 " enter_critical(GLOBAL_LOCK); /* crude, but necessary */",
6096 " /* to make this mode work, also replace emalloc with grab_shared inside store MA routines */",
6097 "#endif",
6098 "",
6099 " if (!dfa_store(Info))",
6100 " { if (pbit == 0",
6101 " && (now._a_t&1)",
6102 " && depth > A_depth)",
6103 " { Info[MA] &= ~(1|16|32); /* _a_t */",
6104 " if (dfa_member(MA))", /* was !dfa_member(MA) */
6105 " { Info[MA-1] = 4; /* off-stack bit */",
6106 " nShadow++;",
6107 " if (!dfa_member(MA-1))",
6108 " { ret_val = 3;",
6109 " #ifdef VERBOSE",
6110 " printf(\"intersected 1st dfs stack\\n\");",
6111 " #endif",
6112 " goto done;",
6113 " } } }",
6114 " ret_val = 0;",
6115 " #ifdef VERBOSE",
6116 " printf(\"new state\\n\");",
6117 " #endif",
6118 " goto done;",
6119 " }",
6120 "#ifdef FULLSTACK",
6121 " if (pbit == 0)",
6122 " { Info[MA-1] = 1; /* proviso bit */",
6123 "#ifndef BFS",
6124 " trpt->proviso = dfa_member(MA-1);",
6125 "#endif",
6126 " Info[MA-1] = 4; /* off-stack bit */",
6127 " if (dfa_member(MA-1))",
6128 " { ret_val = 1; /* off-stack */",
6129 " #ifdef VERBOSE",
6130 " printf(\"old state\\n\");",
6131 " #endif",
6132 " } else",
6133 " { ret_val = 2; /* on-stack */",
6134 " #ifdef VERBOSE",
6135 " printf(\"on-stack\\n\");",
6136 " #endif",
6137 " }",
6138 " goto done;",
6139 " }",
6140 "#endif",
6141 " ret_val = 1;",
6142 "#ifdef VERBOSE",
6143 " printf(\"old state\\n\");",
6144 "#endif",
6145 "done:",
6146 "#if NCORE>1 && !defined(SEP_STATE)",
6147 " leave_critical(GLOBAL_LOCK);",
6148 "#endif",
6149 " return ret_val; /* old state */",
6150 "}",
6151 "#endif",
6152
6153 "#if defined(BITSTATE) && defined(LC)",
6154 "int",
6155 "compact_stack(char *vin, int n)", /* special case of HC4 */
6156 "{ int delta = 0;",
6157 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
6158 "#ifndef SAFETY",
6159 " delta++; /* room for state[0] |= 128 */",
6160 "#endif",
6161 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
6162 " delta += WS;",
6163 " memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
6164 " delta += WS; /* use all available bits */",
6165 " return delta;",
6166 "}",
6167 "#endif",
6168
6169 "int",
6170 "hstore(char *vin, int nin) /* hash table storage */",
6171 "{ struct H_el *ntmp;",
6172 " struct H_el *tmp, *olst = (struct H_el *) 0;",
6173 " char *v; int n, m=0;",
6174 "#ifdef HC",
6175 " uchar rem_a;",
6176 "#endif",
6177 "#ifdef NOCOMP", /* defined by BITSTATE */
6178 "#if defined(BITSTATE) && defined(LC)",
6179 " if (S_Tab == H_tab)",
6180 " { v = (char *) &comp_now;",
6181 " n = compact_stack(vin, nin);",
6182 " } else",
6183 " { v = vin; n = nin;",
6184 " }",
6185 "#else",
6186 " v = vin; n = nin;",
6187 "#endif",
6188 "#else",
6189 " v = (char *) &comp_now;",
6190 " #ifdef HC",
6191 " rem_a = now._a_t;", /* new 5.0 */
6192 " now._a_t = 0;", /* for hashing/state matching to work right */
6193 " #endif",
6194 " n = compress(vin, nin);", /* with HC, this calls s_hash -- but on vin, not on v... */
6195 " #ifdef HC",
6196 " now._a_t = rem_a;", /* new 5.0 */
6197 " #endif",
6198 /* with HC4 -a, compress copies K1 and K2 into v[], leaving v[0] free for the a-bit */
6199 "#ifndef SAFETY",
6200 " if (S_A)",
6201 " { v[0] = 0; /* _a_t */",
6202 "#ifndef NOFAIR",
6203 " if (S_A > NFAIR)",
6204 " for (m = 0; m < NFAIR; m++)",
6205 " v[m+1] = 0; /* _cnt[] */",
6206 "#endif",
6207 " m = 0;",
6208 " }",
6209 " #endif",
6210 "#endif",
6211 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
6212 " s_hash((uchar *)v, n);",
6213 "#endif",
6214 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6215 " enter_critical(CS_ID); /* uses spinlock */",
6216 "#endif",
6217
6218 " tmp = H_tab[j1];",
6219 " if (!tmp)",
6220 " { tmp = grab_state(n);",
6221 "#if NCORE>1",
6222 " if (!tmp)",
6223 " { /* if we get here -- we've already issued a warning */",
6224 " /* but we want to allow the normal distributed termination */",
6225 " /* to collect the stats on all cpus in the wrapup */",
6226 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6227 " leave_critical(CS_ID);",
6228 " #endif",
6229 " return 1; /* allow normal termination */",
6230 " }",
6231 "#endif",
6232 " H_tab[j1] = tmp;",
6233 " } else",
6234 " { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
6235 " { /* skip the _a_t and the _cnt bytes */",
6236 "#ifdef COLLAPSE",
6237 " if (tmp->ln != 0)",
6238 " { if (!tmp->nxt) goto Append;",
6239 " continue;",
6240 " }",
6241 "#endif",
6242 " m = memcmp(((char *)&(tmp->state)) + S_A, ",
6243 " v + S_A, n - S_A);",
6244 " if (m == 0) {",
6245 "#ifdef SAFETY",
6246 "#define wasnew 0",
6247 "#else",
6248 " int wasnew = 0;",
6249 "#endif",
6250
6251 "#ifndef SAFETY",
6252 "#ifndef NOCOMP",
6253 " if (S_A)",
6254 " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
6255 " { wasnew = 1; nShadow++;",
6256 " ((char *)&(tmp->state))[0] |= V_A;",
6257 " }",
6258 "#ifndef NOFAIR",
6259 " if (S_A > NFAIR)",
6260 " { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */",
6261 " unsigned ci, bp; /* index, bit pos */",
6262 " ci = (now._cnt[now._a_t&1] / 8);",
6263 " bp = (now._cnt[now._a_t&1] - 8*ci);",
6264 " if (now._a_t&1) /* use tail-bits in _cnt */",
6265 " { ci = (NFAIR - 1) - ci;",
6266 " bp = 7 - bp; /* bp = 0..7 */",
6267 " }",
6268 " ci++; /* skip over _a_t */",
6269 " bp = 1 << bp; /* the bit mask */",
6270 " if ((((char *)&(tmp->state))[ci] & bp)==0)",
6271 " { if (!wasnew)",
6272 " { wasnew = 1;",
6273 " nShadow++;",
6274 " }",
6275 " ((char *)&(tmp->state))[ci] |= bp;",
6276 " }",
6277 " }",
6278 " /* else: wasnew == 0, i.e., old state */",
6279 "#endif",
6280 " }",
6281 "#endif",
6282 "#endif",
6283
6284 "#if NCORE>1",
6285 " Lstate = (struct H_el *) tmp;",
6286 "#endif",
6287
6288 "#ifdef FULLSTACK",
6289 "#ifndef SAFETY", /* or else wasnew == 0 */
6290 " if (wasnew)",
6291 " { Lstate = (struct H_el *) tmp;",
6292 " tmp->tagged |= V_A;",
6293 " if ((now._a_t&1)",
6294 " && (tmp->tagged&A_V)",
6295 " && depth > A_depth)",
6296 " {",
6297 "intersect:",
6298 "#ifdef CHECK",
6299 "#if NCORE>1",
6300 " printf(\"cpu%%d: \", core_id);",
6301 "#endif",
6302 " printf(\"1st dfs-stack intersected on state %%d+\\n\",",
6303 " (int) tmp->st_id);",
6304 "#endif",
6305
6306 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6307 " leave_critical(CS_ID);",
6308 "#endif",
6309
6310 " return 3;",
6311 " }",
6312 "#ifdef CHECK",
6313 "#if NCORE>1",
6314 " printf(\"cpu%%d: \", core_id);",
6315 "#endif",
6316 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
6317 "#endif",
6318 "#ifdef DEBUG",
6319 " dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
6320 "#endif",
6321 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6322 " leave_critical(CS_ID);",
6323 "#endif",
6324 " return 0;",
6325 " } else",
6326 "#endif",
6327 " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
6328 " { Lstate = (struct H_el *) tmp;",
6329 "#ifndef SAFETY",
6330 " /* already on current dfs stack */",
6331 " /* but may also be on 1st dfs stack */",
6332 " if ((now._a_t&1)",
6333 " && (tmp->tagged&A_V)",
6334
6335 " && depth > A_depth",
6336 /* new (Zhang's example) */
6337 "#ifndef NOFAIR",
6338 " && (!fairness || now._cnt[1] <= 1)",
6339 "#endif",
6340 " )",
6341
6342 " goto intersect;",
6343 "#endif",
6344 "#ifdef CHECK",
6345 "#if NCORE>1",
6346 " printf(\"cpu%%d: \", core_id);",
6347 "#endif",
6348 " printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
6349 "#endif",
6350 "#ifdef DEBUG",
6351 " dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
6352 "#endif",
6353 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6354 " leave_critical(CS_ID);",
6355 "#endif",
6356 " return 2; /* match on stack */",
6357 " }",
6358 "#else",
6359 " if (wasnew)",
6360 " {",
6361 "#ifdef CHECK",
6362 "#if NCORE>1",
6363 " printf(\"cpu%%d: \", core_id);",
6364 "#endif",
6365 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
6366 "#endif",
6367 "#ifdef DEBUG",
6368 " dumpstate(1, (char *)&(tmp->state), n, 0);",
6369 "#endif",
6370 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6371 " leave_critical(CS_ID);",
6372 "#endif",
6373 " return 0;",
6374 " }",
6375 "#endif",
6376 "#ifdef CHECK",
6377 "#if NCORE>1",
6378 " printf(\"cpu%%d: \", core_id);",
6379 "#endif",
6380 " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
6381 "#endif",
6382 "#ifdef DEBUG",
6383 " dumpstate(0, (char *)&(tmp->state), n, 0);",
6384 "#endif",
6385 "#ifdef REACH",
6386 " if (tmp->D > depth)",
6387 " { tmp->D = depth;",
6388 "#ifdef CHECK",
6389 "#if NCORE>1",
6390 " printf(\"cpu%%d: \", core_id);",
6391 "#endif",
6392 " printf(\"\t\tReVisiting (from smaller depth)\\n\");",
6393 "#endif",
6394 " nstates--;",
6395 #if 0
6396 possible variation of iterative search for shortest counter-example (pan -i
6397 and pan -I) suggested by Pierre Moro (for safety properties):
6398 state revisits on shorter depths do not start until after
6399 the first counter-example is found. this assumes that the max search
6400 depth is set large enough that a first (possibly long) counter-example
6401 can be found
6402 if set too short, this variant can miss the counter-example, even if
6403 it would otherwise be shorter than the depth-limit.
6404 (p.m. unsure if this preserves the guarantee of finding the
6405 shortest counter-example - so not enabled yet)
6406 " if (errors > 0 && iterative)", /* Moro */
6407 #endif
6408 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6409 " leave_critical(CS_ID);",
6410 "#endif",
6411 " return 0;",
6412 " }",
6413 "#endif",
6414 "#if (defined(BFS) && defined(Q_PROVISO)) || NCORE>1",
6415 " Lstate = (struct H_el *) tmp;",
6416 "#endif",
6417 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6418 " leave_critical(CS_ID);",
6419 "#endif",
6420 " return 1; /* match outside stack */",
6421 " } else if (m < 0)",
6422 " { /* insert state before tmp */",
6423 " ntmp = grab_state(n);",
6424 "#if NCORE>1",
6425 " if (!ntmp)",
6426 " {",
6427 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6428 " leave_critical(CS_ID);",
6429 " #endif",
6430 " return 1; /* allow normal termination */",
6431 " }",
6432 "#endif",
6433 " ntmp->nxt = tmp;",
6434 " if (!olst)",
6435 " H_tab[j1] = ntmp;",
6436 " else",
6437 " olst->nxt = ntmp;",
6438 " tmp = ntmp;",
6439 " break;",
6440 " } else if (!tmp->nxt)",
6441 " { /* append after tmp */",
6442 "#ifdef COLLAPSE",
6443 "Append:",
6444 "#endif",
6445 " tmp->nxt = grab_state(n);",
6446 "#if NCORE>1",
6447 " if (!tmp->nxt)",
6448 " {",
6449 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6450 " leave_critical(CS_ID);",
6451 " #endif",
6452 " return 1; /* allow normal termination */",
6453 " }",
6454 "#endif",
6455 " tmp = tmp->nxt;",
6456 " break;",
6457 " } }",
6458 " }",
6459 "#ifdef CHECK",
6460 " tmp->st_id = (unsigned) nstates;",
6461 "#if NCORE>1",
6462 " printf(\"cpu%%d: \", core_id);",
6463 "#endif",
6464 "#ifdef BITSTATE",
6465 " printf(\" Push state %%d\\n\", ((int) nstates) - 1);",
6466 "#else",
6467 " printf(\" New state %%d\\n\", (int) nstates);",
6468 "#endif",
6469 "#endif",
6470 "#if !defined(SAFETY) || defined(REACH)",
6471 " tmp->D = depth;",
6472 "#endif",
6473 "#ifndef SAFETY",
6474 "#ifndef NOCOMP",
6475 " if (S_A)",
6476 " { v[0] = V_A;",
6477 "#ifndef NOFAIR",
6478 " if (S_A > NFAIR)",
6479 " { unsigned ci, bp; /* as above */",
6480 " ci = (now._cnt[now._a_t&1] / 8);",
6481 " bp = (now._cnt[now._a_t&1] - 8*ci);",
6482 " if (now._a_t&1)",
6483 " { ci = (NFAIR - 1) - ci;",
6484 " bp = 7 - bp; /* bp = 0..7 */",
6485 " }",
6486 " v[1+ci] = 1 << bp;",
6487 " }",
6488 "#endif",
6489 " }",
6490 "#endif",
6491 "#endif",
6492 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
6493 " tmp->m_K1 = K1;",
6494 "#endif",
6495 " memcpy(((char *)&(tmp->state)), v, n);",
6496 "#ifdef FULLSTACK",
6497 " tmp->tagged = (S_A)?V_A:(depth+1);",
6498 "#ifdef DEBUG",
6499 " dumpstate(-1, v, n, tmp->tagged);",
6500 "#endif",
6501 " Lstate = (struct H_el *) tmp;",
6502 "#else",
6503 " #ifdef DEBUG",
6504 " dumpstate(-1, v, n, 0);",
6505 " #endif",
6506 " #if NCORE>1",
6507 " Lstate = (struct H_el *) tmp;",
6508 " #endif",
6509 "#endif",
6510
6511 "/* #if NCORE>1 && !defined(SEP_STATE) */",
6512 "#if NCORE>1",
6513 " #ifdef V_PROVISO",
6514 " tmp->cpu_id = core_id;",
6515 " #endif",
6516 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6517 " leave_critical(CS_ID);",
6518 " #endif",
6519 "#endif",
6520
6521 " return 0;",
6522 "}",
6523 "#endif",
6524 "#include TRANSITIONS",
6525 "void",
6526 "do_reach(void)",
6527 "{",
6528 0,
6529 };
LTTng 2.x Viewer (LTTV)
This page took 0.231835 seconds and 4 git commands to generate.