1 /***** spin: pangen1.h *****/
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 */
13 static char *Code2a
[] = { /* the tail of procedure run() */
14 "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
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\");",
29 " UnBlock; /* disable rendez-vous */",
33 " { udmem *= 1024L*1024L;",
36 " { void init_SS(unsigned long);",
37 " init_SS((unsigned long) udmem);",
40 " SS = (uchar *) emalloc(udmem);",
41 " bstore = bstore_mod;",
45 " { void init_SS(unsigned long);",
46 " init_SS(ONE_L<<(ssize-3));",
49 " SS = (uchar *) emalloc(ONE_L<<(ssize-3));",
51 "#else", /* if not BITSTATE */
54 "#if defined(FULLSTACK) && defined(BITSTATE)",
57 "#if defined(CNTRSTACK) && !defined(BFS)",
58 " LL = (uchar *) emalloc(ONE_L<<(ssize-3));",
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));",
66 " write(svfd, (uchar *) &vprefix, sizeof(int));",
69 " Addproc(VERI); /* never - pid = 0 */",
71 " active_procs(); /* started after never */",
73 " now._event = start_event;",
74 " reached[EVENT_TRACE][start_event] = 1;",
85 " if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
86 " { printf(\"Run %%d:\\n\", HASH_NR);",
89 " memset(SS, 0, ONE_L<<(ssize-3));",
91 " memset(LL, 0, ONE_L<<(ssize-3));",
94 " memset((uchar *) S_Tab, 0, ",
95 " maxdepth*sizeof(struct H_el *));",
97 " nstates=nlinks=truncs=truncs2=ngrabs = 0;",
98 " nlost=nShadow=hcmp = 0;",
100 " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
105 "#ifdef HAS_PROVIDED",
106 "int provided(int, uchar, int, Trans *);",
110 "#define GLOBAL_LOCK (0)",
112 "#define CS_N (256*NCORE)", /* must be a power of 2 */
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 */
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 */
131 "void e_critical(int);",
132 "void x_critical(int);",
135 " #define enter_critical(w) e_critical(w)",
136 " #define leave_critical(w) x_critical(w)",
139 " #define enter_critical(w) { if (w < 1+NCORE) e_critical(w); }",
140 " #define leave_critical(w) { if (w < 1+NCORE) x_critical(w); }",
142 " #define enter_critical(w) { if (w < 3+NCORE) e_critical(w); }",
143 " #define leave_critical(w) { if (w < 3+NCORE) x_critical(w); }",
148 "cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */
150 " enter_critical(GLOBAL_LOCK); /* printing */",
151 " printf(\"cpu%%d: \", core_id);",
153 " va_start(args, fmt);",
154 " vprintf(fmt, args);",
157 " leave_critical(GLOBAL_LOCK);",
162 "cpu_printf(const char *fmt, ...)",
164 " va_start(args, fmt);",
165 " vprintf(fmt, args);",
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",
187 " va_start(args, fmt);",
188 " vprintf(fmt, args);",
195 " va_start(args, fmt);",
196 " vprintf(fmt, args);",
202 "extern void printm(int);",
205 "#define getframe(i) &trail[i];",
207 "static long HHH, DDD, hiwater;",
208 "static long CNT1, CNT2;",
209 "static int stackwrite;",
210 "static int stackread;",
211 "static Trail frameptr;",
215 " if (CNT1 == CNT2)",
216 " return &trail[d];",
218 " if (d >= (CNT1-CNT2)*DDD)",
219 " return &trail[d - (CNT1-CNT2)*DDD];",
222 " && (stackread = open(stackfile, 0)) < 0)",
223 " { printf(\"getframe: cannot open %%s\\n\", stackfile);",
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\");",
231 " return &frameptr;",
235 "#if !defined(SAFETY) && !defined(BITSTATE)",
236 "#if !defined(FULLSTACK) || defined(MA)",
237 "#define depth_of(x) A_depth /* an estimate */",
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)",
247 " printf(\"pan: cannot happen, depth_of\\n\");",
248 " return depthfound;",
254 "extern void cleanup_shm(int);",
255 "volatile unsigned int *search_terminated; /* to signal early termination */",
257 * Meaning of bitflags in search_terminated:
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
268 * Flags 8|32|128|256 indicate abnormal termination
270 * The flags are checked in 4 functions in the code:
272 * someone_crashed() (proxy and pan version)
278 "{ void stop_timer(void);",
280 " { printf(\"--end of output--\\n\");",
283 " if (search_terminated != NULL)",
284 " { *search_terminated |= 1; /* pan_exit */",
287 " { void dsk_stats(void);",
291 " if (!state_tables && !readtrail)",
292 " { cleanup_shm(1);",
305 "transmognify(char *s)",
307 " static char buf[2][2048];",
308 " int i, toggle = 0;",
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;",
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)",
327 " strcat(buf[1-toggle], code_lookup[i].t);",
330 " strcat(buf[1-toggle], w);",
331 " toggle = 1 - toggle;",
333 " buf[toggle][2047] = '\\0';",
334 " return buf[toggle];",
337 "char * transmognify(char *s) { return s; }",
342 "add_src_txt(int ot, int tt)",
346 " for (t = trans[ot][tt]; t; t = t->nxt)",
347 " { printf(\"\\t\\t\");",
349 " q = transmognify(t->tp);",
350 " for ( ; q && *q; q++)",
352 " printf(\"\\\\n\");",
360 "{ static int wrap_in_progress = 0;",
364 " if (wrap_in_progress++) return;",
366 " printf(\"spin: trail ends after %%ld steps\\n\", depth);",
367 " if (onlyproc >= 0)",
368 " { if (onlyproc >= now._nr_pr) { pan_exit(0); }",
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]);",
379 " printf(\" (state %%2d)\", z->_p);",
380 " if (!stopstate[z->_t][z->_p])",
381 " printf(\" (invalid end state)\");",
383 " add_src_txt(z->_t, z->_p);",
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]);",
398 " printf(\" (state %%2d)\", z->_p);",
399 " if (!stopstate[z->_t][z->_p])",
400 " printf(\" (invalid end state)\");",
402 " add_src_txt(z->_t, z->_p);",
405 " for (II = 0; II < now._nr_pr; II++)",
406 " { z = (P0 *)pptr(II);",
407 " c_locals(II, z->_t);",
417 " char fnm[512], *q;",
418 " char MyFile[512];", /* avoid using a non-writable string */
419 " char MySuffix[16];",
421 " int candidate_files;",
423 " if (trailfilename != NULL)",
424 " { fd = fopen(trailfilename, \"r\");",
426 " { printf(\"pan: cannot find %%s\\n\", trailfilename);",
433 " candidate_files = 0;",
434 " tprefix = \"trail\";",
435 " strcpy(MyFile, TrailFile);",
436 " do { /* see if there's more than one possible trailfile */",
438 " { sprintf(fnm, \"%%s%%d.%%s\",",
439 " MyFile, whichtrail, tprefix);",
440 " fd = fopen(fnm, \"r\");",
442 " { candidate_files++;",
443 " if (verbose==100)",
444 " printf(\"trail%%d: %%s\\n\",",
445 " candidate_files, fnm);",
448 " if ((q = strchr(MyFile, \'.\')) != NULL)",
449 " { *q = \'\\0\';", /* e.g., strip .pml */
450 " sprintf(fnm, \"%%s%%d.%%s\",",
451 " MyFile, whichtrail, tprefix);",
453 " fd = fopen(fnm, \"r\");",
455 " { candidate_files++;",
456 " if (verbose==100)",
457 " printf(\"trail%%d: %%s\\n\",",
458 " candidate_files, fnm);",
462 " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
463 " fd = fopen(fnm, \"r\");",
465 " { candidate_files++;",
466 " if (verbose==100)",
467 " printf(\"trail%%d: %%s\\n\",",
468 " candidate_files, fnm);",
471 " if ((q = strchr(MyFile, \'.\')) != NULL)",
472 " { *q = \'\\0\';", /* e.g., strip .pml */
473 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
475 " fd = fopen(fnm, \"r\");",
477 " { candidate_files++;",
478 " if (verbose==100)",
479 " printf(\"trail%%d: %%s\\n\",",
480 " candidate_files, fnm);",
483 " tprefix = MySuffix;",
484 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
485 " } while (try_core <= NCORE);",
487 " if (candidate_files != 1)",
488 " { if (verbose != 100)",
489 " { printf(\"error: there are %%d trail files:\\n\",",
490 " candidate_files);",
494 " { printf(\"pan: rm or mv all except one\\n\");",
499 " strcpy(MyFile, TrailFile); /* restore */",
500 " tprefix = \"trail\";",
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);",
510 " fd = fopen(fnm, \"r\");",
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);",
519 " fd = fopen(fnm, \"r\");",
522 " { if (try_core < NCORE)",
523 " { tprefix = MySuffix;",
524 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
527 " printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
531 "#if NCORE>1 && defined(SEP_STATE)",
532 " { void set_root(void); /* for partial traces from local root */",
539 "uchar do_transit(Trans *, short);",
545 " int i, t_id, lastnever=-1; short II;",
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\");",
555 " if (i > now._nr_pr)",
556 " { printf(\"pan: Error, proc %%d invalid pid \", i);",
557 " printf(\"transition %%d\\n\", t_id);",
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)",
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);",
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); */",
584 " q = transmognify(t->tp);",
585 " if (gui) simvals[0] = \'\\0\';",
588 " trpt->tau |= 1;", /* timeout always possible */
589 " if (!do_transit(t, II))",
590 " { if (onlyproc >= 0 && II != onlyproc)",
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\");",
597 " if (onlyproc >= 0 && II != onlyproc)",
601 " { printf(\"%%3ld: proc %%2d (%%s) \", depth, II, procname[z->_t]);",
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);",
610 " printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",",
611 " z->_p, t_id, t->forw, q?q:\"\");",
614 " for (i = 0; i < now._nr_pr; i++)",
615 " { c_locals(i, ((P0 *)pptr(i))->_t);",
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]);",
626 " if (!src_all[i].src)",
627 " printf(\"MSC: ~R %%d\\n\", z->_p);",
629 " lastnever = z->_p;",
632 " if (strcmp(procname[z->_t], \":np_:\") != 0)",
634 "sameas: if (no_rck) goto moveon;",
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);",
651 " printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
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);",
661 " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
662 " /* printf(\"\\n\"); */",
664 "moveon: z->_p = t->st;",
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;",
681 "void check_claim(int);",
684 "#if !defined(HASH64) && !defined(HASH32)",
687 "#if defined(HASH32) && defined(SAFETY) && !defined(SFH) && !defined(SPACE)",
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 */",
696 "#if NCORE>1 && !defined(GLOB_HEAP)",
697 " #define SEP_HEAP /* version 5.1.2 */",
703 "bstore_mod(char *v, int n) /* hasharray size not a power of two */",
704 "{ unsigned long x, y;",
705 " unsigned int i = 1;",
707 " d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
708 " x = K1; y = j3;", /* was K2 before 5.1.1 */
710 " { if (!(SS[x%%udmem]&(1<<y))) break;", /* take the hit in speed */
713 " printf(\"Old bitstate\\n\");",
717 " x = (x + K2 + i);", /* no mask, using mod - was K1 before 5.1.1 */
718 " y = (y + j4) & 7;",
722 " if (rand()%%100 > RANDSTOR) return 0;",
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;",
732 " printf(\"New bitstate\\n\");",
741 "bstore_reg(char *v, int n) /* extended hashing, Peter Dillinger, 2004 */",
742 "{ unsigned long x, y;",
743 " unsigned int i = 1;",
745 " d_hash((uchar *) v, n); /* sets j1-j4 */",
748 " { if (!(SS[x]&(1<<y))) break;", /* at least one bit not set */
751 " printf(\"Old bitstate\\n\");",
755 " x = (x + j1 + i) & nmask;",
756 " y = (y + j4) & 7;",
760 " if (rand()%%100 > RANDSTOR) return 0;",
763 " { SS[x] |= (1<<y);",
764 " if (i == hfns) break;", /* done */
765 " x = (x + j1 + i) & nmask;",
766 " y = (y + j4) & 7;",
770 " printf(\"New bitstate\\n\");",
777 "#endif", /* BITSTATE */
778 "unsigned long TMODE = 0666; /* file permission bits for trail files */",
781 "char snap[64], fnm[512];",
787 " char MyFile[512];",
788 " int w_flags = O_CREAT|O_WRONLY|O_TRUNC;",
790 " if (exclusive == 1 && iterative == 0)",
791 " { w_flags |= O_EXCL;",
794 " q = strrchr(TrailFile, \'/\');",
795 " if (q == NULL) q = TrailFile; else q++;",
796 " strcpy(MyFile, q); /* TrailFile is not a writable string */",
798 " if (iterative == 0 && Nr_Trails++ > 0)",
799 " { sprintf(fnm, \"%%s%%d.%%s\",",
800 " MyFile, Nr_Trails-1, tprefix);",
804 " sprintf(fnm, \"%%s%%d.%%s\", MyFile, getpid(), tprefix);",
806 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
810 " if ((fd = open(fnm, w_flags, TMODE)) < 0)",
812 " if ((fd = creat(fnm, TMODE)) < 0)",
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);",
820 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
823 " fd = open(fnm, w_flags, TMODE);",
825 " fd = creat(fnm, TMODE);",
829 " { printf(\"pan: cannot create %%s\\n\", fnm);",
830 " perror(\"cause\");",
833 "#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))",
834 " void write_root(void); ",
837 " printf(\"pan: wrote %%s\\n\", fnm);",
844 "#define FREQ (1000000)",
849 static char *Code2b
[] = { /* breadth-first search option */
852 "#ifndef INLINE_REV",
853 "#define INLINE_REV",
856 "typedef struct SV_Hold {",
859 " struct SV_Hold *nxt;",
862 "typedef struct EV_Hold {",
863 " char *sv;", /* Mask */
864 " int sz;", /* vsize */
870 " struct EV_Hold *nxt;",
873 "typedef struct BFS_Trail {",
878 " struct H_el *lstate;",
881 " struct BFS_Trail *nxt;",
884 "BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
886 "SV_Hold *svhold, *svfree;",
890 " #define BFS_LIMIT 100000",
892 "#ifndef BFS_DSK_LIMIT",
893 " #define BFS_DSK_LIMIT 1000000",
896 "#if defined(WIN32) || defined(WIN64)",
897 " #define RFLAGS (O_RDONLY|O_BINARY)",
898 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
900 " #define RFLAGS (O_RDONLY)",
901 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)",
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;",
911 "uchar do_reverse(Trans *, short, uchar);",
912 "void snapshot(void);",
916 "{ SV_Hold *h = (SV_Hold *) 0, *oh;",
918 " oh = (SV_Hold *) 0;",
919 " for (h = svfree; h; oh = h, h = h->nxt)",
920 " { if (n == h->sz)",
924 " oh->nxt = h->nxt;",
925 " h->nxt = (SV_Hold *) 0;",
929 " { h = (SV_Hold *) 0;",
932 " /* else continue */",
936 " { h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
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);",
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\");",
953 " printf(\"pan: created disk file %%s\\n\", dsk_nm);",
955 " if (write(bfs_dsk_write, (char *) &now, n) != n)",
956 " { Uerror(\"aborting -- disk write failed (disk full?)\");",
958 " return h; /* no memcpy */",
960 " bfs_size_limit++;",
962 " h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
965 " memcpy((char *)h->sv, (char *)&now, n);",
972 " static EV_Hold *kept = (EV_Hold *) 0;",
974 " for (h = kept; h; h = h->nxt)",
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)",
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)",
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))",
990 " { h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
992 " h->nrpr = now._nr_pr;",
993 " h->nrqs = now._nr_qs;",
995 " h->sv = (char *) emalloc(n * sizeof(char));",
996 " memcpy((char *) h->sv, (char *) Mask, n);",
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));",
1005 " h->po = (char *) emalloc(now._nr_pr * sizeof(short));",
1006 " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
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));",
1016 " h->qo = (char *) emalloc(now._nr_qs * sizeof(short));",
1017 " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
1028 "freesv(SV_Hold *p)",
1029 "{ SV_Hold *h, *oh;",
1031 " oh = (SV_Hold *) 0;",
1032 " for (h = svfree; h; oh = h, h = h->nxt)",
1033 " if (h->sz >= p->sz)",
1037 " { p->nxt = svfree;",
1046 "get_bfs_frame(void)",
1051 " bfs_free = bfs_free->nxt;",
1052 " t->nxt = (BFS_Trail *) 0;",
1054 " { t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
1056 " t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
1061 "push_bfs(Trail *f, int d)",
1064 " t = get_bfs_frame();",
1065 " memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
1066 " t->frame->o_tt = d; /* depth */",
1069 " t->onow = getsv(vsize);",
1070 " t->omask = getsv_mask(vsize);",
1071 "#if defined(FULLSTACK) && defined(Q_PROVISO)",
1072 " t->lstate = Lstate;",
1075 " { bfs_bot = bfs_trail = t;",
1077 " { bfs_bot->nxt = t;",
1081 " printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
1090 " return (Trail *) 0;",
1093 " bfs_trail = t->nxt;",
1095 " bfs_bot = (BFS_Trail *) 0;",
1096 "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
1097 " if (t->lstate) t->lstate->tagged = 0;",
1100 " t->nxt = bfs_free;",
1103 " vsize = t->onow->sz;",
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;",
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\");",
1122 " if (read(bfs_dsk_read, (char *) &now, vsize) != vsize)",
1123 " { Uerror(\"bad bfs disk file read\");",
1126 " if (now._vsz != vsize)",
1127 " { Uerror(\"disk read vsz mismatch\");",
1132 " memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
1133 " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
1135 " if (now._nr_pr > 0)",
1136 "#if VECTORSZ>32000",
1137 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
1139 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
1141 " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
1143 " if (now._nr_qs > 0)",
1144 "#if VECTORSZ>32000",
1145 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
1147 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
1149 " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
1153 " if (t->onow->sv != (State *) 0)",
1155 " freesv(t->onow); /* omask not freed */",
1157 " printf(\"POP %%u (%%d)\\n\", t->frame, t->frame->o_tt);",
1159 " return t->frame;",
1163 "store_state(Trail *ntrpt, int shortcut, short oboq)",
1166 " Trans *t2 = (Trans *) 0;",
1167 " uchar ot; int tt, E_state;",
1168 " uchar o_opm = trpt->o_pm, *othis = this;",
1173 " printf(\"claim: shortcut\\n\");",
1175 " goto store_it; /* no claim move */",
1178 " this = (((uchar *)&now)+proc_offset[0]); /* 0 = never claim */",
1179 " trpt->o_pm = 0;", /* to interpret else in never claim */
1181 " tt = (int) ((P0 *)this)->_p;",
1182 " ot = (uchar) ((P0 *)this)->_t;",
1184 "#ifdef HAS_UNLESS",
1187 " for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
1189 "#ifdef HAS_UNLESS",
1191 " && E_state != t2->e_trans)",
1194 " if (do_transit(t2, 0))",
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);",
1201 "#ifdef HAS_UNLESS",
1202 " E_state = t2->e_trans;",
1205 " { ((P0 *)this)->_p = t2->st;",
1206 " reached[ot][t2->st] = 1;",
1208 " check_claim(t2->st);",
1211 " if (now._nr_pr == 0) /* claim terminated */",
1212 " uerror(\"end state in claim reached\");",
1215 " peg[t2->forw]++;",
1217 " trpt->o_pm |= 1;",
1218 " if (t2->atom&2)", /* atomic in claim */
1219 " Uerror(\"atomic in claim not supported in BFS mode\");",
1222 "#endif", /* VERI */
1225 " if (!bstore((char *)&now, vsize))",
1228 " if (!gstore((char *)&now, vsize, 0))",
1230 " if (!hstore((char *)&now, vsize))",
1233 " { static long sdone = (long) 0; long ndone;",
1236 " trpt->tau |= 64;", /* succ definitely outside stack */
1238 " ndone = (unsigned long) (nstates/((double) FREQ));",
1239 " if (ndone != sdone && mreached%%10 != 0)",
1242 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
1243 " if (nstates > ((double)(1<<(ssize+1))))",
1244 " { void resize_hashtable(void);",
1245 " resize_hashtable();",
1252 " else if (oboq != -1)",
1254 " x = (Trail *) trpt->ostate; /* pre-rv state */",
1255 " if (x) x->o_pm |= 4; /* mark success */",
1258 " push_bfs(ntrpt, trpt->o_tt+1);",
1262 "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
1263 "#if !defined(BITSTATE)",
1264 " if (Lstate && Lstate->tagged) trpt->tau |= 64;",
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 */",
1278 " ((P0 *)this)->_p = tt; /* reset claim */",
1280 " do_reverse(t2, 0, 0);",
1285 " trpt->o_pm = o_opm;",
1289 "Trail *ntrpt;", /* 4.2.8 */
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;",
1299 " ntrpt = (Trail *) emalloc(sizeof(Trail));",
1300 " trpt->ostate = (struct H_el *) 0;",
1303 " trpt->o_tt = -1;",
1304 " store_state(ntrpt, 0, oboq); /* initial state */",
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]));",
1311 " if (trpt->o_pm & 4)",
1314 " printf(\"Revisit of atomic not needed (%%d)\\n\",",
1315 " trpt->o_pm);", /* at least 1 rv succeeded */
1322 " if (trpt->o_pm == 8)",
1324 " if (trpt->tau&8)",
1327 " printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
1328 " trpt->o_pm, trpt->tau);",
1330 " trpt->tau &= ~8;",
1333 " else if (trpt->tau&32)", /* was a preselected move */
1336 " printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
1337 " trpt->o_pm, trpt->tau);",
1339 " trpt->tau &= ~32;",
1340 " nps = 1; /* no preselection in repeat */",
1344 " trpt->o_pm &= ~(4|8);",
1345 " if (trpt->o_tt > mreached)",
1346 " { mreached = trpt->o_tt;",
1347 " if (mreached%%10 == 0)",
1350 " depth = trpt->o_tt;",
1352 " if (depth >= maxdepth)",
1357 " { x = (Trail *) trpt->ostate;",
1358 " if (x) x->o_pm |= 4; /* not failing */",
1364 " printf(\"error: max search depth too small\\n\");",
1367 " uerror(\"depth limit reached\");",
1373 " if (boq == -1 && !(trpt->tau&8) && nps == 0)",
1374 " for (II = now._nr_pr-1; II >= BASE; II -= 1)",
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)",
1383 " if (!q_cond(II, t))",
1388 " trpt->tau |= 32; /* preselect marker */",
1390 " printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
1391 " depth, II, trpt->tau);",
1395 " trpt->tau &= ~32;", /* not preselected */
1399 " if (trpt->tau&8) /* atomic */",
1400 " { From = To = (short ) trpt->pr;",
1403 " { From = now._nr_pr-1;",
1408 " for (II = From; II >= To; II -= 1)",
1410 " this = (((uchar *)&now)+proc_offset[II]);",
1411 " tt = (int) ((P0 *)this)->_p;",
1412 " ot = (uchar) ((P0 *)this)->_t;",
1414 " /* no rendezvous with same proc */",
1415 " if (boq != -1 && trpt->pr == II) continue;",
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;",
1423 "#ifdef HAS_PROVIDED",
1424 " if (!provided(II, ot, tt, t)) continue;",
1426 "#ifdef HAS_UNLESS",
1429 " for (t = trans[ot][tt]; t; t = t->nxt)",
1431 "#ifdef HAS_UNLESS",
1433 " && E_state != t->e_trans)",
1440 " if (!(_m = do_transit(t, II)))",
1443 " trpt->o_pm |= 1; /* we moved */",
1444 " (trpt+1)->o_m = _m; /* for unsend */",
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",
1457 " printf(\" (escapes to state %%d)\", t->st);",
1459 " printf(\" %%saccepting [tau=%%d]\\n\",",
1460 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
1462 "#ifdef HAS_UNLESS",
1463 " E_state = t->e_trans;",
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\");",
1472 " if (t->st > 0) ((P0 *)this)->_p = t->st;",
1474 " /* ptr to pred: */ ntrpt->ostate = (struct H_el *) otrpt;",
1476 " if (boq == -1 && (t->atom&2)) /* atomic */",
1477 " ntrpt->tau = 8; /* record for next move */",
1481 " store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
1482 "#ifdef EVENT_TRACE",
1483 " now._event = trpt->o_event;",
1486 " /* undo move and continue */",
1487 " trpt++; /* this is where ovals and ipt are set */",
1488 " do_reverse(t, II, _m); /* restore now. */",
1492 " enter_critical(GLOBAL_LOCK); /* in verbose mode only */",
1493 " printf(\"cpu%%d: \", core_id);",
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);",
1504 " leave_critical(GLOBAL_LOCK);",
1507 " reached[ot][t->st] = 1;",
1508 " reached[ot][tt] = 1;",
1510 " ((P0 *)this)->_p = tt;",
1515 " /* preselected - no succ definitely outside stack */",
1516 " if ((trpt->tau&32) && !(trpt->tau&64))",
1517 " { From = now._nr_pr-1; To = BASE;",
1519 " cpu_printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
1520 " depth, II+1, (int) _n, trpt->tau);",
1522 " _n = 0; trpt->tau &= ~32;",
1527 " trpt->tau &= ~(32|64);",
1533 " printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
1534 " depth, II, trpt->tau, boq, now._nr_pr);",
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]);",
1544 " printf(\"\\treset state of %%d from %%d to %%d\\n\",",
1545 " otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
1547 " ((P0 *)this)->_p = otrpt->st;",
1548 " unsend(boq); /* retract rv offer */",
1551 " push_bfs(x, x->o_tt);",
1553 " printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
1557 " else printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
1559 " } else if (now._nr_pr > 0)",
1561 " if ((trpt->tau&8)) /* atomic */",
1562 " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */",
1564 " printf(\"%%3d: atomic step proc %%d blocks\\n\",",
1570 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
1571 " { trpt->tau |= 1;",
1573 " printf(\"%%d: timeout\\n\", depth);",
1578 " if (!noends && !a_cycles && !endstate())",
1579 " uerror(\"invalid end state\");",
1585 "putter(Trail *trpt, int fd)",
1588 " if (!trpt) return;",
1590 " if (trpt != (Trail *) trpt->ostate)",
1591 " putter((Trail *) trpt->ostate, fd);",
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);",
1604 "nuerror(char *str)",
1605 "{ int fd = make_trail();",
1608 " if (fd < 0) return;",
1610 " sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
1611 " write(fd, snap, strlen(snap));",
1614 " sprintf(snap, \"-4:-4:-4\\n\");",
1615 " write(fd, snap, strlen(snap));",
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);",
1628 " if (errors >= upto && upto != 0)",
1636 static char *Code2d
[] = {
1637 "clock_t start_time;",
1639 "clock_t crash_stamp;",
1641 "#if !defined(WIN32) && !defined(WIN64)",
1642 "struct tms start_tm;",
1646 "start_timer(void)",
1648 "#if defined(WIN32) || defined(WIN64)",
1649 " start_time = clock();",
1651 " start_time = times(&start_tm);",
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));",
1664 " stop_time = clock();",
1665 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
1667 " if (readtrail || delta_time < 0.00) return;",
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);",
1674 " { void check_overkill(void);",
1675 " check_overkill();",
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);",
1682 " { printf(\"pan: avg transition delay %%.5g usec\\n\",",
1683 " delta_time/(nstates+truncs));",
1690 "double t_alerts[17];",
1693 "crash_report(void)",
1695 " printf(\"crash alert intervals:\\n\");",
1696 " for (i = 0; i < 17; i++)",
1697 " { printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);",
1702 "crash_reset(void)",
1703 "{ /* false alarm */",
1704 " if (crash_stamp != (clock_t) 0)",
1707 " double delta_time;",
1709 "#if defined(WIN32) || defined(WIN64)",
1710 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1712 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1714 " for (i = 0; i < 16; i++)",
1715 " { if (delta_time <= (i*30))",
1716 " { t_alerts[i] = delta_time;",
1719 " if (i == 16) t_alerts[i] = delta_time;",
1722 " printf(\"cpu%%d: crash alert off\\n\", core_id);",
1724 " crash_stamp = (clock_t) 0;",
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();",
1735 " crash_stamp = times(&start_tm);",
1738 " { printf(\"cpu%%d: crash detection\\n\", core_id);",
1742 "#if defined(WIN32) || defined(WIN64)",
1743 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1745 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1747 " return (delta_time >= maxtime);",
1752 "do_the_search(void)",
1754 " depth = mreached = 0;",
1755 " trpt = &trail[0];",
1757 " trpt->tau |= 4; /* the claim moves first */",
1759 " for (i = 0; i < (int) now._nr_pr; i++)",
1760 " { P0 *ptr = (P0 *) pptr(i);",
1762 " if (!(trpt->o_pm&2)",
1763 " && accpstate[ptr->_t][ptr->_p])",
1764 " { trpt->o_pm |= 2;",
1767 " if (!(trpt->o_pm&4)",
1768 " && progstate[ptr->_t][ptr->_p])",
1769 " { trpt->o_pm |= 4;",
1773 "#ifdef EVENT_TRACE",
1775 " if (accpstate[EVENT_TRACE][now._event])",
1776 " { trpt->o_pm |= 2;",
1779 " if (progstate[EVENT_TRACE][now._event])",
1780 " { trpt->o_pm |= 4;",
1785 " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */",
1787 " { i = &(now._a_t) - (uchar *) &now;",
1788 " Mask[i] = 1; /* _a_t */",
1793 " i = &(now._cnt[0]) - (uchar *) &now;",
1794 " while (j++ < NFAIR)",
1795 " Mask[i++] = 1; /* _cnt[] */",
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 */
1805 " printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
1806 " depth, now._cnt[now._a_t&1], now._a_t);",
1811 " c_stack_start = (char *) &i; /* meant to be read-only */",
1813 "#if defined(HAS_CODE) && defined (C_INIT)",
1814 " C_INIT; /* initialization of data that must precede fork() */",
1818 "#if defined(C_States) && (HAS_TRACK==1)",
1819 " /* capture initial state of tracked C objects */",
1820 " c_update((uchar *) &(now.c_state[0]));",
1824 " if (readtrail) getrail(); /* no return */",
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]));",
1836 " srand(RANDOMIZE);",
1844 " new_state(); /* start 1st DFS */",
1849 "#ifdef INLINE_REV",
1851 "do_reverse(Trans *t, short II, uchar M)",
1853 " int tt = (int) ((P0 *)this)->_p;",
1854 "#include REVERSE_MOVES",
1860 "#ifdef EVENT_TRACE",
1861 "static char _tp = 'n'; static int _qid = 0;",
1864 "do_transit(Trans *t, short II)",
1866 " int tt = (int) ((P0 *)this)->_p;",
1868 " uchar delta_m = 0;",
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; }",
1876 "#define continue return 0",
1878 " uchar ot = (uchar) ((P0 *)this)->_t;",
1881 "#include FORWARD_MOVES",
1883 "#ifdef EVENT_TRACE",
1884 " if (ot == EVENT_TRACE) boq = oboq;",
1890 "#ifdef EVENT_TRACE",
1892 "require(char tp, int qid)",
1894 " _tp = tp; _qid = qid;",
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;",
1902 " printf(\" event_trace move to -> %%d\\n\", t->st);",
1906 " if (accpstate[EVENT_TRACE][now._event])",
1907 " (trpt+1)->o_pm |= 2;",
1909 " if (progstate[EVENT_TRACE][now._event])",
1910 " (trpt+1)->o_pm |= 4;",
1913 "#ifdef NEGATED_TRACE",
1914 " if (now._event == endevent)",
1917 " depth++; trpt++;",
1919 " uerror(\"event_trace error (all events matched)\");",
1921 " trpt--; depth--;",
1926 " for (t = t->nxt; t; t = t->nxt)",
1927 " { if (do_transit(t, EVENT_TRACE))",
1928 " Uerror(\"non-determinism in event-trace\");",
1934 " printf(\" event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
1935 " tp, qid, now._event, t->forw);",
1938 "#ifdef NEGATED_TRACE",
1939 " now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
1942 " depth++; trpt++;",
1944 " uerror(\"event_trace error (no matching event)\");",
1946 " trpt--; depth--;",
1953 "enabled(int iam, int pid)",
1954 "{ Trans *t; uchar *othis = this;",
1955 " int res = 0; int tt; uchar ot;",
1957 " /* if (pid > 0) */ pid++;",
1960 " Uerror(\"used: enabled(pid=thisproc)\");",
1961 " if (pid < 0 || pid >= (int) now._nr_pr)",
1963 " this = pptr(pid);",
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))",
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));",
1986 " stop_time = clock();",
1987 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
1989 " if (delta_time > 0.01)",
1990 " { printf(\"t= %%6.3g \", delta_time);",
1991 " printf(\"R= %%7.0g\", nstates/delta_time);",
1993 " printf(\"\\n\");",
1994 " if (quota > 0.1 && delta_time > quota)",
1995 " { printf(\"Time limit of %%6.3g minutes exceeded\\n\", quota/60.0);",
1998 " leave_critical(GLOBAL_LOCK);",
1999 " sudden_stop(\"time-limit\");",
2009 " enter_critical(GLOBAL_LOCK); /* snapshot */",
2010 " printf(\"cpu%%d: \", core_id);",
2012 " printf(\"Depth= %%7ld States= %%8.3g \",",
2014 " (long) (nr_handoffs * z_handoff) +",
2016 " mreached, nstates);",
2017 " printf(\"Transitions= %%8.3g \", nstates+truncs);",
2019 " printf(\"Nodes= %%7d \", nr_states);",
2021 " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
2025 " leave_critical(GLOBAL_LOCK);",
2034 " && (stackwrite = creat(stackfile, TMODE)) < 0)",
2035 " Uerror(\"cannot create stackfile\");",
2037 " if (write(stackwrite, trail, DDD*sizeof(Trail))",
2038 " != DDD*sizeof(Trail))",
2039 " Uerror(\"stackfile write error -- disk is full?\");",
2041 " memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
2042 " memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
2050 " memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
2053 " || lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
2054 " Uerror(\"disk2stack lseek error\");",
2057 " && (stackread = open(stackfile, 0)) < 0)",
2058 " Uerror(\"cannot open stackfile\");",
2060 " if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
2061 " Uerror(\"disk2stack lseek error\");",
2063 " have = read(stackread, trail, DDD*sizeof(Trail));",
2064 " if (have != DDD*sizeof(Trail))",
2065 " Uerror(\"stackfile read error\");",
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 */
2074 " return (uchar *) pptr(x);",
2076 "int qs_empty(void);",
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",
2088 "#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
2093 "tally_succ(int cnt)",
2094 "{ if (cnt < 512) N_succ[cnt]++;",
2095 " else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);",
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];",
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];",
2112 " if (sum > N_succ[0])",
2113 " printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));",
2120 " uchar _n, _m, ot;",
2125 " uchar delta_m = 0;",
2127 " short II, JJ = 0, kk;",
2130 " short From = BASE, To = now._nr_pr-1;",
2132 " short From = now._nr_pr-1, To = BASE;",
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);",
2142 " { trpt->sched_limit = (trpt-1)->sched_limit;",
2144 " { trpt->sched_limit = 0;",
2149 " if (depth > hiwater)",
2151 " maxdepth += DDD;",
2155 " printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",",
2156 " CNT1, hiwater, maxdepth);",
2160 " trpt->tau &= ~(16|32|64); /* make sure these are off */",
2161 "#if defined(FULLSTACK) && defined(MA)",
2162 " trpt->proviso = 0;",
2165 " trpt->n_succ = 0;",
2168 " if (mem_hand_off())",
2171 " (trpt+1)->o_n = 1; /* not a deadlock: as below */",
2173 "#ifndef LOOPSTATE",
2174 " (trpt-1)->tau |= 16; /* worstcase guess: as below */",
2176 "#if NCORE>1 && defined(FULL_TRAIL)",
2178 " { Pop_Stack_Tree();",
2185 " if (depth >= maxdepth)",
2188 " printf(\"error: max search depth too small\\n\");",
2191 " { uerror(\"depth limit reached\");",
2195 " (trpt+1)->o_n = 1; /* not a deadlock */",
2197 "#ifndef LOOPSTATE",
2198 " (trpt-1)->tau |= 16; /* worstcase guess */",
2201 "#if NCORE>1 && defined(FULL_TRAIL)",
2203 " { Pop_Stack_Tree();",
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;*/
2214 " if ((trpt->tau&4) || ((trpt-1)->tau&128))",
2216 " if (boq == -1) { /* if not mid-rv */",
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",
2223 " if ((now._a_t&1) && depth > A_depth)",
2224 " { if (!memcmp((char *)&A_Root, ",
2225 " (char *)&now, vsize))",
2227 " depthfound = A_depth;",
2229 " printf(\"matches seed\\n\");",
2232 " uerror(\"non-progress cycle\");",
2234 " uerror(\"acceptance cycle\");",
2236 "#if NCORE>1 && defined(FULL_TRAIL)",
2238 " { Pop_Stack_Tree();",
2244 " printf(\"not seed\\n\");",
2248 " if (!(trpt->tau&8)) /* if no atomic move */",
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];",
2257 " JJ = onstack_now();", /* sets j1 */
2260 " JJ = II; /* worstcase guess for p.o. */",
2263 " II = bstore((char *)&now, vsize);", /* sets j1-j4 */
2267 " II = gstore((char *)&now, vsize, 0);",
2268 "#ifndef FULLSTACK",
2271 " JJ = (II == 2)?1:0;",
2274 " II = hstore((char *)&now, vsize);",
2276 " JJ = (II == 2)?1:0;",
2280 " kk = (II == 1 || II == 2);",
2282 /* II==0 new state */
2283 /* II==1 old state */
2284 /* II==2 on current dfs stack */
2285 /* II==3 on 1st dfs stack */
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)))",
2292 " if (!fairness || ((now._a_t&1) && now._cnt[1] == 1)) /* 5.1.4 */",
2294 " if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */",
2298 " II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
2300 " printf(\"state match on dfs stack\\n\");",
2306 "#if defined(FULLSTACK) && defined(BITSTATE)",
2307 " if (!JJ && (now._a_t&1) && depth > A_depth)",
2309 " uchar o_a_t = now._a_t;",
2310 " now._a_t &= ~(1|16|32);", /* 1st stack */
2311 " if (onstack_now())", /* changes j1 */
2314 " printf(\"state match on 1st dfs stack\\n\");",
2317 " now._a_t = o_a_t;", /* restore */
2321 " if (II == 3 && a_cycles && (now._a_t&1))",
2324 " if (fairness && now._cnt[1] > 1) /* was != 0 */",
2327 " printf(\"\tfairness count non-zero\\n\");",
2329 " II = 0;", /* treat as new state */
2336 "same_case: if (Lstate) depthfound = Lstate->D;",
2338 " uerror(\"non-progress cycle\");",
2340 " uerror(\"acceptance cycle\");",
2342 "#if NCORE>1 && defined(FULL_TRAIL)",
2344 " { Pop_Stack_Tree();",
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 */
2359 " if ((II && JJ) || (II == 3))",
2360 " { /* marker for liveness proviso */",
2361 "#ifndef LOOPSTATE",
2362 " (trpt-1)->tau |= 16;", /* truncated on stack */
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;",
2372 " { /* treat as non-stack state */",
2373 " (trpt-1)->tau |= 64;",
2377 " { /* successor outside stack */",
2378 " (trpt-1)->tau |= 64;",
2384 "#if NCORE>1 && defined(FULL_TRAIL)",
2386 " { Pop_Stack_Tree();",
2394 " { static long sdone = (long) 0; long ndone;",
2396 "#if defined(ZAPH) && defined(BITSTATE)",
2397 " zstates += (double) hfns;",
2399 " ndone = (unsigned long) (nstates/((double) FREQ));",
2400 " if (ndone != sdone)",
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();",
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();",
2419 " if (vprefix > 0)",
2420 " if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
2421 " { fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);",
2425 "#if defined(MA) && defined(W_XPT)",
2426 " if ((unsigned long) nstates%%W_XPT == 0)",
2427 " { void w_xpoint(void);",
2433 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
2436 "#if defined(FULLSTACK) && !defined(MA)",
2437 " printf(\"%%d: putting %%u (%%d)\\n\", depth,",
2439 " (trpt->ostate)?trpt->ostate->tagged:0);",
2441 " printf(\"%%d: putting\\n\", depth);",
2446 " trpt->ostate = Lstate;",
2452 " if (depth > mreached)",
2453 " mreached = depth;",
2455 " if (trpt->tau&4)",
2457 " trpt->tau &= ~(1|2); /* timeout and -request off */",
2460 " (trpt+1)->o_n = 0;",
2463 " if (now._nr_pr == 0) /* claim terminated */",
2464 " uerror(\"end state in claim reached\");",
2465 " check_claim(((P0 *)pptr(0))->_p);",
2467 " if (trpt->tau&4) /* must make a claimmove */",
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;",
2477 " printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
2478 " depth, now._a_t);",
2483 " II = 0; /* never */",
2488 " /* Look for a process with only safe transitions */",
2489 " /* (special rules apply in the 2nd dfs) */",
2490 " if (boq == -1 && From != To",
2494 " && (depth < z_handoff)", /* not for border states */
2499 " && ((a_cycles) || (!a_cycles && depth < z_handoff))",
2501 " && (!(now._a_t&1)",
2503 " #ifndef BITSTATE",
2506 " !((trpt-1)->proviso))",
2508 " !(trpt->proviso))",
2512 " (trpt-1)->ostate &&",
2513 " !(((char *)&((trpt-1)->ostate->state))[0] & 128))", /* proviso bit in _a_t */
2515 " !(((char *)&(trpt->ostate->state))[0] & 128))",
2520 " (trpt-1)->ostate &&",
2521 " (trpt-1)->ostate->proviso == 0)",
2523 " trpt->ostate->proviso == 0)",
2527 "#endif", /* SAFETY */
2530 " for (II = From; II <= To; II++)",
2532 " for (II = From; II >= To; II--)",
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)",
2543 " if (!q_cond(II, t))",
2547 " From = To = II; /* the process preselected */",
2551 " trpt->tau |= 32; /* preselect marker */",
2554 " printf(\"%%3d: proc %%d Pre\", depth, II);",
2555 " printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
2556 " t->om, trpt->tau);",
2558 " printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
2559 " depth, II, trpt->tau);",
2565 " trpt->tau &= ~32;",
2567 "#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
2571 " /* The Main Expansion Loop over Processes */",
2573 " trpt->o_pm &= ~(8|16|32|64); /* fairness-marks */",
2575 " if (fairness && boq == -1",
2577 " && (!(trpt->tau&4) && !((trpt-1)->tau&128))",
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 */
2583 " if (a_cycles && (trpt->o_pm&2))",
2584 " { /* Accepting state */",
2586 " now._cnt[now._a_t&1] = now._nr_pr + 1;", /* NEW +1 */
2587 " trpt->o_pm |= 8;",
2589 " printf(\"%%3d: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
2590 " depth, now._cnt[now._a_t&1], now._a_t);",
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;",
2600 " printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
2601 " depth, now._a_t);",
2607 " for (II = From; II <= To; II++)",
2609 " for (II = From; II >= To; II--)",
2613 " /* no rendezvous with same proc */",
2614 " if (boq != -1 && trpt->pr == II) continue;",
2617 " /* limit max nr of interleavings */",
2618 " if (From != To", /* not a PO or atomic move */
2619 " && depth > 0", /* there is a prior move */
2621 " && II != 0", /* never claim can always move */
2623 " && (trpt-1)->pr != II", /* context switch */
2624 " && trpt->sched_limit >= sched_max)",
2631 " this = pptr(II);",
2632 " tt = (int) ((P0 *)this)->_p;",
2633 " ot = (uchar) ((P0 *)this)->_t;",
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 */
2648 " if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
2649 " continue; /* did it before */",
2652 " trpt->o_pm &= ~1; /* no move in this pid yet */",
2653 "#ifdef EVENT_TRACE",
2654 " (trpt+1)->o_event = now._event;",
2656 " /* Fairness: Cnt++ when Cnt == II */",
2658 " trpt->o_pm &= ~64; /* didn't apply rule 2 */",
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;",
2666 " /* claim need not participate */",
2668 " now._cnt[now._a_t&1] = 1;",
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);",
2675 " trpt->o_pm |= (32|64);",
2678 "#ifdef HAS_PROVIDED",
2679 " if (!provided(II, ot, tt, t)) continue;",
2681 " /* check all trans of proc II - escapes first */",
2682 "#ifdef HAS_UNLESS",
2683 " trpt->e_state = 0;",
2685 " (trpt+1)->pr = (uchar) II;", /* for uerror */
2686 " (trpt+1)->st = tt;",
2689 " for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
2690 " { if (strcmp(t->tp, \"else\") == 0)",
2695 " { t = trans[ot][tt];",
2697 " printf(\"randomizer: suppressed, saw else\\n\");",
2700 " { eoi = rand()%%ooi;",
2702 " printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
2704 " for (t = trans[ot][tt]; t; t = t->nxt)",
2705 " if (eoi-- <= 0) break;",
2708 " for ( ; t && ooi > 0; t = t->nxt, ooi--)",
2709 "#else", /* ie dont randomize */
2710 " for (t = trans[ot][tt]; t; t = t->nxt)",
2713 "#ifdef HAS_UNLESS",
2714 " /* exploring all transitions from",
2715 " * a single escape state suffices",
2717 " if (trpt->e_state > 0",
2718 " && trpt->e_state != t->e_trans)",
2721 " printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
2722 " t->e_trans, trpt->e_state);",
2727 " (trpt+1)->o_t = t;", /* for uerror */
2729 "#include FORWARD_MOVES",
2730 "P999: /* jumps here when move succeeds */",
2732 " if (!(_m = do_transit(t, II))) continue;",
2739 " && (trpt-1)->pr != II)",
2740 " { trpt->sched_limit = 1 + (trpt-1)->sched_limit;",
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 */",
2752 " trpt->o_pm |= 1; /* we moved */",
2756 " if (loopstate[ot][tt])",
2759 " printf(\"exiting from loopstate:\\n\");",
2761 " trpt->tau |= 16;", /* exiting loopstate */
2769 "#if defined(VERBOSE) || defined(CHECK)",
2770 "#if defined(SVDUMP)",
2771 " cpu_printf(\"%%3d: proc %%d exec %%d \\n\", depth, II, t->t_id);",
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",
2780 " cpu_printf(\"\\t(escape to state %%d)\\n\", t->st);",
2784 " cpu_printf(\"\\t(randomizer %%d)\\n\", ooi);",
2792 " now._last = II - BASE;",
2794 "#ifdef HAS_UNLESS",
2795 " trpt->e_state = t->e_trans;",
2798 " depth++; trpt++;",
2799 " trpt->pr = (uchar) II;",
2801 " trpt->o_pm &= ~(2|4);",
2803 " { ((P0 *)this)->_p = t->st;",
2804 "/* moved down reached[ot][t->st] = 1; */",
2809 "#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
2812 "#define P__Q ((P0 *)pptr(ii))",
2815 " /* state 1 of np_ claim is accepting */",
2816 " if (((P0 *)pptr(0))->_p == 1)",
2817 " trpt->o_pm |= 2;",
2819 " for (ii = 0; ii < (int) now._nr_pr; ii++)",
2820 " { if (accpstate[P__Q->_t][P__Q->_p])",
2821 " { trpt->o_pm |= 2;",
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;",
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;",
2841 " trpt->oo_i = ooi;",
2843 " if (boq != -1 || (t->atom&2))",
2844 " { trpt->tau |= 8;",
2846 " /* atomic sequence in claim */",
2847 " if((trpt-1)->tau&4)",
2850 " trpt->tau &= ~4;",
2852 " { if ((trpt-1)->tau&4)",
2853 " trpt->tau &= ~4;",
2857 " /* if claim allowed timeout, so */",
2858 " /* does the next program-step: */",
2859 " if (((trpt-1)->tau&1) && !(trpt->tau&4))",
2863 " trpt->tau &= ~8;",
2865 " if (boq == -1 && (t->atom&2))",
2866 " { From = To = II; nlinks++;",
2869 " { From = BASE; To = now._nr_pr-1;",
2871 " { From = now._nr_pr-1; To = BASE;",
2874 "#if NCORE>1 && defined(FULL_TRAIL)",
2876 " { Push_Stack_Tree(II, t->t_id);",
2879 " goto Down; /* pseudo-recursion */",
2882 " cpu_printf(\"%%d: Up - %%s\\n\", depth,",
2883 " (trpt->tau&4)?\"claim\":\"program\");",
2891 "#if defined(MA) || NCORE>1",
2892 " if (depth <= 0) return;",
2893 " /* e.g., if first state is old, after a restart */",
2898 " && depth < hiwater - (HHH-DDD) + 2)",
2902 " maxdepth -= DDD;",
2905 " printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
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);",
2923 " { int d; Trail *trl;",
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;",
2932 " now._last = (depth<1)?0:(trpt-1)->pr;",
2935 "#ifdef EVENT_TRACE",
2936 " now._event = trpt->o_event;",
2939 " if ((now._a_t&1) && depth <= A_depth)",
2940 " return; /* to checkcycles() */",
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;",
2947 " ooi = trpt->oo_i;",
2949 "#ifdef INLINE_REV",
2950 " _m = do_reverse(t, II, _m);",
2952 "#include REVERSE_MOVES",
2953 "R999: /* jumps here when done */",
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);",
2963 " /* pass the proviso tags */",
2964 " if ((trpt->tau&8) /* rv or atomic */",
2965 " && (trpt->tau&16))",
2966 " (trpt-1)->tau |= 16;", /* pass upward */
2968 " if ((trpt->tau&8) /* rv or atomic */",
2969 " && (trpt->tau&64))",
2970 " (trpt-1)->tau |= 64;",
2973 " depth--; trpt--;",
2979 " (trans[ot][tt])->om = _m; /* head of list */",
2982 " /* i.e., not set if rv fails */",
2985 "#if defined(VERI) && !defined(NP)",
2986 " if (II == 0 && verbose && !reached[ot][t->st])",
2988 " printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
2989 " depth, t->st, src_claim [t->st]);",
2993 " reached[ot][t->st] = 1;",
2994 " reached[ot][tt] = 1;",
2996 "#ifdef HAS_UNLESS",
2997 " else trpt->e_state = 0; /* undo */",
3000 " if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
3001 " ((P0 *)this)->_p = tt;",
3002 " } /* all options */",
3005 " if (!t && ooi > 0)", /* means we skipped some initial options */
3006 " { t = trans[ot][tt];",
3008 " printf(\"randomizer: continue for %%d more\\n\", ooi);",
3014 " printf(\"randomizer: done\\n\");",
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 */
3025 " if (now._cnt[now._a_t&1] == 1)",
3026 " now._cnt[now._a_t&1] = 2;",
3028 " now._cnt[now._a_t&1] += 1;",
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);",
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;",
3040 " II = From-1;", /* after loop incr II == From */
3042 " II = From+1;", /* after loop decr II == From */
3048 " if (II == 0) break; /* never claim */",
3050 " } /* all processes */",
3053 " tally_succ(trpt->n_succ);",
3057 " if (_n == 0 /* no process could move */",
3062 " && trpt->sched_limit >= sched_max)",
3063 " { _n = 1; /* not a deadlock */",
3068 " /* Fairness: undo Rule 2 */",
3069 " if (trpt->o_pm&32) /* remains if proc blocked */",
3072 " if (now._cnt[now._a_t&1] == 1)",
3073 " now._cnt[now._a_t&1] = 2;",
3075 " now._cnt[now._a_t&1] += 1;",
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);",
3081 " trpt->o_pm &= ~32;",
3084 /* 12/97 non-progress cycles cannot be created
3085 * by stuttering extension, here or elsewhere
3088 " && _n == 0 /* nobody moved */",
3090 " && !(trpt->tau&4) /* in program move */",
3092 " && !(trpt->tau&8) /* not an atomic one */",
3094 " && ((trpt->tau&1) || endstate())",
3097 " && (trpt->tau&1) /* already tried timeout */",
3102 " && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
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;",
3115 " From = BASE; To = now._nr_pr-1;",
3117 " From = now._nr_pr-1; To = BASE;",
3119 "#if defined(VERBOSE) || defined(CHECK)",
3120 " printf(\"%%3d: fairness default move \", depth);",
3121 " printf(\"(all procs block)\\n\");",
3126 "Q999: /* returns here with _n>0 when done */;",
3128 " if (trpt->o_pm&8)",
3129 " { now._a_t &= ~2;",
3130 " now._cnt[now._a_t&1] = 0;",
3131 " trpt->o_pm &= ~8;",
3133 " printf(\"%%3d: fairness undo Rule 1, _a_t=%%d\\n\",",
3134 " depth, now._a_t);",
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;",
3142 " printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
3143 " depth, now._a_t);",
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)))",
3155 " /* preselected move - no successors outside stack */",
3156 " if ((trpt->tau&32) && !(trpt->tau&64))",
3159 " { From = BASE; To = now._nr_pr-1;",
3161 " { From = now._nr_pr-1; To = BASE;",
3164 " printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3165 " depth, II+1, _n, trpt->tau);",
3167 " _n = 0; trpt->tau &= ~(16|32|64);",
3169 " if (II <= To) /* II already decremented */",
3171 " if (II >= BASE) /* II already decremented */",
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)))",
3184 " printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3185 " depth, II+1, (int) _n, trpt->tau);",
3187 " if (a_cycles && (trpt->tau&16))",
3188 " { if (!(now._a_t&1))",
3191 " printf(\"%%3d: setting proviso bit\\n\", depth);",
3196 " (trpt-1)->proviso = 1;",
3198 " trpt->proviso = 1;",
3202 " if ((trpt-1)->ostate)",
3203 " ((char *)&((trpt-1)->ostate->state))[0] |= 128;",
3205 " ((char *)&(trpt->ostate->state))[0] |= 128;",
3210 " if ((trpt-1)->ostate)",
3211 " (trpt-1)->ostate->proviso = 1;",
3213 " trpt->ostate->proviso = 1;",
3217 " From = BASE; To = now._nr_pr-1;",
3219 " From = now._nr_pr-1; To = BASE;",
3221 " _n = 0; trpt->tau &= ~(16|32|64);",
3222 " goto Again; /* do full search */",
3223 " } /* else accept reduction */",
3226 " { From = BASE; To = now._nr_pr-1;",
3228 " { From = now._nr_pr-1; To = BASE;",
3230 " _n = 0; trpt->tau &= ~(16|32|64);",
3232 " if (II <= To) /* already decremented */",
3234 " if (II >= BASE) /* already decremented */",
3244 " if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
3247 " cpu_printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
3248 " depth, II, trpt->tau, boq);",
3251 " /* ok if a rendez-vous fails: */",
3252 " if (boq != -1) goto Done;",
3254 " /* ok if no procs or we're at maxdepth */",
3255 " if ((now._nr_pr == 0 && (!strict || qs_empty()))",
3259 " || depth >= maxdepth-1) goto Done;",
3261 " if ((trpt->tau&8) && !(trpt->tau&4))",
3262 " { trpt->tau &= ~(1|8);",
3263 " /* 1=timeout, 8=atomic */",
3265 " From = BASE; To = now._nr_pr-1;",
3267 " From = now._nr_pr-1; To = BASE;",
3270 " cpu_printf(\"%%3d: atomic step proc %%d unexecutable\\n\", depth, II+1);",
3273 " trpt->tau |= 4; /* switch to claim */",
3279 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
3282 " if (trpt->tau&4)",
3285 " if (trpt->tau&2) /* requested */",
3287 " { trpt->tau |= 1;",
3288 " trpt->tau &= ~2;",
3290 " cpu_printf(\"%%d: timeout\\n\", depth);",
3295 " { /* only claim can enable timeout */",
3296 " if ((trpt->tau&8)",
3297 " && !((trpt-1)->tau&4))",
3298 "/* blocks inside an atomic */ goto BreakOut;",
3300 " cpu_printf(\"%%d: req timeout\\n\",",
3303 " (trpt-1)->tau |= 2; /* request */",
3304 "#if NCORE>1 && defined(FULL_TRAIL)",
3306 " { Pop_Stack_Tree();",
3314 " cpu_printf(\"%%d: timeout\\n\", depth);",
3322 /* old location of atomic block code */
3325 "#ifndef NOSTUTTER",
3326 " if (!(trpt->tau&4))",
3327 " { trpt->tau |= 4; /* claim stuttering */",
3328 " trpt->tau |= 128; /* stutter mark */",
3330 " cpu_printf(\"%%d: claim stutter\\n\", depth);",
3338 " if (!noends && !a_cycles && !endstate())",
3339 " { depth--; trpt--; /* new 4.2.3 */",
3340 " uerror(\"invalid end state\");",
3341 " depth++; trpt++;",
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++;",
3353 " if (!(trpt->tau&8)) /* not in atomic seqs */",
3356 " if (_n != 0", /* we made a move */
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))",
3365 " && !(now._a_t&1))", /* not in 2nd DFS */
3368 " if (fairness)", /* implies a_cycles */
3371 " cpu_printf(\"Consider check %%d %%d...\\n\",",
3372 " now._a_t, now._cnt[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
3385 " if ((now._a_t&2) /* A-bit */",
3386 " && (now._cnt[0] == 1))",
3390 " if (a_cycles && (trpt->o_pm&2))",
3395 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
3398 " && (((trpt->tau&4) && !(trpt->tau&128))",
3399 " || ( (trpt-1)->tau&128)))",
3405 "#if defined(FULLSTACK)",
3406 " printf(\"%%d: zapping %%u (%%d)\\n\",",
3407 " depth, trpt->ostate,",
3408 " (trpt->ostate)?trpt->ostate->tagged:0);",
3417 " && (((trpt->tau&4) && !(trpt->tau&128))",
3418 " || ( (trpt-1)->tau&128)))",
3424 " printf(\"%%d: zapping\\n\", depth);",
3428 " if (trpt->proviso)",
3429 " gstore((char *) &now, vsize, 1);",
3436 "#if NCORE>1 && defined(FULL_TRAIL)",
3438 " { Pop_Stack_Tree();",
3445 "void new_state(void) { /* place holder */ }",
3449 "assert(int a, char *s, int ii, int tt, Trans *t)",
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';",
3458 " strcpy(&bad[19], s);",
3462 "#ifndef NOBOUNDCHECK",
3464 "Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
3466 " assert((x >= 0 && x < y), \"- invalid array index\",",
3475 " printf(\"%%9.8g states, stored (%%g visited)\\n\",",
3476 " nstates - nShadow, nstates);",
3478 " printf(\"%%9.8g states, stored\\n\", nstates);",
3481 " printf(\" %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
3482 " printf(\" %%8g rvs succeeded\\n\", midrv-failedrv);",
3484 " printf(\" %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
3487 " printf(\" %%8g midrv\\n\", midrv);",
3488 " printf(\" %%8g failedrv\\n\", failedrv);",
3489 " printf(\" %%8g revrv\\n\", revrv);",
3492 " printf(\"%%9.8g states, matched\\n\", truncs);",
3494 " printf(\"%%9.8g matches within stack\\n\",truncs2);",
3497 " printf(\"%%9.8g transitions (= visited+matched)\\n\",",
3498 " nstates+truncs);",
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);",
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 */",
3514 " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
3517 " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
3518 " (double)(((double) udmem) * 8.0) / (double) nstates);",
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);",
3526 " { printf(\"total bits available: %%8g (-M%%ld)\\n\",",
3527 " ((double) udmem) * 8.0, udmem/(1024L*1024L));",
3530 " printf(\"total bits available: %%8g (-w%%d)\\n\",",
3531 " ((double) (ONE_L << (ssize-4)) * 16.0), ssize);",
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\");",
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;",
3551 " int mverbose = verbose;",
3555 " if (verbose) cpu_printf(\"wrapup -- %%d error(s)\\n\", errors);",
3556 " if (core_id != 0)",
3559 " void dsk_stats(void);",
3562 " if (search_terminated != NULL)",
3563 " { *search_terminated |= 2; /* wrapup */",
3565 " exit(0); /* normal termination, not an error */",
3568 "#if !defined(WIN32) && !defined(WIN64)",
3569 " signal(SIGINT, SIG_DFL);",
3571 " printf(\"\\n(%%s)\\n\", SpinVersion);",
3572 " if (!done) printf(\"Warning: Search not completed\\n\");",
3574 " (void) unlink((const char *)stackfile);",
3578 " { printf(\" + Multi-Core (NCORE=%%d)\\n\", NCORE);",
3580 " { printf(\" + Multi-Core (NCORE=%%d -z%%d)\\n\", NCORE, z_handoff);",
3584 " printf(\" + Using Breadth-First Search\\n\");",
3587 " printf(\" + Partial Order Reduction\\n\");",
3590 " printf(\" + Reverse Depth-First Search Order\\n\");",
3593 " printf(\" + Reverse Transition Ordering\\n\");",
3596 " printf(\" + Randomized Transition Ordering\\n\");",
3599 " printf(\" + Scheduling Restriction (-DSCHED=%%d)\\n\", sched_max);",
3603 " printf(\" + Queue Proviso\\n\");",
3607 " printf(\" + Compression\\n\");",
3610 " printf(\" + Graph Encoding (-DMA=%%d)\\n\", MA);",
3612 " printf(\" Restarted from checkpoint %%s.xpt\\n\", PanSource);",
3616 " #ifdef FULLSTACK",
3617 " printf(\" + FullStack Matching\\n\");",
3619 " #ifdef CNTRSTACK",
3620 " printf(\" + CntrStack Matching\\n\");",
3624 " printf(\"\\nBit statespace search for:\\n\");",
3627 " printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
3629 " printf(\"\\nFull statespace search for:\\n\");",
3632 "#ifdef EVENT_TRACE",
3633 "#ifdef NEGATED_TRACE",
3634 " printf(\"\tnotrace assertion \t+\\n\");",
3636 " printf(\"\ttrace assertion \t+\\n\");",
3640 " printf(\"\tnever claim \t+\\n\");",
3641 " printf(\"\tassertion violations\t\");",
3643 " printf(\"- (disabled by -A flag)\\n\");",
3645 " printf(\"+ (if within scope of claim)\\n\");",
3648 " printf(\"\tnever claim \t- (not selected)\\n\");",
3650 " printf(\"\tnever claim \t- (none specified)\\n\");",
3652 " printf(\"\tassertion violations\t\");",
3654 " printf(\"- (disabled by -A flag)\\n\");",
3656 " printf(\"+\\n\");",
3660 " printf(\"\tnon-progress cycles \t\");",
3662 " printf(\"\tacceptance cycles \t\");",
3665 " printf(\"+ (fairness %%sabled)\\n\",",
3666 " fairness?\"en\":\"dis\");",
3667 " else printf(\"- (not selected)\\n\");",
3669 " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");",
3672 " printf(\"\tinvalid end states\t- \");",
3673 " printf(\"(disabled by \");",
3675 " printf(\"-E flag)\\n\\n\");",
3677 " printf(\"never claim)\\n\\n\");",
3679 " printf(\"\tinvalid end states\t\");",
3681 " printf(\"- (disabled by -E flag)\\n\\n\");",
3683 " printf(\"+\\n\\n\");",
3685 " printf(\"State-vector %%d byte, depth reached %%ld\", hmax,",
3687 " (nr_handoffs * z_handoff) +",
3690 " printf(\", errors: %%d\\n\", errors);",
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);",
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);",
3710 " printf(\"\\n\");",
3713 "#if defined(BITSTATE) || !defined(NOCOMP)",
3714 " nr1 = (nstates-nShadow)*",
3715 " (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
3719 " nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
3723 "#if !defined(MA) || defined(COLLAPSE)",
3724 " nr3 = (double) (ONE_L<<ssize)*sizeof(struct H_el *);",
3729 " nr3 = (double) (udmem);",
3732 " nr3 = (double) (ONE_L<<(ssize-3));",
3734 " nr5 = (double) (ONE_L<<(ssize-3));",
3737 " nr5 = (double) (maxdepth*sizeof(struct H_el *));",
3740 " nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
3741 " + (double) (smax * (sizeof(Stack) + Maxbody));",
3743 " if (mverbose || memcnt < nr1+nr2+nr3+nr4+nr5)",
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;",
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.);",
3759 " printf(\"\t\tin %%d local heaps of %%7.3f MB each\\n\",",
3760 " NCORE, mem_reserved/(NCORE*1048576.));",
3762 " printf(\"\\n\");",
3767 " printf(\"%%9.3f\tmemory used for hash array (-M%%ld)\\n\",",
3768 " nr3/1048576., udmem/(1024L*1024L));",
3771 " printf(\"%%9.3f\tmemory used for hash array (-w%%d)\\n\",",
3772 " nr3/1048576., ssize);",
3774 " printf(\"%%9.3f\tmemory used for bit stack\\n\",",
3776 " remainder = remainder - nr3 - nr5;",
3778 " printf(\"%%9.3f\tactual memory usage for states\",",
3779 " tmp_nr/1048576.);",
3780 " remainder -= tmp_nr;",
3782 " if (tmp_nr > 0.)",
3783 " { if (tmp_nr > nr1) printf(\"unsuccessful \");",
3784 " printf(\"compression: %%.2f%%%%)\\n\",",
3785 " (100.0*tmp_nr)/nr1);",
3787 " printf(\"less than 1k)\\n\");",
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));",
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;",
3804 " printf(\"%%9.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
3805 " nr2/1048576., maxdepth);",
3806 " remainder -= nr2;",
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.);",
3815 " printf(\" + a global q of %%7.3f MB\\n\",",
3816 " (double) GWQ_SIZE / 1048576.);",
3818 " printf(\"\\n\");",
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.);",
3835 " printf(\"%%9.3f\tmemory usage (Mbyte)\\n\\n\",",
3836 " memcnt/1048576.);",
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\");",
3848 " if ((done || verbose) && !no_rck) do_reach();",
3851 " printf(\"\\nPeg Counts (transitions executed):\\n\");",
3852 " for (i = 1; i < NTRANS; i++)",
3853 " { if (peg[i]) putpeg(i, peg[i]);",
3856 "#ifdef VAR_RANGES",
3860 " if (vprefix > 0) close(svfd);",
3863 " printf(\"%%g loopstates hit\\n\", cnt_loops);",
3868 "#if NCORE>1 && defined(T_ALERT)",
3875 "{ printf(\"Interrupted\\n\");",
3877 " was_interrupted = 1;",
3885 " * super fast hash, based on Paul Hsieh's function",
3886 " * http://www.azillionmonkeys.com/qed/hash.html",
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)))",
3895 " #ifndef get16bits",
3896 " #define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\",
3897 " +(uint32_t)(((const uint8_t *)(d))[0]) )",
3901 "d_sfh(const char *s, int len)",
3902 "{ uint32_t h = len, tmp;",
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);",
3916 " case 3: h += get16bits(s);",
3918 " h ^= s[sizeof(uint16_t)] << 18;",
3921 " case 2: h += get16bits(s);",
3925 " case 1: h += *s;",
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",
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); \\",
3961 "/* 32-bit Jenkins hash, 2006",
3962 " * http://burtleburtle.net/bob/c/lookup3.c",
3964 "#define rot(x,k) (((x)<<(k))|((x)>>(32-(k))))",
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; \\",
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); \\",
3987 "d_hash(uchar *kb, int nbytes)",
3989 "#if defined(HASH64) || defined(WIN64)",
3990 " uint64_t a = 0, b, c, n;",
3991 " uint64_t *k = (uint64_t *) kb;",
3993 " uint32_t a, b, c, n;",
3994 " uint32_t *k = (uint32_t *) kb;",
3996 " /* extend to multiple of words, if needed */",
3997 " n = nbytes/WS; /* nr of words */",
3998 " a = nbytes - (n*WS);",
4001 " bp = kb + nbytes;",
4003 " case 3: *bp++ = 0; /* fall thru */",
4004 " case 2: *bp++ = 0; /* fall thru */",
4005 " case 1: *bp = 0;",
4008 "#if defined(HASH64) || defined(WIN64)",
4009 " b = HASH_CONST[HASH_NR];",
4010 " c = 0x9e3779b97f4a7c13LL; /* arbitrary value */",
4019 " c += (((uint64_t) nbytes)<<3);",
4021 " case 2: b += k[1];",
4022 " case 1: a += k[0];",
4026 "#else", /* 32 bit version: */
4027 " a = c = 0xdeadbeef + (n<<2);",
4028 " b = HASH_CONST[HASH_NR];",
4038 " case 3: c += k[2];",
4039 " case 2: b += k[1];",
4040 " case 1: a += k[0];",
4045 " j1 = c&nmask; j3 = a&7; /* 1st bit */",
4046 " j2 = b&nmask; j4 = (a>>3)&7; /* 2nd bit */",
4051 "s_hash(uchar *cp, int om)",
4054 " d_sfh((const char *) cp, om); /* sets K1 */",
4056 " d_hash(cp, om); /* sets K1 etc */",
4059 " if (S_Tab == H_tab)", /* state stack in bitstate search */
4060 " j1 = K1 %% omaxdepth;",
4062 "#endif", /* if (S_Tab != H_Tab) */
4063 " if (ssize < 8*WS)",
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();",
4080 "{ if (!prerand) inirand();",
4081 " return prerand[depth];",
4086 "set_masks(void) /* 4.2.5 */",
4088 " if (WS == 4 && ssize >= 32)",
4089 " { mask = 0xffffffff;",
4091 " switch (ssize) {",
4092 " case 34: nmask = (mask>>1); break;",
4093 " case 33: nmask = (mask>>2); break;",
4094 " default: nmask = (mask>>3); break;",
4099 " } else if (WS == 8)",
4100 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
4102 " nmask = mask>>3;",
4106 " } else if (WS != 4)",
4107 " { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", (long int) WS);",
4109 " } else /* WS == 4 and ssize < 32 */",
4110 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
4111 " nmask = (mask>>3);",
4115 "static long reclaim_size;",
4116 "static char *reclaim_mem;",
4117 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
4119 " #error cannot combine AUTO_RESIZE with NCORE>1 yet",
4121 "static struct H_el **N_tab;",
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 */",
4129 " if (ssize < 8*WS) /* probably always true */",
4132 " p->nxt = N_tab[j2];",
4136 "resize_hashtable(void)",
4138 " if (WS == 4 && ssize >= 27 - 1)",
4139 " { return; /* canot increase further */",
4142 " ssize += 2; /* 4x size */",
4144 " printf(\"pan: resizing hashtable to -w%%d.. \", ssize);",
4146 " N_tab = (struct H_el **)",
4147 " emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
4149 " set_masks(); /* they changed */",
4151 " for (j1 = 0; j1 < (ONE_L << (ssize - 2)); j1++)",
4152 " { reverse_capture(H_tab[j1]);",
4154 " reclaim_mem = (char *) H_tab;",
4155 " reclaim_size = (ONE_L << (ssize - 2));",
4158 " printf(\" done\\n\");",
4161 "#if defined(ZAPH) && defined(BITSTATE)",
4163 "zap_hashtable(void)",
4164 "{ cpu_printf(\"pan: resetting hashtable\\n\");",
4166 " { memset(SS, 0, udmem);",
4168 " { memset(SS, 0, ONE_L<<(ssize-3));",
4174 "main(int argc, char *argv[])",
4175 "{ void to_compile(void);\n",
4176 " efd = stderr; /* default */",
4178 " bstore = bstore_reg; /* default */",
4182 " strcpy(o_cmdline, \"\");",
4183 " for (j = 1; j < argc; j++)",
4184 " { strcat(o_cmdline, argv[j]);",
4185 " strcat(o_cmdline, \" \");",
4187 " /* printf(\"Command Line: %%s\\n\", o_cmdline); */",
4188 " if (strlen(o_cmdline) >= sizeof(o_cmdline))",
4189 " { Uerror(\"option list too long\");",
4192 " while (argc > 1 && argv[1][0] == '-')",
4193 " { switch (argv[1][1]) {",
4196 " case 'a': fprintf(efd, \"error: -a disabled\");",
4197 " usage(efd); break;",
4199 " case 'a': a_cycles = 1; break;",
4202 " case 'A': noasserts = 1; break;",
4203 " case 'b': bounded = 1; break;",
4205 " case 'C': coltrace = 1; goto samething;",
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;",
4212 " case 'F': if (strlen(argv[1]) > 2)",
4213 " stackfile = &argv[1][2];",
4216 "#if !defined(SAFETY) && !defined(NOFAIR)",
4217 " case 'f': fairness = 1; break;",
4220 " case 'g': gui = 1; goto samething;",
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 */",
4228 " case 'k': hfns = atoi(&argv[1][2]); break;",
4231 " case 'L': sched_max = atoi(&argv[1][2]); break;",
4235 " case 'l': a_cycles = 1; break;",
4237 " case 'l': fprintf(efd, \"error: -l disabled\");",
4238 " usage(efd); break;",
4243 " case 'M': udmem = atoi(&argv[1][2]); break;",
4244 " case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
4246 " case 'M': case 'G':",
4247 " fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
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 */",
4260 " case 'p': vprefix = atoi(&argv[1][2]); break;",
4263 " case 'Q': quota = (double) 60.0 * (double) atoi(&argv[1][2]); break;",
4265 " case 'q': strict = 1; break;",
4266 " case 'R': Nrun = atoi(&argv[1][2]); break;",
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 */",
4277 " case 'S': silent = 1; goto samething;",
4280 " case 's': hfns = 1; break;",
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;",
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]);",
4302 " { printf(\"cpu%%d: pid %%d parent %%d\\n\",",
4303 " core_id, getpid(), worker_pids[0]);",
4306 " case 'z': z_handoff = atoi(&argv[1][2]); break;",
4308 " case 'z': break; /* ignored for single-core */",
4310 " default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
4314 " if (iterative && TMODE != 0666)",
4316 " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
4318 "#if defined(HASH32) && !defined(SFH)",
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\");",
4324 "#if defined(WIN32) || defined(WIN64)",
4325 " if (TMODE == 0666)",
4326 " TMODE = _S_IWRITE | _S_IREAD;",
4328 " TMODE = _S_IREAD;",
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\");",
4339 " if (z_handoff < 0)",
4340 " { z_handoff = 20; /* conservative default - for non-liveness checks */",
4342 "#if defined(NGQ) || defined(LWQ_FIXED)",
4343 " LWQ_SIZE = (double) (128.*1048576.);",
4345 " LWQ_SIZE = (double) ( z_handoff + 2.) * (double) sizeof(SM_frame);",
4346 /* the added margin of +2 is not really necessary */
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\");",
4354 " }", /* it still works though, the later cores get states from the global q */
4356 " #ifdef HAS_HIDDEN",
4357 " #error cannot use hidden variables when compiling multi-core",
4363 " fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
4366 " omaxdepth = maxdepth;",
4368 " if (WS == 4 && ssize > 34)", /* 32-bit word size */
4370 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
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",
4377 " if (WS == 4 && ssize > 27)",
4379 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
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",
4389 " hiwater = HHH = maxdepth-10;",
4392 " { stackfile = (char *) emalloc(strlen(PanSource)+4+1);",
4393 " sprintf(stackfile, \"%%s._s_\", PanSource);",
4396 " { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
4401 "#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
4402 " #warning -DR_XPT and -DW_XPT assume -DMA (ignored)",
4405 " if (iterative && a_cycles)",
4406 " fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",
4410 " #error -DBFS not compatible with -DSC",
4413 " #error -DBFS not compatible with _last",
4415 " #ifdef HAS_STACK",
4416 " #error cannot use c_track UnMatched with BFS",
4419 " #warning -DREACH is redundant when -DBFS is used",
4422 "#if defined(MERGED) && defined(PEG)",
4423 " #error to use -DPEG use: spin -o3 -a",
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 */",
4431 " #error cannot combine -DHC and -DNOCOMP",
4435 " #error cannot combine -DHC and -DBITSTATE",
4438 "#if defined(SAFETY) && defined(NP)",
4439 " #error cannot combine -DNP and -DBFS or -DSAFETY",
4443 " #error cannot combine -DMA and -DBITSTATE",
4446 " #error usage: -DMA=N with N > 0 and N < VECTORSZ",
4451 " #error cannot combine -DBITSTATE and -DCOLLAPSE",
4454 " #error cannot combine -DCOLLAPSE and -DSFH",
4455 " /* use of NOCOMP is the real reason */",
4458 " #error cannot combine -DCOLLAPSE and -DNOCOMP",
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\");",
4472 "#if defined(REM_VARS) && !defined(NOREDUCE)",
4473 " #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)",
4475 "#if defined(NOCOMP) && !defined(BITSTATE)",
4477 " { fprintf(efd, \"error: use of -DNOCOMP voids -l and -a\\n\");",
4483 " memlim = ((double) MEMLIM) * (double) (1<<20); /* size in Mbyte */",
4487 " if (Nrun > 1) HASH_NR = Nrun - 1;",
4489 " if (Nrun < 1 || Nrun > 32)",
4490 " { fprintf(efd, \"error: invalid arg for -R\\n\");",
4494 " if (fairness && !a_cycles)",
4495 " { fprintf(efd, \"error: -f requires -a or -l\\n\");",
4498 " #if ACCEPT_LAB==0",
4500 " { fprintf(efd, \"error: no accept labels defined \");",
4501 " fprintf(efd, \"in model (for option -a)\\n\");",
4507 " #ifdef HAS_ENABLED",
4508 " #error use of enabled() requires -DNOREDUCE",
4510 " #ifdef HAS_PCVALUE",
4511 " #error use of pcvalue() requires -DNOREDUCE",
4513 " #ifdef HAS_BADELSE",
4514 " #error use of 'else' combined with i/o stmnts requires -DNOREDUCE",
4517 " #error use of _last requires -DNOREDUCE",
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\");",
4527 " fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
4531 "#if SYNC>0 && defined(BFS)",
4532 " #warning use of rendezvous with BFS does not preserve all invalid endstates",
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\");",
4539 "#if defined(BITSTATE) && defined(REACH)",
4540 " #warning -DREACH is voided by -DBITSTATE",
4542 "#if defined(MA) && defined(REACH)",
4543 " #warning -DREACH is voided by -DMA",
4545 "#if defined(FULLSTACK) && defined(CNTRSTACK)",
4546 " #error cannot combine -DFULLSTACK and -DCNTRSTACK",
4548 "#if defined(VERI)",
4549 " #if ACCEPT_LAB>0",
4558 " && !state_tables)",
4559 " { fprintf(efd, \"warning: never claim + accept labels \");",
4560 " fprintf(efd, \"requires -a flag to fully verify\\n\");",
4563 " if (!state_tables",
4568 " { fprintf(efd, \"warning: verification in BFS mode \");",
4569 " fprintf(efd, \"is restricted to safety properties\\n\");",
4582 " && !state_tables)",
4583 " { fprintf(efd, \"hint: this search is more efficient \");",
4584 " fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
4590 " { if (!fairness)",
4591 " { S_A = 1; /* _a_t */",
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 */",
4600 " signal(SIGINT, stopped);",
4603 " trail = (Trail *) emalloc(6*sizeof(Trail));",
4606 " trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
4607 " trail++; /* protect trpt-1 refs at depth 0 */",
4610 " if (vprefix > 0)",
4612 " sprintf(nm, \"%%s.svd\", PanSource);",
4613 " if ((svfd = creat(nm, TMODE)) < 0)",
4614 " { fprintf(efd, \"couldn't create %%s\\n\", nm);",
4621 "#if SYNC>0 && ASYNC==0",
4628 "}", /* end of main() */
4633 " fprintf(fd, \"%%s\\n\", SpinVersion);",
4634 " fprintf(fd, \"Valid Options are:\\n\");",
4637 " fprintf(fd, \"\t-a -> is disabled by -DNP \");",
4638 " fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
4640 " fprintf(fd, \"\t-a find acceptance cycles\\n\");",
4643 " fprintf(fd, \"\t-a,-l,-f -> are disabled by -DSAFETY\\n\");",
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\");",
4653 " fprintf(fd, \"\t-Ffile use 'file' to store disk-stack\\n\");",
4656 " fprintf(fd, \"\t-f add weak fairness (to -a or -l)\\n\");",
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\");",
4663 " fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
4666 " fprintf(fd, \"\t-LN set scheduling restriction to N (default 10)\\n\");",
4670 " fprintf(fd, \"\t-l find non-progress cycles\\n\");",
4672 " fprintf(fd, \"\t-l find non-progress cycles -> \");",
4673 " fprintf(fd, \"disabled, requires \");",
4674 " fprintf(fd, \"compilation with -DNP\\n\");",
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\");",
4683 " fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
4684 " fprintf(fd, \"\t-n no listing of unreached states\\n\");",
4686 " fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
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\");",
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\");",
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\");",
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\");",
4711 " fprintf(fd, \"\t-zN handoff states below depth N to 2nd cpu (multi_core)\\n\");",
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\");",
4718 " multi_usage(fd);",
4724 "Malloc(unsigned long n)",
4727 " if (memcnt+ (double) n > memlim) goto err;",
4730 " tmp = (char *) malloc(n);",
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)
4739 " tmp = (char *) sbrk(n);",
4740 " if (tmp == (char *) -ONE_L)",
4746 " printf(\"pan: out of memory\\n\");",
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\",",
4754 " printf(\"hint: to reduce memory, recompile with\\n\");",
4756 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
4758 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
4761 " printf(\"hint: to reduce memory, recompile with\\n\");",
4763 " printf(\" -DCOLLAPSE # good, fast compression, or\\n\");",
4765 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
4767 " printf(\" -DHC # hash-compaction, approximation\\n\");",
4769 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
4773 " #ifdef FULL_TRAIL",
4774 " printf(\" omit -DFULL_TRAIL or use pan -c0 to reduce memory\\n\");",
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\");",
4783 " memcnt += (double) n;",
4787 "#define CHUNK (100*VECTORSZ)",
4790 "emalloc(unsigned long n) /* never released or reallocated */",
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;",
4799 " have = Malloc(grow);",
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 *);",
4810 " fragment += (double) left;",
4814 " have += (long) n;",
4815 " left -= (long) n;",
4816 " memset(tmp, 0, n);",
4821 "Uerror(char *str)",
4822 "{ /* always fatal */",
4825 " sudden_stop(\"Uerror\");",
4829 "#if defined(MA) && !defined(SAFETY)",
4832 "{ Trans *t; uchar ot, _m; int tt; short II;",
4836 " uchar oat = now._a_t;",
4837 " now._a_t &= ~(1|16|32);",
4838 " memcpy((char *) &comp_now, (char *) &now, vsize);",
4842 " trpt = getframe(depth);",
4845 " printf(\"%%d State: \", depth);",
4846 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
4847 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
4848 " printf(\"\\n\");",
4851 " if (trpt->o_pm&128) /* fairness alg */",
4852 " { now._cnt[now._a_t&1] = trpt->bup.oval;",
4855 " trpt = getframe(depth);",
4864 " { int d; Trail *trl;",
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;",
4873 " now._last = (depth<1)?0:(trpt-1)->pr;",
4876 "#ifdef EVENT_TRACE",
4877 " now._event = trpt->o_event;",
4879 " if ((now._a_t&1) && depth <= A_depth)",
4880 " { now._a_t &= ~(1|16|32);",
4881 " if (fairness) now._a_t |= 2; /* ? */",
4883 " goto CameFromHere; /* checkcycles() */",
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);",
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);",
4900 " trpt = getframe(depth);",
4904 " /* reached[ot][t->st] = 1; 3.4.13 */",
4905 " ((P0 *)this)->_p = tt;",
4907 " if ((trpt->o_pm&32))",
4910 " if (now._cnt[now._a_t&1] == 0)",
4911 " now._cnt[now._a_t&1] = 1;",
4913 " now._cnt[now._a_t&1] += 1;",
4916 " if (trpt->o_pm&8)",
4917 " { now._a_t &= ~2;",
4918 " now._cnt[now._a_t&1] = 0;",
4920 " if (trpt->o_pm&16)",
4924 " if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)",
4926 " if (depth > 0) goto Up;",
4930 "static char unwinding;",
4932 "uerror(char *str)",
4933 "{ static char laststr[256];",
4936 " if (unwinding) return; /* 1.4.2 */",
4937 " if (strncmp(str, laststr, 254))",
4939 " cpu_printf(\"pan: %%s (at depth %%ld)\\n\", str,",
4941 " printf(\"pan: %%s (at depth %%ld)\\n\", str,",
4944 " (nr_handoffs * z_handoff) + ",
4946 " ((depthfound==-1)?depth:depthfound));",
4947 " strncpy(laststr, str, 254);",
4950 " if (readtrail) { wrap_trail(); return; }",
4952 " is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
4954 " { depth++; trpt++;", /* include failed step */
4956 " if ((every_error != 0)",
4957 " || errors == upto)",
4959 "#if defined(MA) && !defined(SAFETY)",
4961 " { int od = depth;",
4963 " depthfound = Unwind();",
4969 " writing_trail = 1;",
4972 " if (depth > 1) trpt--;",
4974 " if (depth > 1) trpt++;",
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 */",
4986 " if (search_terminated != NULL)",
4987 " { *search_terminated |= 4; /* uerror */",
4989 " writing_trail = 0;",
4993 " { depth--; trpt--; /* undo */",
4996 " if (iterative != 0 && maxdepth > 0)",
4997 " { maxdepth = (iterative == 1)?(depth-1):(depth/2);",
4999 " printf(\"pan: reducing search depth to %%ld\\n\",",
5003 " if (errors >= upto && upto != 0)",
5006 " sudden_stop(\"uerror\");",
5010 " depthfound = -1;",
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)",
5017 " { if (strcmp(T->tp, \".(goto)\") == 0",
5018 " || strncmp(T->tp, \"goto :\", 6) == 0)",
5019 " return 1; /* not reported */",
5021 " printf(\"\\tline %%d\", lno);",
5023 " for (j = 0; j < sizeof(mp); j++)",
5024 " if (i >= mp[j].from && i <= mp[j].upto)",
5025 " { printf(\", \\\"%%s\\\"\", mp[j].fnm);",
5028 " printf(\", state %%d\", i);",
5029 " if (strcmp(T->tp, \"\") != 0)",
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 */",
5041 "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
5044 " if (M == VERI && !verbose) return;",
5046 " printf(\"unreached in proctype %%s\\n\", procname[M]);",
5047 " for (i = 1; i < N; i++)",
5049 " if (which[i] == 0 /* && trans[M][i] */)",
5051 " if (which[i] == 0",
5052 " && (mapstate[M][i] == 0",
5053 " || which[mapstate[M][i]] == 0))",
5055 " m += xrefsrc((int) src[i], mp, M, i);",
5058 " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
5060 "#if NCORE>1 && !defined(SEP_STATE)",
5061 "static long rev_trail_cnt;",
5063 "#ifdef FULL_TRAIL",
5065 "rev_trail(int fd, volatile Stack_Tree *st_tr)",
5066 "{ long j; char snap[64];",
5071 " rev_trail(fd, st_tr->prv);",
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]);",
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\");",
5086 " } else /* handoff point */",
5088 " { write(fd, \"-1:-1:-1\\n\", 9);",
5091 "#endif", /* FULL_TRAIL */
5092 "#endif", /* NCORE>1 */
5097 "#if defined VERI || defined(MERGED)",
5100 "#if NCORE==1 || defined(SEP_STATE) || !defined(FULL_TRAIL)",
5104 " fd = make_trail();",
5105 " if (fd < 0) return;",
5107 " sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
5108 " write(fd, snap, strlen(snap));",
5111 " sprintf(snap, \"-4:-4:-4\\n\");",
5112 " write(fd, snap, strlen(snap));",
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);",
5120 " i = 1; /* trail starts at position 1 */",
5121 " #if NCORE>1 && defined(SEP_STATE)",
5122 " if (cur_Root.m_vsize > 0) { i++; depth++; }",
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\");",
5141 " cpu_printf(\"pan: wrote trailfile\\n\");",
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;",
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;",
5158 " svtack = svtack->nxt;",
5160 " svtack->o_boq = boq;",
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]));",
5168 " cpu_printf(\"%%d: sv_save\\n\", depth);",
5172 "sv_restor(void) /* pop state vector from save stack */",
5174 " memcpy((char *)&now, svtack->body, svtack->o_delta);",
5176 " boq = svtack->o_boq;",
5179 "#if defined(C_States) && (HAS_TRACK==1)",
5181 " c_unstack((uchar *) &(svtack->c_stack[0]));",
5183 " c_revert((uchar *) &(now.c_state[0]));",
5186 " if (vsize != svtack->o_delta)",
5187 " Uerror(\"sv_restor\");",
5188 " if (!svtack->lst)",
5189 " Uerror(\"error: v_restor\");",
5190 " svtack = svtack->lst;",
5192 " cpu_printf(\" sv_restor\\n\");",
5197 "{ int i; char *z = (char *) &now;\n",
5198 " proc_offset[h] = stack->o_offset;",
5199 " proc_skip[h] = (uchar) stack->o_skip;",
5201 " p_name[h] = stack->o_name;",
5204 " for (i = vsize + stack->o_skip; i > vsize; i--)",
5205 " Mask[i-1] = 1; /* align */",
5207 " vsize += stack->o_skip;",
5208 " memcpy(z+vsize, stack->body, stack->o_delta);",
5209 " vsize += stack->o_delta;",
5211 " now._vsz = vsize;",
5214 " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
5215 " Mask[vsize - i] = 1; /* pad */",
5216 " Mask[proc_offset[h]] = 1; /* _pid */",
5218 " if (BASE > 0 && h > 0)",
5219 " ((P0 *)pptr(h))->_pid = h-BASE;",
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;",
5233 "{ char *z = (char *) &now;",
5237 " q_offset[now._nr_qs] = stack->o_offset;",
5238 " q_skip[now._nr_qs] = (uchar) stack->o_skip;",
5240 " q_name[now._nr_qs] = stack->o_name;",
5242 " vsize += stack->o_skip;",
5243 " memcpy(z+vsize, stack->body, stack->o_delta);",
5244 " vsize += stack->o_delta;",
5246 " now._vsz = vsize;",
5248 " now._nr_qs += 1;",
5250 " k_end = stack->o_offset;",
5251 " k = k_end - stack->o_skip;",
5254 " if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
5257 " for ( ; k < k_end; k++)",
5260 " if (!stack->lst) /* debugging */",
5261 " Uerror(\"error: q_restor\");",
5262 " stack = stack->lst;",
5265 "typedef struct IntChunks {",
5267 " struct IntChunks *nxt;",
5269 "IntChunks *filled_chunks[512];",
5270 "IntChunks *empty_chunks[512];",
5273 "grab_ints(int nr)",
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;",
5280 " { z = (IntChunks *) emalloc(sizeof(IntChunks));",
5281 " z->ptr = (int *) emalloc(nr * sizeof(int));",
5283 " z->nxt = empty_chunks[nr];",
5284 " empty_chunks[nr] = z;",
5288 "ungrab_ints(int *p, int nr)",
5290 " if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");",
5291 " z = empty_chunks[nr];",
5292 " empty_chunks[nr] = empty_chunks[nr]->nxt;",
5294 " z->nxt = filled_chunks[nr];",
5295 " filled_chunks[nr] = z;",
5298 "delproc(int sav, int h)",
5301 " int o_vsize = vsize;",
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])",
5309 " d = vsize - proc_offset[h];",
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;",
5319 " stack = stack->nxt;",
5320 " stack->o_offset = proc_offset[h];",
5321 "#if VECTORSZ>32000",
5322 " stack->o_skip = (int) proc_skip[h];",
5324 " stack->o_skip = (short) proc_skip[h];",
5327 " stack->o_name = p_name[h];",
5329 " stack->o_delta = d;",
5330 " stack->o_delqs = i;",
5331 " memcpy(stack->body, (char *)pptr(h), d);",
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];",
5338 " now._vsz = vsize;",
5341 " for (i = vsize; i < o_vsize; i++)",
5342 " Mask[i] = 0; /* reset */",
5348 "{ int h = now._nr_qs - 1;",
5349 " int d = vsize - q_offset[now._nr_qs - 1];",
5351 " int k, o_vsize = vsize;",
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;",
5362 " stack = stack->nxt;",
5363 " stack->o_offset = q_offset[h];",
5364 "#if VECTORSZ>32000",
5365 " stack->o_skip = (int) q_skip[h];",
5367 " stack->o_skip = (short) q_skip[h];",
5370 " stack->o_name = q_name[h];",
5372 " stack->o_delta = d;",
5373 " memcpy(stack->body, (char *)qptr(h), d);",
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];",
5380 " now._vsz = vsize;",
5383 " for (k = vsize; k < o_vsize; k++)",
5384 " Mask[k] = 0; /* reset */",
5390 " for (i = 0; i < (int) now._nr_qs; i++)",
5391 " { if (q_sz(i) > 0)",
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])",
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\");",
5415 "checkcycles(void)",
5416 "{ uchar o_a_t = now._a_t;",
5421 " uchar o_cnt = now._cnt[1];",
5425 " struct H_el *sv = trpt->ostate; /* save */",
5427 " uchar prov = trpt->proviso; /* save */",
5431 " { int i; uchar *v = (uchar *) &now;",
5432 " printf(\" set Seed state \");",
5434 " if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
5435 " now._cnt[0], now._cnt[1], now._nr_pr);",
5437 " /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */",
5438 " printf(\"\\n\");",
5440 " printf(\"%%d: cycle check starts\\n\", depth);",
5442 " now._a_t |= (1|16|32);",
5443 " /* 1 = 2nd DFS; (16|32) to help hasher */",
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 */",
5452 " now._cnt[1] = now._cnt[0];",
5455 " memcpy((char *)&A_Root, (char *)&now, vsize);",
5456 " A_depth = depthfound = depth;",
5459 " mem_put_acc();", /* handoff accept states */
5462 " o_limit = trpt->sched_limit;",
5463 " trpt->sched_limit = 0;",
5465 " new_state(); /* start 2nd DFS */",
5467 " trpt->sched_limit = o_limit;",
5471 " now._a_t = o_a_t;",
5473 " now._cnt[1] = o_cnt;",
5475 " A_depth = 0; depthfound = -1;",
5477 " printf(\"%%d: cycle check returns\\n\", depth);",
5481 " trpt->ostate = sv; /* restore */",
5483 " trpt->proviso = prov;",
5488 "#if defined(FULLSTACK) && defined(BITSTATE)",
5489 "struct H_el *Free_list = (struct H_el *) 0;",
5491 "onstack_init(void) /* to store stack states in a bitstate search */",
5492 "{ S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(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)",
5501 " last->nxt = v->nxt;",
5503 "gotcha: Free_list = v->nxt;",
5513 " /* new: second try */",
5514 " v = Free_list;", /* try to avoid emalloc */
5515 " if (v && ((int) v->tagged >= n))",
5519 " return (struct H_el *)",
5520 " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
5526 "grab_state(int n)",
5527 "{ struct H_el *grab_shared(int);",
5528 " return grab_shared(sizeof(struct H_el)+n-sizeof(unsigned));",
5531 " #ifndef AUTO_RESIZE",
5532 " #define grab_state(n) (struct H_el *) \\",
5533 " emalloc(sizeof(struct H_el)+n-sizeof(unsigned long));",
5536 " grab_state(int n)",
5537 " { struct H_el *p;",
5538 " int cnt = sizeof(struct H_el)+n-sizeof(unsigned long);",
5540 " if (reclaim_size >= cnt+WS)",
5541 " { if ((cnt & (WS-1)) != 0) /* alignment */",
5542 " { cnt += WS - (cnt & (WS-1));",
5544 " p = (struct H_el *) reclaim_mem;",
5545 " reclaim_mem += cnt;",
5546 " reclaim_size -= cnt;",
5547 " memset(p, 0, cnt);",
5549 " { p = (struct H_el *) emalloc(cnt);",
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);",
5564 "#if NCORE>1 && !defined(SEP_STATE)",
5565 " enter_critical(CS_ID); /* uses spinlock - 1..128 */",
5568 " tmp = H_tab[j1];",
5570 " { tmp = grab_state(n);",
5571 " H_tab[j1] = tmp;",
5573 " for ( ;; olst = tmp, tmp = tmp->nxt)",
5574 " { m = memcmp(((char *)&(tmp->state)), v, n);",
5575 " if (n == tmp->ln)",
5581 "Insert: ntmp = grab_state(n);",
5582 " ntmp->nxt = tmp;",
5584 " H_tab[j1] = ntmp;",
5586 " olst->nxt = ntmp;",
5589 " } else if (!tmp->nxt)",
5591 "Append: tmp->nxt = grab_state(n);",
5597 " if (n < tmp->ln)",
5599 " else if (!tmp->nxt)",
5602 " m = ++ncomps[tp];",
5604 " tmp->tagged = m;",
5608 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
5611 " memcpy(((char *)&(tmp->state)), v, n);",
5615 "#if NCORE>1 && !defined(SEP_STATE)",
5616 " leave_critical(CS_ID); /* uses spinlock */",
5620 " return tmp->tagged;",
5622 " return tmp->st_id;",
5627 "compress(char *vin, int nin) /* collapse compression */",
5628 "{ char *w, *v = (char *) &comp_now;",
5630 " unsigned long n;",
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 *);",
5638 " *v++ = now._a_t;",
5641 " for (i = 0; i < NFAIR; i++)",
5642 " *v++ = now._cnt[i];",
5647 "#ifndef JOINPROCS",
5648 " for (i = 0; i < (int) now._nr_pr; i++)",
5649 " { n = col_p(i, (char *) 0);",
5651 " nbytes[nbytelen] = 0;",
5653 " nbytes[nbytelen] = 1;",
5654 " *v++ = ((P0 *) pptr(i))->_t;",
5657 " if (n >= (1<<8))",
5658 " { nbytes[nbytelen]++;",
5659 " *v++ = (n>>8)&255;",
5661 " if (n >= (1<<16))",
5662 " { nbytes[nbytelen]++;",
5663 " *v++ = (n>>16)&255;",
5665 " if (n >= (1<<24))",
5666 " { nbytes[nbytelen]++;",
5667 " *v++ = (n>>24)&255;",
5673 " for (i = 0; i < (int) now._nr_pr; i++)",
5674 " x += col_p(i, x);",
5675 " n = ordinal(scratch, x-scratch, 2); /* procs */",
5677 " nbytes[nbytelen] = 0;",
5678 " if (n >= (1<<8))",
5679 " { nbytes[nbytelen]++;",
5680 " *v++ = (n>>8)&255;",
5682 " if (n >= (1<<16))",
5683 " { nbytes[nbytelen]++;",
5684 " *v++ = (n>>16)&255;",
5686 " if (n >= (1<<24))",
5687 " { nbytes[nbytelen]++;",
5688 " *v++ = (n>>24)&255;",
5693 " for (i = 0; i < (int) now._nr_qs; i++)",
5694 " { n = col_q(i, (char *) 0);",
5695 " nbytes[nbytelen] = 0;",
5697 " if (n >= (1<<8))",
5698 " { nbytes[nbytelen]++;",
5699 " *v++ = (n>>8)&255;",
5701 " if (n >= (1<<16))",
5702 " { nbytes[nbytelen]++;",
5703 " *v++ = (n>>16)&255;",
5705 " if (n >= (1<<24))",
5706 " { nbytes[nbytelen]++;",
5707 " *v++ = (n>>24)&255;",
5714 " /* 3 = _a_t, _nr_pr, _nr_qs */",
5715 " w = (char *) &now + 3 * sizeof(uchar);",
5720 "#if VECTORSZ<65536",
5721 " w = (char *) &(now._vsz) + sizeof(unsigned short);",
5723 " w = (char *) &(now._vsz) + sizeof(unsigned long);",
5727 " *x++ = now._nr_pr;",
5728 " *x++ = now._nr_qs;",
5730 " if (now._nr_qs > 0 && qptr(0) < pptr(0))",
5731 " n = qptr(0) - (uchar *) w;",
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;",
5738 " for (i = 0; i < (int) now._nr_qs; i++)",
5739 " x += col_q(i, x);",
5743 " for (i = 0, j = 6; i < nbytelen; i++)",
5749 " *x |= (nbytes[i] << j);",
5752 " for (j = 0; j < WS-1; j++)",
5755 " n = ordinal(scratch, x-scratch, 0); /* globals */",
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 */",
5762 " for (i = 0; i < WS-1; i++)",
5766 " printf(\"collapse %%d -> %%d\\n\",",
5767 " vsize, v - (char *)&comp_now);",
5769 " return v - (char *)&comp_now;",
5773 "#if !defined(NOCOMP)",
5775 "compress(char *vin, int n) /* default compression */",
5779 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
5782 " { delta++; /* _a_t */",
5784 " if (S_A > NFAIR)",
5785 " delta += NFAIR; /* _cnt[] */",
5789 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
5792 " memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
5798 " char *v = (char *) &comp_now;",
5800 " #ifndef NO_FAST_C", /* disable faster compress */
5801 " int r = 0, unroll = n/8;", /* most sv are much longer */
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++];",
5823 " r = n - i; /* the rest, at most 7 */",
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++];",
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;",
5846 " default: Uerror(\"unexpected wordsize\");",
5851 " { for (i = 0; i < n; i++, vv++)",
5852 " if (!Mask[i]) *v++ = *vv;",
5853 " for (i = 0; i < WS-1; i++)",
5858 " printf(\"compress %%d -> %%d\\n\",",
5859 " n, v - (char *)&comp_now);",
5861 " return v - (char *)&comp_now;",
5866 "#if defined(FULLSTACK) && defined(BITSTATE)",
5868 "#if !defined(onstack_now)",
5869 "int onstack_now(void) {}", /* to suppress compiler errors */
5871 "#if !defined(onstack_put)",
5872 "void onstack_put(void) {}", /* for this invalid combination */
5874 "#if !defined(onstack_zap)",
5875 "void onstack_zap(void) {}", /* of directives */
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;",
5887 " nv = (char *) &comp_now;",
5888 " n = compress((char *)&now, vsize);",
5890 "#if defined(BITSTATE) && defined(LC)",
5891 " nv = (char *) &comp_now;",
5892 " n = compact_stack((char *)&now, vsize);",
5894 " nv = (char *) &now;",
5898 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
5899 " s_hash((uchar *)nv, n);",
5902 " for (v = S_Tab[j1]; v; Zh++, last=v, v=v->nxt)",
5903 " { m = memcmp(&(v->state), nv, n);",
5911 " #if defined(BITSTATE) && NCORE>1",
5912 " /* seen this happen, likely harmless, but not yet understood */",
5913 " if (warned == 0)",
5915 " { /* Uerror(\"stack out of wack - zap\"); */",
5916 " cpu_printf(\"pan: warning, stack incomplete\\n\");",
5924 " last->nxt = v->nxt;",
5926 " S_Tab[j1] = v->nxt;",
5927 " v->tagged = (unsigned) n;",
5928 "#if !defined(NOREDUCE) && !defined(SAFETY)",
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)",
5938 " { v->nxt = Free_list;",
5950 "onstack_put(void)",
5951 "{ struct H_el **tmp = H_tab;",
5953 " if (hstore((char *)&now, vsize) != 0)",
5954 "#if defined(BITSTATE) && defined(LC)",
5955 " printf(\"pan: warning, double stack entry\\n\");",
5958 " Uerror(\"cannot happen - unstack_put\");",
5962 " trpt->ostate = Lstate;",
5966 "onstack_now(void)",
5967 "{ struct H_el *tmp;",
5968 " struct H_el **tmp2 = H_tab;",
5969 " char *v; int n, m = 1;\n",
5972 "#if defined(BITSTATE) && defined(LC)",
5973 " v = (char *) &comp_now;",
5974 " n = compact_stack((char *)&now, vsize);",
5976 " v = (char *) &now;",
5980 " v = (char *) &comp_now;",
5981 " n = compress((char *)&now, vsize);",
5983 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
5984 " s_hash((uchar *)v, n);",
5987 " for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
5988 " { m = memcmp(((char *)&(tmp->state)),v,n);",
5990 " { Lstate = (struct H_el *) tmp;",
5994 " return (m == 0);",
6005 " { void r_xpoint(void);",
6009 " dfa_init((unsigned short) (MA+a_cycles));",
6010 "#if NCORE>1 && !defined(COLLAPSE)",
6012 " { void init_HT(unsigned long);",
6018 " #if !defined(MA) || defined(COLLAPSE)",
6021 " { void init_HT(unsigned long);",
6022 " init_HT((unsigned long) (ONE_L<<ssize)*sizeof(struct H_el *));",
6025 " H_tab = (struct H_el **)",
6026 " emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
6031 "#if !defined(BITSTATE) || defined(FULLSTACK)",
6035 "dumpstate(int wasnew, char *v, int n, int tag)",
6039 " { printf(\"\tstate tags %%d (%%d::%%d): \",",
6040 " V_A, wasnew, v[0]);",
6042 " printf(\" %%d \", tag);",
6044 " printf(\"\\n\");",
6049 " printf(\"\t State: \");",
6050 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
6051 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
6053 " printf(\"\\n\tVector: \");",
6054 " for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
6055 " printf(\"\\n\");",
6062 "gstore(char *vin, int nin, uchar pbit)",
6064 " int ret_val = 1;",
6066 " static uchar Info[MA+1];",
6068 " n = compress(vin, nin);",
6069 " v = (uchar *) &comp_now;",
6075 " { printf(\"pan: error, MA too small, recompile pan.c\");",
6076 " printf(\" with -DMA=N with N>%%d\\n\", n);",
6077 " Uerror(\"aborting\");",
6079 " if (n > (int) maxgs)",
6080 " { maxgs = (unsigned int) n;",
6082 " for (i = 0; i < n; i++)",
6083 " { Info[i] = v[i];",
6085 " for ( ; i < MA-1; i++)",
6088 " Info[MA-1] = pbit;",
6089 " if (a_cycles) /* place _a_t at the end */",
6090 " { Info[MA] = Info[0];",
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 */",
6099 " if (!dfa_store(Info))",
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 */",
6107 " if (!dfa_member(MA-1))",
6110 " printf(\"intersected 1st dfs stack\\n\");",
6116 " printf(\"new state\\n\");",
6122 " { Info[MA-1] = 1; /* proviso bit */",
6124 " trpt->proviso = dfa_member(MA-1);",
6126 " Info[MA-1] = 4; /* off-stack bit */",
6127 " if (dfa_member(MA-1))",
6128 " { ret_val = 1; /* off-stack */",
6130 " printf(\"old state\\n\");",
6133 " { ret_val = 2; /* on-stack */",
6135 " printf(\"on-stack\\n\");",
6143 " printf(\"old state\\n\");",
6146 "#if NCORE>1 && !defined(SEP_STATE)",
6147 " leave_critical(GLOBAL_LOCK);",
6149 " return ret_val; /* old state */",
6153 "#if defined(BITSTATE) && defined(LC)",
6155 "compact_stack(char *vin, int n)", /* special case of HC4 */
6157 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
6159 " delta++; /* room for state[0] |= 128 */",
6161 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
6163 " memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
6164 " delta += WS; /* use all available bits */",
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;",
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);",
6183 " { v = vin; n = nin;",
6186 " v = vin; n = nin;",
6189 " v = (char *) &comp_now;",
6191 " rem_a = now._a_t;", /* new 5.0 */
6192 " now._a_t = 0;", /* for hashing/state matching to work right */
6194 " n = compress(vin, nin);", /* with HC, this calls s_hash -- but on vin, not on v... */
6196 " now._a_t = rem_a;", /* new 5.0 */
6198 /* with HC4 -a, compress copies K1 and K2 into v[], leaving v[0] free for the a-bit */
6201 " { v[0] = 0; /* _a_t */",
6203 " if (S_A > NFAIR)",
6204 " for (m = 0; m < NFAIR; m++)",
6205 " v[m+1] = 0; /* _cnt[] */",
6211 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
6212 " s_hash((uchar *)v, n);",
6214 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6215 " enter_critical(CS_ID); /* uses spinlock */",
6218 " tmp = H_tab[j1];",
6220 " { tmp = grab_state(n);",
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);",
6229 " return 1; /* allow normal termination */",
6232 " H_tab[j1] = tmp;",
6234 " { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
6235 " { /* skip the _a_t and the _cnt bytes */",
6237 " if (tmp->ln != 0)",
6238 " { if (!tmp->nxt) goto Append;",
6242 " m = memcmp(((char *)&(tmp->state)) + S_A, ",
6243 " v + S_A, n - S_A);",
6254 " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
6255 " { wasnew = 1; nShadow++;",
6256 " ((char *)&(tmp->state))[0] |= V_A;",
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 */",
6268 " ci++; /* skip over _a_t */",
6269 " bp = 1 << bp; /* the bit mask */",
6270 " if ((((char *)&(tmp->state))[ci] & bp)==0)",
6275 " ((char *)&(tmp->state))[ci] |= bp;",
6278 " /* else: wasnew == 0, i.e., old state */",
6285 " Lstate = (struct H_el *) tmp;",
6289 "#ifndef SAFETY", /* or else wasnew == 0 */
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)",
6300 " printf(\"cpu%%d: \", core_id);",
6302 " printf(\"1st dfs-stack intersected on state %%d+\\n\",",
6303 " (int) tmp->st_id);",
6306 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6307 " leave_critical(CS_ID);",
6314 " printf(\"cpu%%d: \", core_id);",
6316 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
6319 " dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
6321 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6322 " leave_critical(CS_ID);",
6327 " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
6328 " { Lstate = (struct H_el *) tmp;",
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)",
6335 " && depth > A_depth",
6336 /* new (Zhang's example) */
6338 " && (!fairness || now._cnt[1] <= 1)",
6346 " printf(\"cpu%%d: \", core_id);",
6348 " printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
6351 " dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
6353 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6354 " leave_critical(CS_ID);",
6356 " return 2; /* match on stack */",
6363 " printf(\"cpu%%d: \", core_id);",
6365 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
6368 " dumpstate(1, (char *)&(tmp->state), n, 0);",
6370 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6371 " leave_critical(CS_ID);",
6378 " printf(\"cpu%%d: \", core_id);",
6380 " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
6383 " dumpstate(0, (char *)&(tmp->state), n, 0);",
6386 " if (tmp->D > depth)",
6387 " { tmp->D = depth;",
6390 " printf(\"cpu%%d: \", core_id);",
6392 " printf(\"\t\tReVisiting (from smaller depth)\\n\");",
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
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 */
6408 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6409 " leave_critical(CS_ID);",
6414 "#if (defined(BFS) && defined(Q_PROVISO)) || NCORE>1",
6415 " Lstate = (struct H_el *) tmp;",
6417 "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
6418 " leave_critical(CS_ID);",
6420 " return 1; /* match outside stack */",
6421 " } else if (m < 0)",
6422 " { /* insert state before tmp */",
6423 " ntmp = grab_state(n);",
6427 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6428 " leave_critical(CS_ID);",
6430 " return 1; /* allow normal termination */",
6433 " ntmp->nxt = tmp;",
6435 " H_tab[j1] = ntmp;",
6437 " olst->nxt = ntmp;",
6440 " } else if (!tmp->nxt)",
6441 " { /* append after tmp */",
6445 " tmp->nxt = grab_state(n);",
6449 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6450 " leave_critical(CS_ID);",
6452 " return 1; /* allow normal termination */",
6460 " tmp->st_id = (unsigned) nstates;",
6462 " printf(\"cpu%%d: \", core_id);",
6465 " printf(\" Push state %%d\\n\", ((int) nstates) - 1);",
6467 " printf(\" New state %%d\\n\", (int) nstates);",
6470 "#if !defined(SAFETY) || defined(REACH)",
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);",
6483 " { ci = (NFAIR - 1) - ci;",
6484 " bp = 7 - bp; /* bp = 0..7 */",
6486 " v[1+ci] = 1 << bp;",
6492 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
6495 " memcpy(((char *)&(tmp->state)), v, n);",
6497 " tmp->tagged = (S_A)?V_A:(depth+1);",
6499 " dumpstate(-1, v, n, tmp->tagged);",
6501 " Lstate = (struct H_el *) tmp;",
6504 " dumpstate(-1, v, n, 0);",
6507 " Lstate = (struct H_el *) tmp;",
6511 "/* #if NCORE>1 && !defined(SEP_STATE) */",
6513 " #ifdef V_PROVISO",
6514 " tmp->cpu_id = core_id;",
6516 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
6517 " leave_critical(CS_ID);",
6524 "#include TRANSITIONS",