/***** spin: pangen1.h *****/ /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */ /* All Rights Reserved. This software is for educational purposes only. */ /* No guarantee whatsoever is expressed or implied by the distribution of */ /* this code. Permission is given to distribute this code provided that */ /* this introductory message is not removed and no monies are exchanged. */ /* Software written by Gerard J. Holzmann. For tool documentation see: */ /* http://spinroot.com/ */ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ /* (c) 2007-2011: additions, enhancements, and bugfixes GJH */ static char *Code2a[] = { /* the tail of procedure run() */ " if (state_tables)", " { if (dodot) exit(0);", " printf(\"\\nTransition Type: \");", " printf(\"A=atomic; D=d_step; L=local; G=global\\n\");", " printf(\"Source-State Labels: \");", " printf(\"p=progress; e=end; a=accept;\\n\");", "#ifdef MERGED", " printf(\"Note: statement merging was used. Only the first\\n\");", " printf(\" stmnt executed in each merge sequence is shown\\n\");", " printf(\" (use spin -a -o3 to disable statement merging)\\n\");", "#endif", " pan_exit(0);", " }", "#if defined(BFS) && defined(TRIX)", /* before iniglobals */ " { int i;", " for (i = 0; i < MAXPROC+1; i++)", " { processes[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));", " processes[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));", " }", " for (i = 0; i < MAXQ+1; i++)", " { channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));", " channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));", " } }", "#endif", " iniglobals(258); /* arg outside range of pids */", "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)", " if (!state_tables", "#ifdef HAS_CODE", " && !readtrail", "#endif", "#if NCORE>1", " && core_id == 0", "#endif", " )", " { printf(\"warning: for p.o. reduction to be valid \");", " printf(\"the never claim must be stutter-invariant\\n\");", " printf(\"(never claims generated from LTL \");", " printf(\"formulae are stutter-invariant)\\n\");", " }", "#endif", " UnBlock; /* disable rendez-vous */", "#ifdef BITSTATE", " if (udmem)", " { udmem *= 1024L*1024L;", " #if NCORE>1", " if (!readtrail)", " { void init_SS(unsigned long);", " init_SS((unsigned long) udmem);", " } else", " #endif", " SS = (uchar *) emalloc(udmem);", " bstore = bstore_mod;", " } else", " #if NCORE>1", " { void init_SS(unsigned long);", " init_SS(ONE_L<<(ssize-3));", " }", " #else", " SS = (uchar *) emalloc(ONE_L<<(ssize-3));", " #endif", "#else", /* if not BITSTATE */ " hinit();", "#endif", "#if defined(FULLSTACK) && defined(BITSTATE)", " onstack_init();", "#endif", "#if defined(CNTRSTACK) && !defined(BFS)", " LL = (uchar *) emalloc(ONE_L<<(ssize-3));", "#endif", " stack = (_Stack *) emalloc(sizeof(_Stack));", " svtack = (Svtack *) emalloc(sizeof(Svtack));", " /* a place to point for Pptr of non-running procs: */", " noqptr = noptr = (uchar *) emalloc(Maxbody * sizeof(char));", "#if defined(SVDUMP) && defined(VERBOSE)", " if (vprefix > 0)", " (void) write(svfd, (uchar *) &vprefix, sizeof(int));", "#endif", "#ifdef VERI", " Addproc(VERI); /* pid = 0 */", " #if NCLAIMS>1", " if (claimname != NULL)", " { whichclaim = find_claim(claimname);", " select_claim(whichclaim);", " }", " #endif", "#endif", " active_procs(); /* started after never */", "#ifdef EVENT_TRACE", " now._event = start_event;", " reached[EVENT_TRACE][start_event] = 1;", "#endif", "#ifdef HAS_CODE", " globinit();", "#endif", "#ifdef BITSTATE", "go_again:", "#endif", " do_the_search();", "#ifdef BITSTATE", " if (--Nrun > 0 && HASH_CONST[++HASH_NR])", " { printf(\"Run %%d:\\n\", HASH_NR);", " wrap_stats();", " printf(\"\\n\");", " if (udmem) /* Dillinger 3/2/09 */", " { memset(SS, 0, udmem);", " } else", " { memset(SS, 0, ONE_L<<(ssize-3));", " }", "#ifdef CNTRSTACK", " memset(LL, 0, ONE_L<<(ssize-3));", "#endif", "#ifdef FULLSTACK", " memset((uchar *) S_Tab, 0, ", " maxdepth*sizeof(struct H_el *));", "#endif", " nstates=nlinks=truncs=truncs2=ngrabs = 0;", " nlost=nShadow=hcmp = 0;", " Fa=Fh=Zh=Zn = 0;", " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;", " goto go_again;", " }", "#endif", "}", "#ifdef HAS_PROVIDED", "int provided(int, uchar, int, Trans *);", "#endif", "#if NCORE>1", "#define GLOBAL_LOCK (0)", "#ifndef CS_N", "#define CS_N (256*NCORE)", /* must be a power of 2 */ "#endif", "#ifdef NGQ", /* no global queue */ "#define NR_QS (NCORE)", "#define CS_NR (CS_N+1) /* 2^N + 1, nr critical sections */", "#define GQ_RD GLOBAL_LOCK", /* not really used in this mode */ "#define GQ_WR GLOBAL_LOCK", /* but just in case... */ "#define CS_ID (1 + (int) (j1_spin & (CS_N-1))) /* mask: 2^N - 1, zero reserved */", "#define QLOCK(n) (1+n)", /* overlaps first n zones of hashtable */ "#else", "#define NR_QS (NCORE+1)", /* add a global queue */ "#define CS_NR (CS_N+3)", /* 2 extra locks for global q */ "#define GQ_RD (1)", /* read access to global q */ "#define GQ_WR (2)", /* write access to global q */ "#define CS_ID (3 + (int) (j1_spin & (CS_N-1)))", "#define QLOCK(n) (3+n)",/* overlaps first n zones of hashtable */ "#endif", "", "void e_critical(int);", "void x_critical(int);", "", "#ifndef SEP_STATE", " #define enter_critical(w) e_critical(w)", " #define leave_critical(w) x_critical(w)", "#else", " #ifdef NGQ", " #define enter_critical(w) { if (w < 1+NCORE) e_critical(w); }", " #define leave_critical(w) { if (w < 1+NCORE) x_critical(w); }", " #else", " #define enter_critical(w) { if (w < 3+NCORE) e_critical(w); }", " #define leave_critical(w) { if (w < 3+NCORE) x_critical(w); }", " #endif", "#endif", "", "int", "cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */ "{ va_list args;", " enter_critical(GLOBAL_LOCK); /* printing */", " printf(\"cpu%%d: \", core_id);", " fflush(stdout);", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", " fflush(stdout);", " leave_critical(GLOBAL_LOCK);", " return 1;", "}", "#else", "int", "cpu_printf(const char *fmt, ...)", "{ va_list args;", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", " return 1;", "}", "#endif", #ifndef PRINTF "int", "Printf(const char *fmt, ...)", "{ /* Make sure the args to Printf", " * are always evaluated (e.g., they", " * could contain a run stmnt)", " * but do not generate the output", " * during verification runs", " * unless explicitly wanted", " * If this fails on your system", " * compile SPIN itself -DPRINTF", " * and this code is not generated", " */", "#ifdef HAS_CODE", " if (readtrail)", " { va_list args;", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", " return 1;", " }", "#endif", "#ifdef PRINTF", " va_list args;", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", "#endif", " return 1;", "}", #endif "extern void printm(int);", "#ifndef SC", "#define getframe(i) &trail[i];", "#else", "static long HHH, DDD, hiwater;", "static long CNT1, CNT2;", "static int stackwrite;", "static int stackread;", "static Trail frameptr;", "Trail *", "getframe(int d)", "{", " if (CNT1 == CNT2)", " return &trail[d];", "", " if (d >= (CNT1-CNT2)*DDD)", " return &trail[d - (CNT1-CNT2)*DDD];", "", " if (!stackread", " && (stackread = open(stackfile, 0)) < 0)", " { printf(\"getframe: cannot open %%s\\n\", stackfile);", " wrapup();", " }", " if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1", " || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))", " { printf(\"getframe: frame read error\\n\");", " wrapup();", " }", " return &frameptr;", "}", "#endif", "#if !defined(SAFETY) && !defined(BITSTATE)", "#if !defined(FULLSTACK) || defined(MA)", "#define depth_of(x) A_depth /* an estimate */", "#else", "int", "depth_of(struct H_el *s)", "{ Trail *t; int d;", " for (d = 0; d <= A_depth; d++)", " { t = getframe(d);", " if (s == t->ostate)", " return d;", " }", " printf(\"pan: cannot happen, depth_of\\n\");", " return depthfound;", "}", "#endif", "#endif", "#if NCORE>1", "extern void cleanup_shm(int);", "volatile unsigned int *search_terminated; /* to signal early termination */", /* * Meaning of bitflags in search_terminated: * 1 set by pan_exit * 2 set by wrapup * 4 set by uerror * 8 set by sudden_stop -- called after someone_crashed and [Uu]error * 16 set by cleanup_shm * 32 set by give_up -- called on signal * 64 set by proxy_exit * 128 set by proxy on write port failure * 256 set by proxy on someone_crashed * * Flags 8|32|128|256 indicate abnormal termination * * The flags are checked in 4 functions in the code: * sudden_stop() * someone_crashed() (proxy and pan version) * mem_hand_off() */ "#endif", "void", "pan_exit(int val)", "{ void stop_timer(void);", " if (signoff)", " { printf(\"--end of output--\\n\");", " }", "#if NCORE>1", " if (search_terminated != NULL)", " { *search_terminated |= 1; /* pan_exit */", " }", "#ifdef USE_DISK", " { void dsk_stats(void);", " dsk_stats();", " }", "#endif", " if (!state_tables && !readtrail)", " { cleanup_shm(1);", " }", "#endif", " if (val == 2)", " { val = 0;", " } else", " { stop_timer();", " }", "", "#ifdef C_EXIT", " C_EXIT; /* trust that it defines a fct */", "#endif", " exit(val);", "}", "#ifdef HAS_CODE", "static char tbuf[2][2048];", "", "char *", "transmognify(char *s)", "{ char *v, *w;", " int i, toggle = 0;", " if (!s || strlen(s) > 2047) return s;", " memset(tbuf[0], 0, 2048);", " memset(tbuf[1], 0, 2048);", " strcpy(tbuf[toggle], s);", " while ((v = strstr(tbuf[toggle], \"{c_code\")))", /* assign v */ " { *v = '\\0'; v++;", " strcpy(tbuf[1-toggle], tbuf[toggle]);", " for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;", " if (*w != '}') return s;", " *w = '\\0'; w++;", " for (i = 0; code_lookup[i].c; i++)", " if (strcmp(v, code_lookup[i].c) == 0", " && strlen(v) == strlen(code_lookup[i].c))", " { if (strlen(tbuf[1-toggle])", " + strlen(code_lookup[i].t)", " + strlen(w) > 2047)", " return s;", " strcat(tbuf[1-toggle], code_lookup[i].t);", " break;", " }", " strcat(tbuf[1-toggle], w);", " toggle = 1 - toggle;", " }", " tbuf[toggle][2047] = '\\0';", " return tbuf[toggle];", "}", "#else", "char * transmognify(char *s) { return s; }", "#endif", "#ifdef HAS_CODE", "void", "add_src_txt(int ot, int tt)", "{ Trans *t;", " char *q;", "", " for (t = trans[ot][tt]; t; t = t->nxt)", " { printf(\"\\t\\t\");", " q = transmognify(t->tp);", " for ( ; q && *q; q++)", " if (*q == '\\n')", " printf(\"\\\\n\");", " else", " putchar(*q);", " printf(\"\\n\");", " }", "}", "", "char *", "find_source(int tp, int s)", "{", " if (s >= flref[tp]->from", " && s <= flref[tp]->upto)", " { return flref[tp]->fnm;", " }", " return PanSource; /* i.e., don't know */", "}", "", "void", "wrap_trail(void)", "{ static int wrap_in_progress = 0;", " int i; short II;", " P0 *z;", "", " if (wrap_in_progress++) return;", "", " printf(\"spin: trail ends after %%ld steps\\n\", depth);", " if (onlyproc >= 0)", " { if (onlyproc >= now._nr_pr) { pan_exit(0); }", " II = onlyproc;", " z = (P0 *)pptr(II);", " printf(\"%%3ld:\tproc %%d (%%s) \",", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\" %%s:%%d\",", " find_source((int) z->_t, (int) z->_p),", " src_all[i].src[z->_p]);", " break;", " }", " printf(\" (state %%2d)\", z->_p);", " if (!stopstate[z->_t][z->_p])", " printf(\" (invalid end state)\");", " printf(\"\\n\");", " add_src_txt(z->_t, z->_p);", " pan_exit(0);", " }", " printf(\"#processes %%d:\\n\", now._nr_pr);", " if (depth < 0) depth = 0;", " for (II = 0; II < now._nr_pr; II++)", " { z = (P0 *)pptr(II);", " printf(\"%%3ld:\tproc %%d (%%s) \",", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\" %%s:%%d\",", " find_source((int) z->_t, (int) z->_p),", " src_all[i].src[z->_p]);", " break;", " }", " printf(\" (state %%2d)\", z->_p);", " if (!stopstate[z->_t][z->_p])", " printf(\" (invalid end state)\");", " printf(\"\\n\");", " add_src_txt(z->_t, z->_p);", " }", " c_globals();", " for (II = 0; II < now._nr_pr; II++)", " { z = (P0 *)pptr(II);", " c_locals(II, z->_t);", " }", "#ifdef ON_EXIT", " ON_EXIT;", "#endif", " pan_exit(0);", "}", "FILE *", "findtrail(void)", "{ FILE *fd;", " char fnm[512], *q;", " char MyFile[512];", /* avoid using a non-writable string */ " char MySuffix[16];", " int try_core;", " int candidate_files;", "", " if (trailfilename != NULL)", " { fd = fopen(trailfilename, \"r\");", " if (fd == NULL)", " { printf(\"pan: cannot find %%s\\n\", trailfilename);", " pan_exit(1);", " } /* else */", " goto success;", " }", "talk:", " try_core = 1;", " candidate_files = 0;", " tprefix = \"trail\";", " strcpy(MyFile, TrailFile);", " do { /* see if there's more than one possible trailfile */", " if (whichtrail)", " { sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, whichtrail, tprefix);", " fd = fopen(fnm, \"r\");", " if (fd != NULL)", " { candidate_files++;", " if (verbose==100)", " printf(\"trail%%d: %%s\\n\",", " candidate_files, fnm);", " fclose(fd);", " }", " if ((q = strchr(MyFile, \'.\')) != NULL)", " { *q = \'\\0\';", /* e.g., strip .pml */ " sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, whichtrail, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " if (fd != NULL)", " { candidate_files++;", " if (verbose==100)", " printf(\"trail%%d: %%s\\n\",", " candidate_files, fnm);", " fclose(fd);", " } }", " } else", " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " fd = fopen(fnm, \"r\");", " if (fd != NULL)", " { candidate_files++;", " if (verbose==100)", " printf(\"trail%%d: %%s\\n\",", " candidate_files, fnm);", " fclose(fd);", " }", " if ((q = strchr(MyFile, \'.\')) != NULL)", " { *q = \'\\0\';", /* e.g., strip .pml */ " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " if (fd != NULL)", " { candidate_files++;", " if (verbose==100)", " printf(\"trail%%d: %%s\\n\",", " candidate_files, fnm);", " fclose(fd);", " } } }", " tprefix = MySuffix;", " sprintf(tprefix, \"cpu%%d_trail\", try_core++);", " } while (try_core <= NCORE);", "", " if (candidate_files != 1)", " { if (verbose != 100)", " { printf(\"error: there are %%d trail files:\\n\",", " candidate_files);", " verbose = 100;", " goto talk;", " } else", " { printf(\"pan: rm or mv all except one\\n\");", " exit(1);", " } }", " try_core = 1;", " strcpy(MyFile, TrailFile); /* restore */", " tprefix = \"trail\";", "try_again:", " if (whichtrail)", " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);", " fd = fopen(fnm, \"r\");", " if (fd == NULL && (q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* e.g., strip .pml on original file */ " sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, whichtrail, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " }", " } else", " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " fd = fopen(fnm, \"r\");", " if (fd == NULL && (q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* e.g., strip .pml on original file */ " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " } }", " if (fd == NULL)", " { if (try_core < NCORE)", " { tprefix = MySuffix;", " sprintf(tprefix, \"cpu%%d_trail\", try_core++);", " goto try_again;", " }", " printf(\"pan: cannot find trailfile %%s\\n\", fnm);", " pan_exit(1);", " }", "success:", "#if NCORE>1 && defined(SEP_STATE)", " { void set_root(void); /* for partial traces from local root */", " set_root();", " }", "#endif", " return fd;", "}", "", "uchar do_transit(Trans *, short);", "", "void", "getrail(void)", "{ FILE *fd;", " char *q;", " int i, t_id, lastnever=-1; short II;", " Trans *t;", " P0 *z;", "", " fd = findtrail(); /* exits if unsuccessful */", " while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)", " { if (depth == -1)", " printf(\"<<<<>>>>\\n\");", " if (depth < 0)", " continue;", " if (i > now._nr_pr)", " { printf(\"pan: Error, proc %%d invalid pid \", i);", " printf(\"transition %%d\\n\", t_id);", " break;", " }", " II = i;", " z = (P0 *)pptr(II);", " for (t = trans[z->_t][z->_p]; t; t = t->nxt)", " if (t->t_id == (T_ID) t_id)", " break;", " if (!t)", " { for (i = 0; i < NrStates[z->_t]; i++)", " { t = trans[z->_t][i];", " if (t && t->t_id == (T_ID) t_id)", " { printf(\"\\tRecovered at state %%d\\n\", i);", " z->_p = i;", " goto recovered;", " } }", " printf(\"pan: Error, proc %%d type %%d state %%d: \",", " II, z->_t, z->_p);", " printf(\"transition %%d not found\\n\", t_id);", " printf(\"pan: list of possible transitions in this process:\\n\");", " if (z->_t >= 0 && z->_t <= _NP_)", " for (t = trans[z->_t][z->_p]; t; t = t->nxt)", " printf(\" t_id %%d -- case %%d, [%%s]\\n\",", " t->t_id, t->forw, t->tp);", " break; /* pan_exit(1); */", " }", "recovered:", " q = transmognify(t->tp);", " if (gui) simvals[0] = \'\\0\';", " this = pptr(II);", " trpt->tau |= 1;", /* timeout always possible */ " if (!do_transit(t, II))", " { if (onlyproc >= 0 && II != onlyproc)", " goto moveon;", " printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");", " printf(\" most likely causes: missing c_track statements\\n\");", " printf(\" or illegal side-effects in c_expr statements\\n\");", " }", " if (onlyproc >= 0 && II != onlyproc)", " goto moveon;", " if (verbose)", " { printf(\"%%3ld: proc %%2d (%%s) \", depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\" %%s:%%d \",", " find_source((int) z->_t, (int) z->_p),", " src_all[i].src[z->_p]);", " break;", " }", " printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",", " z->_p, t_id, t->forw, q?q:\"\");", " c_globals();", " for (i = 0; i < now._nr_pr; i++)", " { c_locals(i, ((P0 *)pptr(i))->_t);", " }", " } else if (Btypes[z->_t] == N_CLAIM)", " { if (lastnever != (int) z->_p)", " { for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\"MSC: ~G %%d\\n\",", " src_all[i].src[z->_p]);", " break;", " }", " if (!src_all[i].src)", " printf(\"MSC: ~R %%d\\n\", z->_p);", " }", " lastnever = z->_p;", " goto sameas;", " } else if (Btypes[z->_t] != 0) /* not :np_: */", " {", "sameas: if (no_rck) goto moveon;", " if (coltrace)", " { printf(\"%%ld: \", depth);", " for (i = 0; i < II; i++)", " printf(\"\\t\\t\");", " printf(\"%%s(%%d):\", procname[z->_t], II);", " printf(\"[%%s]\\n\", q?q:\"\");", " } else if (!silent)", " { if (strlen(simvals) > 0) {", " printf(\"%%3ld: proc %%2d (%%s)\", ", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\" %%s:%%d \",", " find_source((int) z->_t, (int) z->_p),", " src_all[i].src[z->_p]);", " break;", " }", " printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);", " }", " printf(\"%%3ld: proc %%2d (%%s)\", ", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", " { printf(\" %%s:%%d \",", " find_source((int) z->_t, (int) z->_p),", " src_all[i].src[z->_p]);", " break;", " }", " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");", " /* printf(\"\\n\"); */", " } }", "moveon: z->_p = t->st;", " }", " wrap_trail();", "}", "#endif", "int", "f_pid(int pt)", "{ int i;", " P0 *z;", " for (i = 0; i < now._nr_pr; i++)", " { z = (P0 *)pptr(i);", " if (z->_t == (unsigned) pt)", " return BASE+z->_pid;", " }", " return -1;", "}", "", "#if !defined(HASH64) && !defined(HASH32)", " #if WS>4", " #define HASH64", " #else", " #define HASH32", " #endif", "#endif", "#if defined(HASH32) && defined(SAFETY) && !defined(SFH) && !defined(SPACE)", " #define SFH", "#endif", "#if defined(SFH) && (defined(BITSTATE) || defined(COLLAPSE) || defined(HC) || defined(HASH64) || defined(MA))", " #undef SFH", /* need 2 hash fcts, for which Jenkins is best */ "#endif", /* or a 64 bit hash, which we dont have for SFH */ /* for MA, it would slow down the search to use a larger sv then possible */ "#if defined(SFH) && !defined(NOCOMP)", " #define NOCOMP /* go for speed */", "#endif", "#if NCORE>1 && !defined(GLOB_HEAP)", " #define SEP_HEAP /* version 5.1.2 */", "#endif", "", "#ifdef BITSTATE", "int", "bstore_mod(char *v, int n) /* hasharray size not a power of two */", "{ unsigned long x, y;", " unsigned int i = 1;", "", " d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */", " x = K1; y = j3;", /* was K2 before 5.1.1 */ " for (;;)", " { if (!(SS[x%%udmem]&(1< RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x%%udmem] |= (1< RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x] |= (1< 0)", " { sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, Nr_Trails-1, tprefix);", " } else", " {", "#ifdef PUTPID", " sprintf(fnm, \"%%s_%%s_%%d.%%s\", MyFile, progname, getpid(), tprefix);", "#else", " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", "#endif", " }", " if ((fd = open(fnm, w_flags, TMODE)) < 0)", " { if ((q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* strip .pml */ " if (iterative == 0 && Nr_Trails-1 > 0)", " sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, Nr_Trails-1, tprefix);", " else", " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " *q = \'.\';", " fd = open(fnm, w_flags, TMODE);", " } }", " if (fd < 0)", " { printf(\"pan: cannot create %%s\\n\", fnm);", " perror(\"cause\");", " } else", " {", "#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))", " void write_root(void); ", " write_root();", "#else", " printf(\"pan: wrote %%s\\n\", fnm);", "#endif", " }", " return fd;", "}", "", "#ifndef FREQ", "#define FREQ (1000000)", "#endif", "double freq = (double) FREQ;\n", "#ifdef TRIX", "void sv_populate(void);", "", "void", "re_populate(void) /* restore procs and chans from now._ids_ */", "{ int i, cnt = 0;", " char *b;", "#ifdef V_TRIX", " printf(\"%%4d: re_populate\\n\", depth);", "#endif", " for (i = 0; i < now._nr_pr; i++, cnt++)", " { b = now._ids_[cnt];", " processes[i]->psize = what_p_size( ((P0 *)b)->_t );", " memcpy(processes[i]->body, b, processes[i]->psize);", "#ifdef TRIX_RIX", " ((P0 *)pptr(i))->_pid = i;", "#endif", "#ifndef BFS", " processes[i]->modified = 1; /* re-populate */", "#endif", " }", " for (i = 0; i < now._nr_qs; i++, cnt++)", " { b = now._ids_[cnt];", " channels[i]->psize = what_q_size( ((Q0 *)b)->_t );", " memcpy(channels[i]->body, b, channels[i]->psize);", "#ifndef BFS", " channels[i]->modified = 1; /* re-populate */", "#endif", " }", "}", "#endif\n", "#ifdef BFS", /* breadth-first search */ "#define Q_PROVISO", " #ifndef INLINE_REV", " #define INLINE_REV", " #endif", "", "typedef struct SV_Hold {", " State *sv;", " int sz;", " struct SV_Hold *nxt;", "} SV_Hold;", "", "typedef struct EV_Hold {", " char *sv;", /* Mask */ " int sz;", /* vsize */ " int nrpr;", " int nrqs;", "#ifndef TRIX", " char *po, *qo;", " char *ps, *qs;", "#endif", " struct EV_Hold *nxt;", "} EV_Hold;", "", "typedef struct BFS_Trail {", " Trail *frame;", " SV_Hold *onow;", " EV_Hold *omask;", "#ifdef Q_PROVISO", " struct H_el *lstate;", "#endif", " short boq;", "#ifdef VERBOSE", " unsigned long nr;", "#endif", " struct BFS_Trail *nxt;", "} BFS_Trail;", "", "BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;", "", "SV_Hold *svhold, *svfree;", "", "#ifdef BFS_DISK", " #ifndef BFS_LIMIT", " #define BFS_LIMIT 100000", " #endif", " #ifndef BFS_DSK_LIMIT", " #define BFS_DSK_LIMIT 1000000", " #endif", " #if defined(WIN32) || defined(WIN64)", " #define RFLAGS (O_RDONLY|O_BINARY)", " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)", " #else", " #define RFLAGS (O_RDONLY)", " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)", " #endif", "long bfs_size_limit;", "int bfs_dsk_write = -1;", "int bfs_dsk_read = -1;", "long bfs_dsk_writes, bfs_dsk_reads;", "int bfs_dsk_seqno_w, bfs_dsk_seqno_r;", "#endif", "", "uchar do_reverse(Trans *, short, uchar);", "void snapshot(void);", "", "void", "select_claim(int x) /* ignored in BFS mode */", "{ if (verbose)", " { printf(\"select %%d (ignored)\\n\", x);", " }", "}", "", "SV_Hold *", "getsv(int n)", "{ SV_Hold *h = (SV_Hold *) 0, *oh;", "", " oh = (SV_Hold *) 0;", " for (h = svfree; h; oh = h, h = h->nxt)", " { if (n == h->sz)", " { if (!oh)", " svfree = h->nxt;", " else", " oh->nxt = h->nxt;", " h->nxt = (SV_Hold *) 0;", " break;", " }", " if (n < h->sz)", " { h = (SV_Hold *) 0;", " break;", " }", " /* else continue */", " }", "", " if (!h)", " { h = (SV_Hold *) emalloc(sizeof(SV_Hold));", " h->sz = n;", "#ifdef BFS_DISK", " if (bfs_size_limit >= BFS_LIMIT)", " { h->sv = (State *) 0; /* means: read disk */", " bfs_dsk_writes++; /* count */", " if (bfs_dsk_write < 0 /* file descriptor */", " || bfs_dsk_writes%%BFS_DSK_LIMIT == 0)", " { char dsk_nm[32];", " if (bfs_dsk_write >= 0)", " { (void) close(bfs_dsk_write);", " }", " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_w++);", " bfs_dsk_write = open(dsk_nm, WFLAGS, 0644);", " if (bfs_dsk_write < 0)", " { Uerror(\"could not create tmp disk file\");", " }", " printf(\"pan: created disk file %%s\\n\", dsk_nm);", " }", " if (write(bfs_dsk_write, (char *) &now, n) != n)", " { Uerror(\"aborting -- disk write failed (disk full?)\");", " }", " return h; /* no memcpy */", " }", /* else */ " bfs_size_limit++;", "#endif", " h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);", " }", "", " memcpy((char *)h->sv, (char *)&now, n);", " return h;", "}", "", "EV_Hold *", "getsv_mask(int n)", "{ EV_Hold *h;", " static EV_Hold *kept = (EV_Hold *) 0;", "", " for (h = kept; h; h = h->nxt)", " if (n == h->sz", " && (memcmp((char *) Mask, (char *) h->sv, n) == 0)", " && (now._nr_pr == h->nrpr)", " && (now._nr_qs == h->nrqs)", "#ifdef TRIX", " )", "#else", " #if VECTORSZ>32000", " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)", " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)", " #else", " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)", " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)", " #endif", " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)", " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))", "#endif", " break;", " if (!h)", " { h = (EV_Hold *) emalloc(sizeof(EV_Hold));", " h->sz = n;", " h->nrpr = now._nr_pr;", " h->nrqs = now._nr_qs;", "", " h->sv = (char *) emalloc(n * sizeof(char));", " memcpy((char *) h->sv, (char *) Mask, n);", "#ifndef TRIX", " if (now._nr_pr > 0)", " { h->ps = (char *) emalloc(now._nr_pr * sizeof(int));", " memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(uchar));", " #if VECTORSZ>32000", " h->po = (char *) emalloc(now._nr_pr * sizeof(int));", " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));", " #else", " h->po = (char *) emalloc(now._nr_pr * sizeof(short));", " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));", " #endif", " }", " if (now._nr_qs > 0)", " { h->qs = (char *) emalloc(now._nr_qs * sizeof(int));", " memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(uchar));", " #if VECTORSZ>32000", " h->qo = (char *) emalloc(now._nr_qs * sizeof(int));", " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));", " #else", " h->qo = (char *) emalloc(now._nr_qs * sizeof(short));", " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));", " #endif", " }", "#endif", " h->nxt = kept;", " kept = h;", " }", " return h;", "}", "", "void", "freesv(SV_Hold *p)", "{ SV_Hold *h, *oh;", "", " oh = (SV_Hold *) 0;", " for (h = svfree; h; oh = h, h = h->nxt)", " { if (h->sz >= p->sz)", " break;", " }", " if (!oh)", " { p->nxt = svfree;", " svfree = p;", " } else", " { p->nxt = h;", " oh->nxt = p;", " }", "}", "", "BFS_Trail *", "get_bfs_frame(void)", "{ BFS_Trail *t;", "", " if (bfs_free)", " { t = bfs_free;", " bfs_free = bfs_free->nxt;", " t->nxt = (BFS_Trail *) 0;", " } else", " { t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));", " }", " t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */ " /* new because we keep a ptr to the frame of parent states */", " /* used for reconstructing path and recovering failed rvs etc */", " return t;", "}", "", "void", "push_bfs(Trail *f, int d)", "{ BFS_Trail *t;", "", " t = get_bfs_frame();", " memcpy((char *)t->frame, (char *)f, sizeof(Trail));", " t->frame->o_tt = d; /* depth */", "", " t->boq = boq;", "#ifdef TRIX", " sv_populate();", "#endif", " t->onow = getsv(vsize);", " t->omask = getsv_mask(vsize);", "#if defined(FULLSTACK) && defined(Q_PROVISO)", " t->lstate = Lstate;", "#endif", " if (!bfs_bot)", " { bfs_bot = bfs_trail = t;", " } else", " { bfs_bot->nxt = t;", " bfs_bot = t;", " }", "#ifdef VERBOSE", " t->nr = nstates;", "#endif", "#ifdef CHECK", " printf(\"PUSH %%u (depth %%d, nr %%d)\\n\", t->frame, d, t->nr);", "#endif", "}", "", "Trail *", "pop_bfs(void)", "{ BFS_Trail *t;", "", " if (!bfs_trail)", " { return (Trail *) 0;", " }", " t = bfs_trail;", " bfs_trail = t->nxt;", " if (!bfs_trail)", " { bfs_bot = (BFS_Trail *) 0;", " }", "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)", " if (t->lstate)", " { t->lstate->tagged = 0;", " }", "#endif", " t->nxt = bfs_free;", " bfs_free = t;", "", " vsize = t->onow->sz;", " boq = t->boq;", "#ifdef BFS_DISK", " if (t->onow->sv == (State *) 0)", " { char dsk_nm[32];", " bfs_dsk_reads++; /* count */", " if (bfs_dsk_read >= 0 /* file descriptor */", " && bfs_dsk_reads%%BFS_DSK_LIMIT == 0)", " { (void) close(bfs_dsk_read);", " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r-1);", " (void) unlink(dsk_nm);", " bfs_dsk_read = -1;", " }", " if (bfs_dsk_read < 0)", " { sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r++);", " bfs_dsk_read = open(dsk_nm, RFLAGS);", " if (bfs_dsk_read < 0)", " { Uerror(\"could not open temp disk file\");", " } }", " if (read(bfs_dsk_read, (char *) &now, vsize) != vsize)", " { Uerror(\"bad bfs disk file read\");", " }", " #ifndef NOVSZ", " if (now._vsz != vsize)", " { Uerror(\"disk read vsz mismatch\");", " }", " #endif", " } else", "#endif", " { memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);", " }", " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);", "#ifdef TRIX", " re_populate();", "#else", " if (now._nr_pr > 0)", " #if VECTORSZ>32000", " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));", " #else", " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));", " #endif", " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));", " }", " if (now._nr_qs > 0)", " #if VECTORSZ>32000", " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));", " #else", " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));", " #endif", " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));", " }", "#endif", "#ifdef BFS_DISK", " if (t->onow->sv != (State *) 0)", "#endif", " { freesv(t->onow); /* omask not freed */", " }", "#ifdef CHECK", " printf(\"POP %%u (depth %%d, nr %%d)\\n\", t->frame, t->frame->o_tt, t->nr);", "#endif", " return t->frame;", "}", "", "void", "store_state(Trail *ntrpt, int shortcut, short oboq)", "{", "#ifdef VERI", " Trans *t2 = (Trans *) 0;", " uchar ot; int tt, E_state;", " uchar o_opm = trpt->o_pm, *othis = this;", "", " if (shortcut)", " {", " #ifdef VERBOSE", " printf(\"claim: shortcut\\n\");", " #endif", " goto store_it; /* no claim move */", " }", "", " this = pptr(0); /* 0 = never claim */", " trpt->o_pm = 0;", /* to interpret else in never claim */ "", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", "", " #ifdef HAS_UNLESS", " E_state = 0;", " #endif", " for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)", " {", " #ifdef HAS_UNLESS", " if (E_state > 0 && E_state != t2->e_trans)", " { break;", " }", " #endif", " if (do_transit(t2, 0))", " {", " #ifdef VERBOSE", " if (!reached[ot][t2->st])", " printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",", " trpt->o_tt, ((P0 *)this)->_p, t2->st);", " #endif", " #ifdef HAS_UNLESS", " E_state = t2->e_trans;", " #endif", " if (t2->st > 0)", " { ((P0 *)this)->_p = t2->st;", " reached[ot][t2->st] = 1;", " #ifndef NOCLAIM", " if (stopstate[ot][t2->st])", " { uerror(\"end state in claim reached\");", " }", " #endif", " }", " if (now._nr_pr == 0) /* claim terminated */", " uerror(\"end state in claim reached\");", "", " #ifdef PEG", " peg[t2->forw]++;", " #endif", " trpt->o_pm |= 1;", " if (t2->atom&2)", " { Uerror(\"atomic in claim not supported in BFS\");", " }", "store_it:", "", "#endif", /* VERI */ "", "#if defined(BITSTATE)", " if (!bstore((char *)&now, vsize))", "#elif defined(MA)", " if (!gstore((char *)&now, vsize, 0))", "#else", " if (!hstore((char *)&now, vsize))", "#endif", " { static long sdone = (long) 0; long ndone;", " nstates++;", "#ifndef NOREDUCE", " trpt->tau |= 64;", /* bfs: succ definitely outside stack */ "#endif", " ndone = (unsigned long) (nstates/(freq));", " if (ndone != sdone && mreached%%10 != 0)", " { snapshot();", " sdone = ndone;", "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)", " if (nstates > ((double)(1<<(ssize+1))))", " { void resize_hashtable(void);", " resize_hashtable();", " }", "#endif", " }", "#if SYNC", " if (boq != -1)", " midrv++;", " else if (oboq != -1)", " { Trail *x;", " x = (Trail *) trpt->ostate; /* pre-rv state */", " if (x) x->o_pm |= 4; /* mark success */", " }", "#endif", " push_bfs(ntrpt, trpt->o_tt+1);", " } else", " { truncs++;", "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)", " #if !defined(BITSTATE)", " if (Lstate && Lstate->tagged)", " { trpt->tau |= 64;", " }", " #else", " if (trpt->tau&32)", " { BFS_Trail *tprov;", " for (tprov = bfs_trail; tprov; tprov = tprov->nxt)", " if (tprov->onow->sv != (State *) 0", " && memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize) == 0)", " { trpt->tau |= 64;", " break; /* state is in queue */", " } }", " #endif", "#endif", " }", "#ifdef VERI", " ((P0 *)this)->_p = tt; /* reset claim */", " if (t2)", " do_reverse(t2, 0, 0);", " else", " break;", " } }", " this = othis;", " trpt->o_pm = o_opm;", "#endif", "}", "", "Trail *ntrpt;", /* 4.2.8 */ "", "void", "bfs(void)", "{ Trans *t; Trail *otrpt, *x;", " uchar _n, _m, ot, nps = 0;", " int tt, E_state;", " short II, From = (short) (now._nr_pr-1), To = BASE;", " short oboq = boq;", "", " ntrpt = (Trail *) emalloc(sizeof(Trail));", " trpt->ostate = (struct H_el *) 0;", " trpt->tau = 0;", "", " trpt->o_tt = -1;", " store_state(ntrpt, 0, oboq); /* initial state */", "", " while ((otrpt = pop_bfs())) /* also restores now */", " { memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));", "#if defined(C_States) && (HAS_TRACK==1)", " c_revert((uchar *) &(now.c_state[0]));", "#endif", " if (trpt->o_pm & 4)", " {", "#ifdef VERBOSE", " printf(\"Revisit of atomic not needed (%%d)\\n\",", " trpt->o_pm);", /* at least 1 rv succeeded */ "#endif", " continue;", " }", "#ifndef NOREDUCE", " nps = 0;", "#endif", " if (trpt->o_pm == 8)", " { revrv++;", " if (trpt->tau&8)", " {", "#ifdef VERBOSE", " printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",", " trpt->o_pm, trpt->tau);", "#endif", " trpt->tau &= ~8;", " }", "#ifndef NOREDUCE", " else if (trpt->tau&32)", /* was a preselected move */ " {", " #ifdef VERBOSE", " printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",", " trpt->o_pm, trpt->tau);", " #endif", " trpt->tau &= ~32;", " nps = 1; /* no preselection in repeat */", " }", "#endif", " }", " trpt->o_pm &= ~(4|8);", " if (trpt->o_tt > mreached)", " { mreached = trpt->o_tt;", " if (mreached%%10 == 0)", " { snapshot();", " } }", " depth = trpt->o_tt;", " if (depth >= maxdepth)", " {", "#if SYNC", " Trail *x;", " if (boq != -1)", " { x = (Trail *) trpt->ostate;", " if (x) x->o_pm |= 4; /* not failing */", " }", "#endif", " truncs++;", " if (!warned)", " { warned = 1;", " printf(\"error: max search depth too small\\n\");", " }", " if (bounded)", " { uerror(\"depth limit reached\");", " }", " continue;", " }", "#ifndef NOREDUCE", " if (boq == -1 && !(trpt->tau&8) && nps == 0)", " for (II = now._nr_pr-1; II >= BASE; II -= 1)", " {", "Pickup: this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " if (trans[ot][tt]->atom & 8)", /* safe */ " { t = trans[ot][tt];", " if (t->qu[0] != 0)", " { Ccheck++;", " if (!q_cond(II, t))", " continue;", " Cholds++;", " }", " From = To = II;", " trpt->tau |= 32; /* preselect marker */", " #ifdef DEBUG", " printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ", " depth, II, trpt->tau);", " #endif", " goto MainLoop;", " } }", " trpt->tau &= ~32;", /* not preselected */ "#endif", /* if !NOREDUCE */ "Repeat:", " if (trpt->tau&8) /* atomic */", " { From = To = (short ) trpt->pr;", " nlinks++;", " } else", " { From = now._nr_pr-1;", " To = BASE;", " }", "MainLoop:", " _n = _m = 0;", " for (II = From; II >= To; II -= 1)", " {", " this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", "#if SYNC", " /* no rendezvous with same proc */", " if (boq != -1 && trpt->pr == II)", " { continue;", " }", "#endif", " ntrpt->pr = (uchar) II;", " ntrpt->st = tt; ", " trpt->o_pm &= ~1; /* no move yet */", "#ifdef EVENT_TRACE", " trpt->o_event = now._event;", "#endif", "#ifdef HAS_PROVIDED", " if (!provided(II, ot, tt, t))", " { continue;", " }", "#endif", "#ifdef HAS_UNLESS", " E_state = 0;", "#endif", " for (t = trans[ot][tt]; t; t = t->nxt)", " {", "#ifdef HAS_UNLESS", " if (E_state > 0", " && E_state != t->e_trans)", " break;", "#endif", " ntrpt->o_t = t;", "", " oboq = boq;", "", " if (!(_m = do_transit(t, II)))", " continue;", "", " trpt->o_pm |= 1; /* we moved */", " (trpt+1)->o_m = _m; /* for unsend */", "#ifdef PEG", " peg[t->forw]++;", "#endif", "#ifdef CHECK", " printf(\"%%3ld: proc %%d exec %%d, \",", " depth, II, t->forw);", " printf(\"%%d to %%d, %%s %%s %%s\",", " tt, t->st, t->tp,", " (t->atom&2)?\"atomic\":\"\",", " (boq != -1)?\"rendez-vous\":\"\");", " #ifdef HAS_UNLESS", " if (t->e_trans)", " printf(\" (escapes to state %%d)\", t->st);", " #endif", " printf(\" %%saccepting [tau=%%d]\\n\",", " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);", "#endif", "#ifdef HAS_UNLESS", " E_state = t->e_trans;", " #if SYNC>0", " if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))", " { fprintf(efd, \"error:\ta rendezvous stmnt in the escape clause\\n\");", " fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");", " pan_exit(1);", " }", " #endif", "#endif", " if (t->st > 0)", " { ((P0 *)this)->_p = t->st;", " }", "", " /* ptr to pred: */ ntrpt->ostate = (struct H_el *) otrpt;", " ntrpt->st = tt;", " if (boq == -1 && (t->atom&2)) /* atomic */", " ntrpt->tau = 8; /* record for next move */", " else", " ntrpt->tau = 0;", " store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);", "#ifdef EVENT_TRACE", " now._event = trpt->o_event;", "#endif", " /* undo move and continue */", " trpt++; /* this is where ovals and ipt are set */", " do_reverse(t, II, _m); /* restore now. */", " trpt--;", "#ifdef CHECK", " #if NCORE>1", " enter_critical(GLOBAL_LOCK); /* verbose mode */", " printf(\"cpu%%d: \", core_id);", " #endif", " printf(\"%%3d: proc %%d \", depth, II);", " printf(\"reverses %%d, %%d to %%d,\",", " t->forw, tt, t->st);", " printf(\" %%s [abit=%%d,adepth=%%d,\",", " t->tp, now._a_t, A_depth);", " printf(\"tau=%%d,%%d]\\n\",", " trpt->tau, (trpt-1)->tau);", " #if NCORE>1", " leave_critical(GLOBAL_LOCK);", " #endif", "#endif", " reached[ot][t->st] = 1;", " reached[ot][tt] = 1;", "", " ((P0 *)this)->_p = tt;", " _n |= _m;", " } }", "#ifndef NOREDUCE", /* with PO */ " /* preselected - no succ definitely outside stack */", " if ((trpt->tau&32) && !(trpt->tau&64))", " { From = now._nr_pr-1; To = BASE;", " #ifdef DEBUG", " cpu_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ", " depth, II+1, (int) _n, trpt->tau);", " #endif", " _n = 0; trpt->tau &= ~32;", " if (II >= BASE)", " { goto Pickup;", " }", " goto MainLoop;", " }", " trpt->tau &= ~(32|64);", "#endif", /* PO */ " if (_n != 0)", " { continue;", " }", "#ifdef DEBUG", " printf(\"%%3ld: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",", " depth, II, trpt->tau, boq, now._nr_pr);", "#endif", " if (boq != -1)", " { failedrv++;", " x = (Trail *) trpt->ostate; /* pre-rv state */", " if (!x)", " { continue; /* root state */", " }", " if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */", " { x->o_pm |= 8; /* mark failure */", " this = pptr(otrpt->pr);", "#ifdef VERBOSE", " printf(\"\\treset state of %%d from %%d to %%d\\n\",", " otrpt->pr, ((P0 *)this)->_p, otrpt->st);", "#endif", " ((P0 *)this)->_p = otrpt->st;", " unsend(boq); /* retract rv offer */", " boq = -1;", " push_bfs(x, x->o_tt);", "#ifdef VERBOSE", " printf(\"failed rv, repush with %%d\\n\", x->o_pm);", "#endif", " }", "#ifdef VERBOSE", " else", " { printf(\"failed rv, tau at parent: %%d\\n\", x->tau);", " }", "#endif", " } else if (now._nr_pr > 0)", " {", " if ((trpt->tau&8)) /* atomic */", " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */", "#ifdef DEBUG", " printf(\"%%3ld: atomic step proc %%d blocks\\n\",", " depth, II+1);", "#endif", " goto Repeat;", " }", "", " if (!(trpt->tau&1)) /* didn't try timeout yet */", " { trpt->tau |= 1;", "#ifdef DEBUG", " printf(\"%%d: timeout\\n\", depth);", "#endif", " goto MainLoop;", " }", "#ifndef VERI", " if (!noends && !a_cycles && !endstate())", " { uerror(\"invalid end state\");", " }", "#endif", " } }", "}", "", "void", "putter(Trail *trpt, int fd)", "{ long j;", "", " if (!trpt) return;", "", " if (trpt != (Trail *) trpt->ostate)", " putter((Trail *) trpt->ostate, fd);", "", " if (trpt->o_t)", " { sprintf(snap, \"%%d:%%d:%%d\\n\",", " trcnt++, trpt->pr, trpt->o_t->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", " { printf(\"pan: error writing %%s\\n\", fnm);", " pan_exit(1);", " } }", "}", "", "void", "nuerror(char *str)", "{ int fd = make_trail();", " int j;", "", " if (fd < 0) return;", "#ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);", " (void) write(fd, snap, strlen(snap));", "#endif", "#ifdef MERGED", " sprintf(snap, \"-4:-4:-4\\n\");", " (void) write(fd, snap, strlen(snap));", "#endif", " trcnt = 1;", " putter(trpt, fd);", " if (ntrpt->o_t)", /* 4.2.8 -- Alex example, missing last transition */ " { sprintf(snap, \"%%d:%%d:%%d\\n\",", " trcnt++, ntrpt->pr, ntrpt->o_t->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", " { printf(\"pan: error writing %%s\\n\", fnm);", " pan_exit(1);", " } }", " close(fd);", " if (errors >= upto && upto != 0)", " { wrapup();", " }", "}", "#endif", /* BFS */ 0, }; static char *Code2d[] = { "clock_t start_time;", "#if NCORE>1", "clock_t crash_stamp;", "#endif", "#if !defined(WIN32) && !defined(WIN64)", "struct tms start_tm;", "#endif", "", "void", "start_timer(void)", "{", "#if defined(WIN32) || defined(WIN64)", " start_time = clock();", "#else", " start_time = times(&start_tm);", "#endif", "}", "", "void", "stop_timer(void)", "{ clock_t stop_time;", " double delta_time;", "#if !defined(WIN32) && !defined(WIN64)", " struct tms stop_tm;", " stop_time = times(&stop_tm);", " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));", "#else", " stop_time = clock();", " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);", "#endif", " if (readtrail || delta_time < 0.00) return;", "#if NCORE>1", " if (core_id == 0 && nstates > (double) 0)", " { printf(\"\\ncpu%%d: elapsed time %%.3g seconds (%%g states visited)\\n\",", " core_id, delta_time, nstates);", " if (delta_time > 0.01)", " { printf(\"cpu%%d: rate %%g states/second\\n\", core_id, nstates/delta_time);", " }", " { void check_overkill(void);", " check_overkill();", " } }", "#else", " printf(\"\\npan: elapsed time %%.3g seconds\\n\", delta_time);", " if (delta_time > 0.01)", " { printf(\"pan: rate %%9.8g states/second\\n\", nstates/delta_time);", " if (verbose)", " { printf(\"pan: avg transition delay %%.5g usec\\n\",", " delta_time/(nstates+truncs));", " } }", "#endif", "}", "", "#if NCORE>1", "#ifdef T_ALERT", "double t_alerts[17];", "", "void", "crash_report(void)", "{ int i;", " printf(\"crash alert intervals:\\n\");", " for (i = 0; i < 17; i++)", " { printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);", "} }", "#endif", "", "void", "crash_reset(void)", "{ /* false alarm */", " if (crash_stamp != (clock_t) 0)", " {", "#ifdef T_ALERT", " double delta_time;", " int i;", "#if defined(WIN32) || defined(WIN64)", " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);", "#else", " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));", "#endif", " for (i = 0; i < 16; i++)", " { if (delta_time <= (i*30))", " { t_alerts[i] = delta_time;", " break;", " } }", " if (i == 16) t_alerts[i] = delta_time;", "#endif", " if (verbose)", " printf(\"cpu%%d: crash alert off\\n\", core_id);", " }", " crash_stamp = (clock_t) 0;", "}", "", "int", "crash_test(double maxtime)", "{ double delta_time;", " if (crash_stamp == (clock_t) 0)", " { /* start timing */", "#if defined(WIN32) || defined(WIN64)", " crash_stamp = clock();", "#else", " crash_stamp = times(&start_tm);", "#endif", " if (verbose)", " { printf(\"cpu%%d: crash detection\\n\", core_id);", " }", " return 0;", " }", "#if defined(WIN32) || defined(WIN64)", " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);", "#else", " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));", "#endif", " return (delta_time >= maxtime);", "}", "#endif", "", "void", "do_the_search(void)", "{ int i;", " depth = mreached = 0;", " trpt = &trail[0];", "#ifdef VERI", " trpt->tau |= 4; /* the claim moves first */", "#endif", " for (i = 0; i < (int) now._nr_pr; i++)", " { P0 *ptr = (P0 *) pptr(i);", "#ifndef NP", " if (!(trpt->o_pm&2)", " && accpstate[ptr->_t][ptr->_p])", " { trpt->o_pm |= 2;", " }", "#else", " if (!(trpt->o_pm&4)", " && progstate[ptr->_t][ptr->_p])", " { trpt->o_pm |= 4;", " }", "#endif", " }", "#ifdef EVENT_TRACE", "#ifndef NP", " if (accpstate[EVENT_TRACE][now._event])", " { trpt->o_pm |= 2;", " }", "#else", " if (progstate[EVENT_TRACE][now._event])", " { trpt->o_pm |= 4;", " }", "#endif", "#endif", "#ifndef NOCOMP", " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */", " if (!a_cycles)", " { i = &(now._a_t) - (uchar *) &now;", " Mask[i] = 1; /* _a_t */", " }", "#ifndef NOFAIR", " if (!fairness)", " { int j = 0;", " i = &(now._cnt[0]) - (uchar *) &now;", " while (j++ < NFAIR)", " Mask[i++] = 1; /* _cnt[] */", " }", "#endif", "#endif", "#ifndef NOFAIR", " if (fairness", " && (a_cycles && (trpt->o_pm&2)))", " { now._a_t = 2; /* set the A-bit */", " now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */ "#ifdef VERBOSE", " printf(\"%%3ld: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",", " depth, now._cnt[now._a_t&1], now._a_t);", "#endif", " }", "#endif", " c_stack_start = (char *) &i; /* meant to be read-only */", "#if defined(HAS_CODE) && defined (C_INIT)", " C_INIT; /* initialization of data that must precede fork() */", " c_init_done++;", "#endif", "#if defined(C_States) && (HAS_TRACK==1)", " /* capture initial state of tracked C objects */", " c_update((uchar *) &(now.c_state[0]));", "#endif", "#ifdef HAS_CODE", " if (readtrail) getrail(); /* no return */", "#endif", " start_timer();", "#ifdef BFS", " bfs();", "#else", "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)", " /* initial state of tracked & unmatched objects */", " c_stack((uchar *) &(svtack->c_stack[0]));", "#endif", "#if defined(P_RAND) || defined(T_RAND)", " srand(s_rand);", "#endif", "#if NCORE>1", " mem_get();", "#else", " new_state(); /* start 1st DFS */", "#endif", "#endif", "}", "#ifdef INLINE_REV", "uchar", "do_reverse(Trans *t, short II, uchar M)", "{ uchar _m = M;", " int tt = (int) ((P0 *)this)->_p;", "#include REVERSE_MOVES", "R999: return _m;", "}", "#endif", "#ifndef INLINE", "#ifdef EVENT_TRACE", "static char _tp = 'n'; static int _qid = 0;", "#endif", "uchar", "do_transit(Trans *t, short II)", "{ uchar _m = 0;", " int tt = (int) ((P0 *)this)->_p;", "#ifdef M_LOSS", " uchar delta_m = 0;", "#endif", "#ifdef EVENT_TRACE", " short oboq = boq;", " uchar ot = (uchar) ((P0 *)this)->_t;", " if (II == -EVENT_TRACE) boq = -1;", "#define continue { boq = oboq; return 0; }", "#else", "#define continue return 0", "#ifdef SEPARATE", " uchar ot = (uchar) ((P0 *)this)->_t;", "#endif", "#endif", "#include FORWARD_MOVES", "P999:", "#ifdef EVENT_TRACE", " if (II == -EVENT_TRACE) boq = oboq;", "#endif", " return _m;", "#undef continue", "}", "#ifdef EVENT_TRACE", "void", "require(char tp, int qid)", "{ Trans *t;", " _tp = tp; _qid = qid;", "", " if (now._event != endevent)", " for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)", " { if (do_transit(t, -EVENT_TRACE))", " { now._event = t->st;", " reached[EVENT_TRACE][t->st] = 1;", "#ifdef VERBOSE", " printf(\" event_trace move to -> %%d\\n\", t->st);", "#endif", "#ifndef BFS", "#ifndef NP", " if (accpstate[EVENT_TRACE][now._event])", " (trpt+1)->o_pm |= 2;", "#else", " if (progstate[EVENT_TRACE][now._event])", " (trpt+1)->o_pm |= 4;", "#endif", "#endif", "#ifdef NEGATED_TRACE", " if (now._event == endevent)", " {", "#ifndef BFS", " depth++; trpt++;", "#endif", " uerror(\"event_trace error (all events matched)\");", "#ifndef BFS", " trpt--; depth--;", "#endif", " break;", " }", "#endif", " for (t = t->nxt; t; t = t->nxt)", " { if (do_transit(t, -EVENT_TRACE))", " Uerror(\"non-determinism in event-trace\");", " }", " return;", " }", "#ifdef VERBOSE", " else", " printf(\" event_trace miss '%%c' -- %%d, %%d, %%d\\n\",", " tp, qid, now._event, t->forw);", "#endif", " }", "#ifdef NEGATED_TRACE", " now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */", "#else", "#ifndef BFS", " depth++; trpt++;", "#endif", " uerror(\"event_trace error (no matching event)\");", "#ifndef BFS", " trpt--; depth--;", "#endif", "#endif", "}", "#endif", "int", "enabled(int iam, int pid)", "{ Trans *t; uchar *othis = this;", " int res = 0; int tt; uchar ot;", "#ifdef VERI", " /* if (pid > 0) */ pid++;", "#endif", " if (pid == iam)", " Uerror(\"used: enabled(pid=thisproc)\");", " if (pid < 0 || pid >= (int) now._nr_pr)", " return 0;", " this = pptr(pid);", " TstOnly = 1;", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " for (t = trans[ot][tt]; t; t = t->nxt)", " if (do_transit(t, (short) pid))", " { res = 1;", " break;", " }", " TstOnly = 0;", " this = othis;", " return res;", "}", "#endif", "void", "snap_time(void)", "{ clock_t stop_time;", " double delta_time;", "#if !defined(WIN32) && !defined(WIN64)", " struct tms stop_tm;", " stop_time = times(&stop_tm);", " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));", "#else", " stop_time = clock();", " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);", "#endif", " if (delta_time > 0.01)", " { printf(\"t= %%8.3g \", delta_time);", " printf(\"R= %%7.0g\", nstates/delta_time);", " }", " printf(\"\\n\");", " if (quota > 0.1 && delta_time > quota)", " { printf(\"Time limit of %%6.3g minutes exceeded\\n\", quota/60.0);", "#if NCORE>1", " fflush(stdout);", " leave_critical(GLOBAL_LOCK);", " sudden_stop(\"time-limit\");", " exit(1);", "#endif", " wrapup();", " }", "}", "void", "snapshot(void)", "{", "#if NCORE>1", " enter_critical(GLOBAL_LOCK); /* snapshot */", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"Depth= %%7ld States= %%8.3g \",", "#if NCORE>1", " (long) (nr_handoffs * z_handoff) +", "#endif", " mreached, nstates);", " printf(\"Transitions= %%8.3g \", nstates+truncs);", "#ifdef MA", " printf(\"Nodes= %%7d \", nr_states);", "#endif", " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);", " snap_time();", " fflush(stdout);", "#if NCORE>1", " leave_critical(GLOBAL_LOCK);", "#endif", "}", "#ifdef SC", "void", "stack2disk(void)", "{", " if (!stackwrite", " && (stackwrite = creat(stackfile, TMODE)) < 0)", " Uerror(\"cannot create stackfile\");", "", " if (write(stackwrite, trail, DDD*sizeof(Trail))", " != DDD*sizeof(Trail))", " Uerror(\"stackfile write error -- disk is full?\");", "", " memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));", " memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));", " CNT1++;", "}", "void", "disk2stack(void)", "{ long have;", "", " CNT2++;", " memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));", "", " if (!stackwrite", " || lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)", " Uerror(\"disk2stack lseek error\");", "", " if (!stackread", " && (stackread = open(stackfile, 0)) < 0)", " Uerror(\"cannot open stackfile\");", "", " if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)", " Uerror(\"disk2stack lseek error\");", "", " have = read(stackread, trail, DDD*sizeof(Trail));", " if (have != DDD*sizeof(Trail))", " Uerror(\"stackfile read error\");", "}", "#endif", "uchar *", "Pptr(int x)", "{ if (x < 0 || x >= MAXPROC", /* does not exist */ "#ifdef TRIX", " || !processes[x])", "#else", " || !proc_offset[x])", "#endif", " return noptr;", " else", " return (uchar *) pptr(x);", "}\n", "uchar *", "Qptr(int x)", "{ if (x < 0 || x >= MAXQ", "#ifdef TRIX", " || !channels[x])", "#else", " || !q_offset[x])", "#endif", " return noqptr;", " else", " return (uchar *) qptr(x);", "}\n", "int qs_empty(void);", "#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))", "#ifdef NSUCC", "int N_succ[512];", "void", "tally_succ(int cnt)", "{ if (cnt < 512) N_succ[cnt]++;", " else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);", "}", "", "void", "dump_succ(void)", "{ int i; double sum = 0.0;", " double w_avg = 0.0;", " printf(\"Successor counts:\\n\");", " for (i = 0; i < 512; i++)", " { sum += (double) N_succ[i];", " }", " for (i = 0; i < 512; i++)", " { if (N_succ[i] > 0)", " { printf(\"%%3d\t%%10d\t(%%.4g %%%% of total)\\n\",", " i, N_succ[i], (100.0 * (double) N_succ[i])/sum);", " w_avg += (double) i * (double) N_succ[i];", " } }", " if (sum > N_succ[0])", " printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));", "}", "#endif", "", "#if NCLAIMS>1", "void", "select_claim(int n)", "{ int m, i;", " if (n < 0 || n >= NCLAIMS)", " { uerror(\"non-existing claim\");", " } else", " { m = ((Pclaim *)pptr(0))->_n;", " if (verbose)", " { printf(\"%%d: Claim %%s (%%d), from state %%d\\n\",", " (int) depth, procname[spin_c_typ[n]],", " n, ((Pclaim *)pptr(0))->c_cur[n]);", " }", " ((Pclaim *)pptr(0))->c_cur[m] = ((Pclaim *)pptr(0))->_p;", " ((Pclaim *)pptr(0))->_t = spin_c_typ[n];", " ((Pclaim *)pptr(0))->_p = ((Pclaim *)pptr(0))->c_cur[n];", " ((Pclaim *)pptr(0))->_n = n;", " for (i = 0; src_all[i].src != (short *) 0; i++)", " { if (src_all[i].tp == spin_c_typ[n])", " { src_claim = src_all[i].src;", " break;", " } }", " if (src_all[i].src == (short *) 0)", " { uerror(\"cannot happen: src_ln ref\");", " } }", "}", "#else", "void", "select_claim(int n)", "{ if (n != 0) uerror(\"non-existing claim\");", "}", "#endif", "", "#ifdef REVERSE", " #define FROM_P (BASE)", " #define UPTO_P (now._nr_pr-1)", " #define MORE_P (II <= To)", /* p.o. only */ " #define INI_P (From-1)", /* fairness only */ " #define ALL_P (II = From; II <= To; II++)", "#else", " #define FROM_P (now._nr_pr-1)", " #define UPTO_P (BASE)", " #define MORE_P (II >= BASE)", " #define INI_P (From+1)", " #define ALL_P (II = From; II >= To; II--)", "#endif", "/*", " * new_state() is the main DFS search routine in the verifier", " * it has a lot of code ifdef-ed together to support", " * different search modes, which makes it quite unreadable.", " * if you are studying the code, use the C preprocessor", " * to generate a specific version from the pan.c source,", " * e.g. by saying:", " * gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c", " * and then study the resulting file, instead of this version", " */", "", "void", "new_state(void)", "{ Trans *t;", " uchar _n, _m, ot;", "#ifdef T_RAND", " short ooi, eoi;", "#endif", "#ifdef M_LOSS", " uchar delta_m = 0;", "#endif", " short II, JJ = 0, kk;", " int tt;", " short From = FROM_P, To = UPTO_P;", "#ifdef BCS", " trpt->sched_limit = 0; /* at depth=0 only */", "#endif", "Down:", "#ifdef CHECK", " cpu_printf(\"%%d: Down - %%s %%saccepting [pids %%d-%%d]\\n\",", " depth, (trpt->tau&4)?\"claim\":\"program\",", " (trpt->o_pm&2)?\"\":\"non-\", From, To);", "#endif", "#ifdef P_RAND", " trpt->p_skip = -1;", "#endif", "#ifdef SC", " if (depth > hiwater)", " { stack2disk();", " maxdepth += DDD;", " hiwater += DDD;", " trpt -= DDD;", " if(verbose)", " printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",", " CNT1, hiwater, maxdepth);", " }", "#endif", " trpt->tau &= ~(16|32|64); /* make sure these are off */", "#if defined(FULLSTACK) && defined(MA)", " trpt->proviso = 0;", "#endif", "#ifdef NSUCC", " trpt->n_succ = 0;", "#endif", "#if NCORE>1", " if (mem_hand_off())", " {", "#if SYNC", " (trpt+1)->o_n = 1; /* not a deadlock: as below */", "#endif", "#ifndef LOOPSTATE", " (trpt-1)->tau |= 16; /* worstcase guess: as below */", "#endif", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", "#endif", " if (depth >= maxdepth)", " { if (!warned)", " { warned = 1;", " printf(\"error: max search depth too small\\n\");", " }", " if (bounded)", " { uerror(\"depth limit reached\");", " }", " truncs++;", "#if SYNC", " (trpt+1)->o_n = 1; /* not a deadlock */", "#endif", "#ifndef LOOPSTATE", " (trpt-1)->tau |= 16; /* worstcase guess */", "#endif", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", "AllOver:", "#if (defined(FULLSTACK) && !defined(MA)) || NCORE>1", " /* if atomic or rv move, carry forward previous state */", " trpt->ostate = (trpt-1)->ostate;", "#endif", "#ifdef VERI", " if ((trpt->tau&4) || ((trpt-1)->tau&128))", "#endif", " if (boq == -1) { /* if not mid-rv */", "#ifndef SAFETY", " /* this check should now be redundant", " * because the seed state also appears", " * on the 1st dfs stack and would be", " * matched in hstore below", " */", " if ((now._a_t&1) && depth > A_depth)", " { if (!memcmp((char *)&A_Root, ", " (char *)&now, vsize))", " {", " depthfound = A_depth;", "#ifdef CHECK", " printf(\"matches seed\\n\");", "#endif", "#ifdef NP", " uerror(\"non-progress cycle\");", "#else", " uerror(\"acceptance cycle\");", "#endif", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", "#ifdef CHECK", " printf(\"not seed\\n\");", "#endif", " }", "#endif", " if (!(trpt->tau&8)) /* if no atomic move */", " {", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " uchar was_last = now._last;", " now._last = 0; /* value not stored */", "#endif", "#ifdef BITSTATE", "#ifdef CNTRSTACK", /* -> bitstate, reduced, safety */ " #if defined(BCS) && defined(STORE_CTX)", " { int xj;", " for (xj = trpt->sched_limit; xj <= sched_max; xj++)", " { now._ctx = xj;", " II = bstore((char *)&now, vsize);", " trpt->j6 = j1_spin; trpt->j7 = j2;", " JJ = LL[j1_spin] && LL[j2];", " if (II != 0) { break; }", " }", " now._ctx = 0; /* just in case */", " }", " #else", " II = bstore((char *)&now, vsize);", " trpt->j6 = j1_spin; trpt->j7 = j2;", " JJ = LL[j1_spin] && LL[j2];", " #endif", "#else", " #ifdef FULLSTACK", /* bstore after onstack_now, to preserve j1-j4 */ " #if defined(BCS) && defined(STORE_CTX)", " { int xj;", " now._ctx = 0;", " JJ = onstack_now();", /* mangles j1 */ " for (xj = trpt->sched_limit; xj <= sched_max; xj++)", " { now._ctx = xj;", " II = bstore((char *)&now, vsize);", /* sets j1-j4 */ " if (II != 0) { break; }", " }", " now._ctx = 0;", " }", " #else", " JJ = onstack_now();", /* mangles j1 */ " II = bstore((char *)&now, vsize);", /* sets j1-j4 */ " #endif", " #else", " #if defined(BCS) && defined(STORE_CTX)", " { int xj;", " for (xj = trpt->sched_limit; xj <= sched_max; xj++)", " { now._ctx = xj;", " II = bstore((char *)&now, vsize);", /* sets j1-j4 */ " JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */", " if (II != 0) { break; }", " }", " now._ctx = 0;", " }", " #else", " II = bstore((char *)&now, vsize);", /* sets j1-j4 */ " JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */", " #endif", " #endif", "#endif", "#else", "#ifdef MA", " II = gstore((char *)&now, vsize, 0);", "#ifndef FULLSTACK", " JJ = II;", "#else", " JJ = (II == 2)?1:0;", "#endif", "#else", " II = hstore((char *)&now, vsize);", " /* @hash j1_spin II */", "#ifdef FULLSTACK", " JJ = (II == 2)?1:0;", "#endif", "#endif", "#endif", " kk = (II == 1 || II == 2);", /* actually, BCS implies HAS_LAST */ "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " now._last = was_last; /* restore value */", "#endif", /* II==0 new state */ /* II==1 old state */ /* II==2 on current dfs stack */ /* II==3 on 1st dfs stack */ "#ifndef SAFETY", "#if NCORE==1 || defined (SEP_STATE)", /* or else we don't know which stack its on */ " if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))", " #ifndef NOFAIR", "#if 0", " if (!fairness || ((now._a_t&1) && now._cnt[1] == 1)) /* 5.1.4 */", "#else", " if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */", "#endif", " #endif", " {", " II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */", "#ifdef VERBOSE", " printf(\"state match on dfs stack\\n\");", "#endif", " goto same_case;", " }", "#endif", "#if defined(FULLSTACK) && defined(BITSTATE)", " if (!JJ && (now._a_t&1) && depth > A_depth)", " { int oj1 = j1_spin;", " uchar o_a_t = now._a_t;", " now._a_t &= ~(1|16|32);", /* 1st stack */ " if (onstack_now())", /* changes j1_spin */ " { II = 3;", "#ifdef VERBOSE", " printf(\"state match on 1st dfs stack\\n\");", "#endif", " }", " now._a_t = o_a_t;", /* restore */ " j1_spin = oj1;", " }", "#endif", " if (II == 3 && a_cycles && (now._a_t&1))", " {", "#ifndef NOFAIR", " if (fairness && now._cnt[1] > 1) /* was != 0 */", " {", "#ifdef VERBOSE", " printf(\"\tfairness count non-zero\\n\");", "#endif", " II = 0;", /* treat as new state */ " } else", "#endif", " {", "#ifndef BITSTATE", " nShadow--;", "#endif", "same_case: if (Lstate) depthfound = Lstate->D;", "#ifdef NP", " uerror(\"non-progress cycle\");", "#else", " uerror(\"acceptance cycle\");", "#endif", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", " }", "#endif", "#ifndef NOREDUCE", " #ifndef SAFETY", " #if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)", " if (II != 0 && (!Lstate || Lstate->cpu_id < core_id))", " { (trpt-1)->tau |= 16;", /* treat as a stack state */ " }", " #endif", " if ((II && JJ) || (II == 3))", " { /* marker for liveness proviso */", " #ifndef LOOPSTATE", " (trpt-1)->tau |= 16;", /* truncated on stack */ " #endif", " truncs2++;", " }", "#else", " #if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)", " if (!(II != 0 && (!Lstate || Lstate->cpu_id < core_id)))", " { /* treat as stack state */", " (trpt-1)->tau |= 16;", " } else", " { /* treat as non-stack state */", " (trpt-1)->tau |= 64;", " }", " #endif", " if (!II || !JJ)", " { /* successor outside stack */", " (trpt-1)->tau |= 64;", " }", " #endif", "#endif", "#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))", /* needed for BCS - cover cases where it would not otherwise be set */ " if (!II || !JJ)", " { (trpt-1)->tau |= 64;", " }", "#endif", " if (II)", " { truncs++;", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " if (depth == 0)", " { return;", " } }", "#endif", " goto Up;", " }", " if (!kk)", " { static long sdone = (long) 0; long ndone;", " nstates++;", "#if defined(ZAPH) && defined(BITSTATE)", " zstates += (double) hfns;", "#endif", " ndone = (unsigned long) (nstates/(freq));", " if (ndone != sdone)", " { snapshot();", " sdone = ndone;", "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)", " if (nstates > ((double)(ONE_L<<(ssize+1))))", " { void resize_hashtable(void);", " resize_hashtable();", " }", "#endif", "#if defined(ZAPH) && defined(BITSTATE)", " if (zstates > ((double)(ONE_L<<(ssize-2))))", " { /* more than half the bits set */", " void zap_hashtable(void);", " zap_hashtable();", " zstates = 0;", " }", "#endif", " }", "#ifdef SVDUMP", " if (vprefix > 0)", " #ifdef SHO", /* Store Hash Only */ " /* always use the same hashfunction, for consistency across runs */", " if (HASH_NR != 0)", " { int oh = HASH_NR;", " HASH_NR = 0;", " d_hash((char *) &now, vsize); /* set K1 */", " HASH_NR = oh;", " }", " if (write(svfd, (uchar *) &K1, sizeof(unsigned long)) != sizeof(unsigned long))", " #else", " if (write(svfd, (uchar *) &now, vprefix) != vprefix)", " #endif", " { fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);", " wrapup();", " }", "#endif", "#if defined(MA) && defined(W_XPT)", " if ((unsigned long) nstates%%W_XPT == 0)", " { void w_xpoint(void);", " w_xpoint();", " }", "#endif", " }", "#if defined(FULLSTACK) || defined(CNTRSTACK)", " onstack_put();", "#ifdef DEBUG2", "#if defined(FULLSTACK) && !defined(MA)", " printf(\"%%d: putting %%u (%%d)\\n\", depth,", " trpt->ostate, ", " (trpt->ostate)?trpt->ostate->tagged:0);", "#else", " printf(\"%%d: putting\\n\", depth);", "#endif", "#endif", "#else", " #if NCORE>1", " trpt->ostate = Lstate;", " #endif", "#endif", " } }", " if (depth > mreached)", " mreached = depth;", "#ifdef VERI", " if (trpt->tau&4)", "#endif", " trpt->tau &= ~(1|2); /* timeout and -request off */", " _n = 0;", "#if SYNC", " (trpt+1)->o_n = 0;", "#endif", "#ifdef VERI", " if (now._nr_pr == 0) /* claim terminated */", " uerror(\"end state in claim reached\");", "", " if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])", " { uerror(\"end state in claim reached\");", " }", "Stutter:", " if (trpt->tau&4) /* must make a claimmove */", " {", "#ifndef NOFAIR", " if ((now._a_t&2) /* A-bit set */", " && now._cnt[now._a_t&1] == 1)", " { now._a_t &= ~2;", " now._cnt[now._a_t&1] = 0;", " trpt->o_pm |= 16;", "#ifdef DEBUG", " printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",", " depth, now._a_t);", "#endif", " }", "#endif", " II = 0; /* never */", " goto Veri0;", " }", "#endif", "#ifndef NOREDUCE", " /* Look for a process with only safe transitions */", " /* (special rules apply in the 2nd dfs) */", " if (boq == -1 && From != To", "", "#ifdef SAFETY", " #if NCORE>1", " && (depth < z_handoff)", /* not for border states */ " #endif", " )", "#else", " #if NCORE>1", " && ((a_cycles) || (!a_cycles && depth < z_handoff))", " #endif", " #ifdef BCS", " && (sched_max > 0 || depth > BASE)", /* no po in initial state if -L0 */ " #endif", " && (!(now._a_t&1)", " || (a_cycles &&", " #ifndef BITSTATE", "#ifdef MA", "#ifdef VERI", " !((trpt-1)->proviso))", "#else", " !(trpt->proviso))", "#endif", "#else", "#ifdef VERI", " (trpt-1)->ostate &&", " !(((char *)&((trpt-1)->ostate->state))[0] & 128))", /* proviso bit in _a_t */ "#else", " !(((char *)&(trpt->ostate->state))[0] & 128))", "#endif", "#endif", " #else", "#ifdef VERI", " (trpt-1)->ostate &&", " (trpt-1)->ostate->proviso == 0)", "#else", " trpt->ostate->proviso == 0)", "#endif", " #endif", " ))", "#endif", /* SAFETY */ " /* attempt Partial Order Reduction as preselect moves */", "#ifdef BCS", " if (trpt->sched_limit < sched_max)", /* po only if we can switch */ "#endif", " { for ALL_P", " {", "Resume: /* pick up here if preselect fails */", " this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " if (trans[ot][tt]->atom & 8)", " { t = trans[ot][tt];", " if (t->qu[0] != 0)", " { Ccheck++;", " if (!q_cond(II, t))", " continue;", " Cholds++;", " }", "SelectIt: From = To = II; /* preselect process */", "#ifdef NIBIS", " t->om = 0;", "#endif", " trpt->tau |= 32; /* preselect marker */", "#ifdef DEBUG", " printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ", " depth, II, trpt->tau);", "#endif", " goto Again;", " } } }", " trpt->tau &= ~32;", "#endif", "#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))", "Again:", "#endif", " trpt->o_pm &= ~(8|16|32|64); /* clear fairness-marks */", "#ifndef NOFAIR", " if (fairness && boq == -1", "#ifdef VERI", " && (!(trpt->tau&4) && !((trpt-1)->tau&128))", "#endif", " && !(trpt->tau&8))", " { /* A_bit = 1; Cnt = N in acc states with A_bit 0 */", " if (!(now._a_t&2))", /* A-bit not set */ " { if (a_cycles && (trpt->o_pm&2))", " { /* Accepting state */", " now._a_t |= 2;", " now._cnt[now._a_t&1] = now._nr_pr + 1;", " trpt->o_pm |= 8;", "#ifdef DEBUG", " printf(\"%%3ld: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",", " depth, now._cnt[now._a_t&1], now._a_t);", "#endif", " }", " } else", /* A-bit set */ " { /* A_bit = 0 when Cnt 0 */", " if (now._cnt[now._a_t&1] == 1)", " { now._a_t &= ~2;", /* reset a-bit */ " now._cnt[now._a_t&1] = 0;", " trpt->o_pm |= 16;", "#ifdef DEBUG", " printf(\"%%3ld: fairness Rule 3: _a_t = %%d\\n\",", " depth, now._a_t);", "#endif", " } } }", "#endif", "#ifdef BCS", /* bounded context switching */ " trpt->bcs = trpt->b_pno = 0; /* initial */", " if (From != To /* not a PO or atomic move */", " && depth > BASE) /* there is a prior move */", " { trpt->b_pno = now._last + BASE;", " trpt->bcs = B_PHASE1;", " #ifdef VERBOSE", " printf(\"%%3ld: BCS phase 1 proc %%d limit %%d\\n\",", " depth, trpt->b_pno, trpt->sched_limit);", " #endif", " /* allow only process b_pno to move in this phase */", " }", "c_switch: /* jumps here with bcs == B_PHASE2 with or wo B_FORCED added */", " #ifdef VERBOSE", " printf(\"%%3ld: BCS c_switch phase=%%d pno=%%d [forced %%d]\\n\",", " depth, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);", " #endif", "#endif", "#ifdef P_RAND", " #ifdef REVERSE", " trpt->p_left = 1 + (To - From);", " #else", " trpt->p_left = 1 + (From - To);", " #endif", " if (trpt->p_left > 1)", " { trpt->p_skip = rand() %% (trpt->p_left);", " } else", " { trpt->p_skip = -1;", " }", "r_switch:", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND r_switch p_skip=%%d p_left=%%d\\n\",", " depth, trpt->p_skip, trpt->p_left);", " #endif", "#endif", " /* Main Expansion Loop over Processes */", " for ALL_P", " {", "#ifdef P_RAND", " if (trpt->p_skip >= 0)", " { trpt->p_skip--; /* skip random nr of procs */", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND skipping %%d [new p_skip=%%d p_left=%%d]\\n\",", " depth, II, trpt->p_skip, trpt->p_left);", " #endif", " continue;", " }", " if (trpt->p_left == 0)", " {", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND done at %%d\\n\", depth, II);", " #endif", " break; /* done */", " }", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND explore %%d [p_left=%%d]\\n\",", " depth, II, trpt->p_left);", " #endif", " trpt->p_left--;", "#endif", "#if SYNC", " /* no rendezvous with same proc */", " if (boq != -1 && trpt->pr == II) continue;", "#endif", "#ifdef BCS", /* never claim with II==0 cannot get here */ " if ((trpt->bcs & B_PHASE1)", " && trpt->b_pno != II)", " {", " #ifdef VERBOSE", " printf(\"%%3ld: BCS NotPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",", " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);", " #endif", " continue;", /* avoid context switch */ " }", " #ifdef VERBOSE", " else if ((trpt->bcs & B_PHASE1) && trpt->b_pno == II)", " printf(\"%%3ld: BCS IsPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",", " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);", " #endif", " if (trpt->bcs & B_PHASE2) /* 2nd phase */", " { if (trpt->b_pno == II) /* was already done in phase 1 */", " {", " #ifdef VERBOSE", " printf(\"%%3ld: BCS NoRepeat II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",", " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);", " #endif", " continue;", " }", " if (!(trpt->bcs & B_FORCED) /* unless forced */", " && trpt->sched_limit >= sched_max)", " {", " #ifdef VERBOSE", " printf(\"%%3ld: BCS Bound II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",", " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);", " #endif", " continue; /* enforce bound */", " } }", "#endif", "#ifdef VERI", "Veri0:", "#endif", " this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", "#ifdef NIBIS", " /* don't repeat a previous preselected expansion */", " /* could hit this if reduction proviso was false */", " t = trans[ot][tt];", " if (!(trpt->tau&4)", /* not claim */ " && !(trpt->tau&1)", /* not timeout */ " && !(trpt->tau&32)", /* not preselected */ " && (t->atom & 8)", /* local */ " && boq == -1", /* not inside rendezvous */ " && From != To)", /* not inside atomic seq */ " { if (t->qu[0] == 0", /* unconditional */ " || q_cond(II, t))", /* true condition */ " { _m = t->om;", " if (_m>_n||(_n>3&&_m!=0)) _n=_m;", " continue; /* did it before */", " } }", "#endif", " trpt->o_pm &= ~1; /* no move in this pid yet */", "#ifdef EVENT_TRACE", " (trpt+1)->o_event = now._event;", "#endif", " /* Fairness: Cnt++ when Cnt == II */", "#ifndef NOFAIR", " trpt->o_pm &= ~64; /* didn't apply rule 2 */", " if (fairness", " && boq == -1", /* not mid rv - except rcv - NEW 3.0.8 */ " && !(trpt->o_pm&32)", /* Rule 2 not in effect */ " && (now._a_t&2)", /* A-bit is set */ " && now._cnt[now._a_t&1] == II+2)", " { now._cnt[now._a_t&1] -= 1;", "#ifdef VERI", " /* claim need not participate */", " if (II == 1)", " now._cnt[now._a_t&1] = 1;", "#endif", "#ifdef DEBUG", " printf(\"%%3ld: proc %%d fairness \", depth, II);", " printf(\"Rule 2: --cnt to %%d (%%d)\\n\",", " now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm |= (32|64);", " }", "#endif", "#ifdef HAS_PROVIDED", " if (!provided(II, ot, tt, t)) continue;", "#endif", " /* check all trans of proc II - escapes first */", "#ifdef HAS_UNLESS", " trpt->e_state = 0;", "#endif", " (trpt+1)->pr = (uchar) II;", /* for uerror */ " (trpt+1)->st = tt;", "#ifdef T_RAND", " for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)", " { if (strcmp(t->tp, \"else\") == 0", "#ifdef HAS_UNLESS", " || t->e_trans != 0", "#endif", " )", " { eoi++;", /* no break, must count ooi */ " } }", " if (eoi > 0)", " { t = trans[ot][tt];", " #ifdef VERBOSE", " printf(\"randomizer: suppressed, saw else or escape\\n\");", " #endif", " } else", " { eoi = rand()%%ooi;", " #ifdef VERBOSE", " printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);", " #endif", " for (t = trans[ot][tt]; t; t = t->nxt)", " if (eoi-- <= 0) break;", " }", "domore:", " for ( ; t && ooi > 0; t = t->nxt, ooi--)", "#else", /* ie dont randomize */ " for (t = trans[ot][tt]; t; t = t->nxt)", "#endif", " {", "#ifdef HAS_UNLESS", " /* exploring all transitions from", " * a single escape state suffices", " */", " if (trpt->e_state > 0", " && trpt->e_state != t->e_trans)", " {", "#ifdef DEBUG", " printf(\"skip 2nd escape %%d (did %%d before)\\n\",", " t->e_trans, trpt->e_state);", "#endif", " break;", " }", "#endif", " #if defined(TRIX) && !defined(TRIX_ORIG) && !defined(BFS)", " (trpt+1)->p_bup = now._ids_[II];", " #endif", " (trpt+1)->o_t = t;", /* for uerror */ "#ifdef INLINE", "#include FORWARD_MOVES", "P999: /* jumps here when move succeeds */", "#else", " if (!(_m = do_transit(t, II))) continue;", "#endif", "#ifdef BCS", " if (depth > BASE", /* has prior move */ " && II >= BASE", /* not claim */ " && From != To", /* not atomic or po */ " #ifndef BCS_NOFIX", " /* added 5.2.5: prior move was not po */", " && !((trpt-(BASE+1))->tau & 32)", " #endif", " && boq == -1", /* not rv */ " && (trpt->bcs & B_PHASE2)", " && trpt->b_pno != II /* context switch */", /* redundant */ " && !(trpt->bcs & B_FORCED)) /* unless forced */", " { (trpt+1)->sched_limit = 1 + trpt->sched_limit;", " #ifdef VERBOSE", " printf(\"%%3ld: up sched count to %%d\\n\", depth, (trpt+1)->sched_limit);", " #endif", " } else", " { (trpt+1)->sched_limit = trpt->sched_limit;", " #ifdef VERBOSE", " printf(\"%%3ld: keep sched count at %%d\\n\", depth, (trpt+1)->sched_limit);", " #endif", " }", "#endif", " if (boq == -1)", "#ifdef CTL", " /* for branching-time, can accept reduction only if */", " /* the persistent set contains just 1 transition */", " { if ((trpt->tau&32) && (trpt->o_pm&1))", " trpt->tau |= 16;", /* CTL */ " trpt->o_pm |= 1; /* we moved */", " }", "#else", " trpt->o_pm |= 1; /* we moved */", "#endif", "#ifdef LOOPSTATE", " if (loopstate[ot][tt])", " {", "#ifdef VERBOSE", " printf(\"exiting from loopstate:\\n\");", "#endif", " trpt->tau |= 16;", /* exiting loopstate */ " cnt_loops++;", " }", "#endif", "#ifdef PEG", " peg[t->forw]++;", "#endif", "#if defined(VERBOSE) || defined(CHECK)", "#if defined(SVDUMP)", " cpu_printf(\"%%3ld: proc %%d exec %%d \\n\", depth, II, t->t_id);", "#else", " cpu_printf(\"%%3ld: proc %%d exec %%d, %%d to %%d, %%s %%s %%s %%saccepting [tau=%%d]\\n\", ", " depth, II, t->forw, tt, t->st, t->tp,", " (t->atom&2)?\"atomic\":\"\",", " (boq != -1)?\"rendez-vous\":\"\",", " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);", "#ifdef HAS_UNLESS", " if (t->e_trans)", " cpu_printf(\"\\t(escape to state %%d)\\n\", t->st);", "#endif", "#endif", "#ifdef T_RAND", " cpu_printf(\"\\t(randomizer %%d)\\n\", ooi);", "#endif", "#endif", "#ifdef HAS_LAST", "#ifdef VERI", " if (II != 0)", "#endif", " now._last = II - BASE;", "#endif", "#ifdef HAS_UNLESS", " trpt->e_state = t->e_trans;", "#endif", " depth++; trpt++;", " trpt->pr = (uchar) II;", " trpt->st = tt;", " trpt->o_pm &= ~(2|4);", " if (t->st > 0)", " { ((P0 *)this)->_p = t->st;", "/* moved down reached[ot][t->st] = 1; */", " }", "#ifndef SAFETY", " if (a_cycles)", " {", "#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))", " int ii;", "#endif", "#define P__Q ((P0 *)pptr(ii))", "#if ACCEPT_LAB>0", "#ifdef NP", " /* state 1 of np_ claim is accepting */", " if (((P0 *)pptr(0))->_p == 1)", " trpt->o_pm |= 2;", "#else", " for (ii = 0; ii < (int) now._nr_pr; ii++)", " { if (accpstate[P__Q->_t][P__Q->_p])", " { trpt->o_pm |= 2;", " break;", " } }", "#endif", "#endif", "#if defined(HAS_NP) && PROG_LAB>0", " for (ii = 0; ii < (int) now._nr_pr; ii++)", " { if (progstate[P__Q->_t][P__Q->_p])", " { trpt->o_pm |= 4;", " break;", " } }", "#endif", "#undef P__Q", " }", "#endif", " trpt->o_t = t; trpt->o_n = _n;", " trpt->o_ot = ot; trpt->o_tt = tt;", " trpt->o_To = To; trpt->o_m = _m;", " trpt->tau = 0;", "#ifdef T_RAND", " trpt->oo_i = ooi;", "#endif", " if (boq != -1 || (t->atom&2))", " { trpt->tau |= 8;", "#ifdef VERI", " /* atomic sequence in claim */", " if((trpt-1)->tau&4)", " trpt->tau |= 4;", " else", " trpt->tau &= ~4;", " } else", " { if ((trpt-1)->tau&4)", " trpt->tau &= ~4;", " else", " trpt->tau |= 4;", " }", " /* if claim allowed timeout, so */", " /* does the next program-step: */", " if (((trpt-1)->tau&1) && !(trpt->tau&4))", " trpt->tau |= 1;", "#else", " } else", " trpt->tau &= ~8;", "#endif", " if (boq == -1 && (t->atom&2))", " { From = To = II; nlinks++;", " } else", " { From = FROM_P; To = UPTO_P;", " }", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Push_Stack_Tree(II, t->t_id);", " }", "#endif", "#ifdef TRIX", " if (processes[II])", /* last move could have been a delproc */ " { processes[II]->modified = 1; /* transition in II */", " #ifdef V_TRIX", " printf(\"%%4d: process %%d modified\\n\", depth, II);", " } else", " { printf(\"%%4d: process %%d modified but gone (%%p)\\n\",", " depth, II, trpt);", " #endif", " }", "#endif", " goto Down; /* pseudo-recursion */", "Up:", "#ifdef TRIX", " #ifndef TRIX_ORIG", " #ifndef BFS", " now._ids_[trpt->pr] = trpt->p_bup;", " #endif", " #else", " if (processes[trpt->pr])", " {", " processes[trpt->pr]->modified = 1; /* reverse move */", " #ifdef V_TRIX", " printf(\"%%4d: unmodify pr %%d (%%p)\\n\",", " depth, trpt->pr, trpt);", " } else", " { printf(\"%%4d: unmodify pr %%d (gone) (%%p)\\n\",", " depth, trpt->pr, trpt);", " #endif", " }", " #endif", "#endif", "#ifdef CHECK", " cpu_printf(\"%%d: Up - %%s\\n\", depth,", " (trpt->tau&4)?\"claim\":\"program\");", "#endif", "#if NCORE>1", " iam_alive();", " #ifdef USE_DISK", " mem_drain();", " #endif", "#endif", "#if defined(MA) || NCORE>1", " if (depth <= 0) return;", " /* e.g., if first state is old, after a restart */", "#endif", "#ifdef SC", " if (CNT1 > CNT2", " && depth < hiwater - (HHH-DDD) - 2)", /* 5.1.6: was + 2 */ " {", " trpt += DDD;", " disk2stack();", " maxdepth -= DDD;", " hiwater -= DDD;", " if(verbose)", " printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);", " }", "#endif", "#ifndef SAFETY", /* moved earlier in version 5.2.5 */ " if ((now._a_t&1) && depth <= A_depth)", " return; /* to checkcycles() */", "#endif", "#ifndef NOFAIR", " if (trpt->o_pm&128) /* fairness alg */", " { now._cnt[now._a_t&1] = trpt->bup.oval;", " _n = 1; trpt->o_pm &= ~128;", " depth--; trpt--;", "#if defined(VERBOSE) || defined(CHECK)", " printf(\"%%3ld: reversed fairness default move\\n\", depth);", "#endif", " goto Q999;", " }", "#endif", "#ifdef HAS_LAST", "#ifdef VERI", " { int d; Trail *trl;", " now._last = 0;", " for (d = 1; d < depth; d++)", " { trl = getframe(depth-d); /* was (trpt-d) */", " if (trl->pr != 0)", " { now._last = trl->pr - BASE;", " break;", " } } }", "#else", " now._last = (depth<1)?0:(trpt-1)->pr;", "#endif", "#endif", "#ifdef EVENT_TRACE", " now._event = trpt->o_event;", "#endif", " t = trpt->o_t; _n = trpt->o_n;", " ot = trpt->o_ot; II = trpt->pr;", " tt = trpt->o_tt; this = Pptr(II);", " To = trpt->o_To; _m = trpt->o_m;", "#ifdef T_RAND", " ooi = trpt->oo_i;", "#endif", "#ifdef INLINE_REV", " _m = do_reverse(t, II, _m);", "#else", "#include REVERSE_MOVES", "R999: /* jumps here when done */", "#endif", "#ifdef VERBOSE", " cpu_printf(\"%%3ld: proc %%d reverses %%d, %%d to %%d\\n\",", " depth, II, t->forw, tt, t->st);", " cpu_printf(\"\\t%%s [abit=%%d,adepth=%%d,tau=%%d,%%d]\\n\", ", " t->tp, now._a_t, A_depth, trpt->tau, (trpt-1)->tau);", "#endif", "#ifndef NOREDUCE", " /* pass the proviso tags */", " if ((trpt->tau&8) /* rv or atomic */", " && (trpt->tau&16))", " (trpt-1)->tau |= 16;", /* pass upward */ " #ifdef SAFETY", " if ((trpt->tau&8) /* rv or atomic */", " && (trpt->tau&64))", " (trpt-1)->tau |= 64;", " #endif", "#endif", "#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))", /* for BCS, cover cases where 64 is otherwise not handled */ " if ((trpt->tau&8)", " && (trpt->tau&64))", " (trpt-1)->tau |= 64;", "#endif", " depth--; trpt--;", "", "#ifdef NSUCC", " trpt->n_succ++;", "#endif", "#ifdef NIBIS", " (trans[ot][tt])->om = _m; /* head of list */", "#endif", " /* i.e., not set if rv fails */", " if (_m)", " { reached[ot][t->st] = 1;", " reached[ot][tt] = 1;", " }", "#ifdef HAS_UNLESS", " else trpt->e_state = 0; /* undo */", "#endif", " if (_m>_n||(_n>3&&_m!=0)) _n=_m;", " ((P0 *)this)->_p = tt;", " } /* all options */", "#ifdef T_RAND", " if (!t && ooi > 0)", /* means we skipped some initial options */ " { t = trans[ot][tt];", " #ifdef VERBOSE", " printf(\"randomizer: continue for %%d more\\n\", ooi);", " #endif", " goto domore;", " }", " #ifdef VERBOSE", " else", " printf(\"randomizer: done\\n\");", " #endif", "#endif", "#ifndef NOFAIR", " /* Fairness: undo Rule 2 */", " if ((trpt->o_pm&32)",/* rule 2 was applied */ " && (trpt->o_pm&64))",/* by this process II */ " { if (trpt->o_pm&1)",/* it didn't block */ " {", "#ifdef VERI", " if (now._cnt[now._a_t&1] == 1)", " now._cnt[now._a_t&1] = 2;", "#endif", " now._cnt[now._a_t&1] += 1;", "#ifdef VERBOSE", " printf(\"%%3ld: proc %%d fairness \", depth, II);", " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",", " now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm &= ~(32|64);", " } else", /* process blocked */ " { if (_n > 0)", /* a prev proc didn't */ " {", /* start over */ " trpt->o_pm &= ~64;", " II = INI_P;", /* after loop incr II == From */ " } } }", "#endif", "#ifdef VERI", " if (II == 0) break; /* never claim */", "#endif", " } /* all processes */", "#ifdef NSUCC", " tally_succ(trpt->n_succ);", "#endif", "#ifdef P_RAND", " if (trpt->p_left > 0)", " { trpt->p_skip = -1; /* probably rendundant */", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND -- explore remainder\\n\", depth);", " #endif", " goto r_switch; /* explore the remaining procs */", " } else", " {", " #ifdef VERBOSE", " printf(\"%%3ld: P_RAND -- none left\\n\", depth);", " #endif", " }", "#endif", "#ifdef BCS", " if (trpt->bcs & B_PHASE1)", " { trpt->bcs = B_PHASE2; /* start 2nd phase */", " if (_n == 0 || !(trpt->tau&64)) /* pre-move unexecutable or led to stackstate */", " { trpt->bcs |= B_FORCED; /* forced switch */", " }", " #ifdef VERBOSE", " printf(\"%%3ld: BCS move to phase 2, _n=%%d %%s\\n\", depth, _n,", " (trpt->bcs & B_FORCED)?\"forced\":\"free\");", " #endif", " From = FROM_P; To = UPTO_P;", " goto c_switch;", " }", "", " if (_n == 0 /* no process could move */", " && II >= BASE /* not the never claim */", " && trpt->sched_limit >= sched_max)", " { _n = 1;", " #ifdef VERBOSE", " printf(\"%%3ld: BCS not a deadlock\\n\", depth);", " #endif", " }", "#endif", "#ifndef NOFAIR", " /* Fairness: undo Rule 2 */", " if (trpt->o_pm&32) /* remains if proc blocked */", " {", "#ifdef VERI", " if (now._cnt[now._a_t&1] == 1)", " now._cnt[now._a_t&1] = 2;", "#endif", " now._cnt[now._a_t&1] += 1;", "#ifdef VERBOSE", " printf(\"%%3ld: proc -- fairness \", depth);", " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",", " now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm &= ~32;", " }", "#ifndef NP", /* 12/97 non-progress cycles cannot be created * by stuttering extension, here or elsewhere */ " if (fairness", " && _n == 0 /* nobody moved */", "#ifdef VERI", " && !(trpt->tau&4) /* in program move */", "#endif", " && !(trpt->tau&8) /* not an atomic one */", "#ifdef OTIM", " && ((trpt->tau&1) || endstate())", "#else", "#ifdef ETIM", " && (trpt->tau&1) /* already tried timeout */", "#endif", "#endif", "#ifndef NOREDUCE", " /* see below */", " && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))", "#endif", " && now._cnt[now._a_t&1] > 0) /* needed more procs */", " { depth++; trpt++;", " trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));", " trpt->bup.oval = now._cnt[now._a_t&1];", " now._cnt[now._a_t&1] = 1;", "#ifdef VERI", " trpt->tau = 4;", "#else", " trpt->tau = 0;", "#endif", " From = FROM_P; To = UPTO_P;", "#if defined(VERBOSE) || defined(CHECK)", " printf(\"%%3ld: fairness default move \", depth);", " printf(\"(all procs block)\\n\");", "#endif", " goto Down;", " }", "#endif", "Q999: /* returns here with _n>0 when done */;", " if (trpt->o_pm&8)", " { now._a_t &= ~2;", " now._cnt[now._a_t&1] = 0;", " trpt->o_pm &= ~8;", "#ifdef VERBOSE", " printf(\"%%3ld: fairness undo Rule 1, _a_t=%%d\\n\",", " depth, now._a_t);", "#endif", " }", " if (trpt->o_pm&16)", " { now._a_t |= 2;", /* restore a-bit */ " now._cnt[now._a_t&1] = 1;", /* NEW: restore cnt */ " trpt->o_pm &= ~16;", "#ifdef VERBOSE", " printf(\"%%3ld: fairness undo Rule 3, _a_t=%%d\\n\",", " depth, now._a_t);", "#endif", " }", "#endif", "#ifndef NOREDUCE", "#ifdef SAFETY", " #ifdef LOOPSTATE", " /* at least one move that was preselected at this */", " /* level, blocked or was a loop control flow point */", " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))", " #else", " /* preselected move - no successors outside stack */", " if ((trpt->tau&32) && !(trpt->tau&64))", " #endif", " { From = FROM_P; To = UPTO_P;", " #ifdef DEBUG", " printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ", " depth, II+1, _n, trpt->tau);", " #endif", " _n = 0; trpt->tau &= ~(16|32|64);", " if (MORE_P) /* II already decremented */", " goto Resume;", " else", " goto Again;", " }", "#else", " /* at least one move that was preselected at this */", " /* level, blocked or truncated at the next level */", " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))", " {", " #ifdef DEBUG", " printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ", " depth, II+1, (int) _n, trpt->tau);", " #endif", " if (a_cycles && (trpt->tau&16))", " { if (!(now._a_t&1))", " {", " #ifdef DEBUG", " printf(\"%%3ld: setting proviso bit\\n\", depth);", " #endif", "#ifndef BITSTATE", "#ifdef MA", "#ifdef VERI", " (trpt-1)->proviso = 1;", "#else", " trpt->proviso = 1;", "#endif", "#else", "#ifdef VERI", " if ((trpt-1)->ostate)", " ((char *)&((trpt-1)->ostate->state))[0] |= 128;", "#else", " ((char *)&(trpt->ostate->state))[0] |= 128;", "#endif", "#endif", "#else", "#ifdef VERI", " if ((trpt-1)->ostate)", " (trpt-1)->ostate->proviso = 1;", "#else", " trpt->ostate->proviso = 1;", "#endif", "#endif", " From = FROM_P; To = UPTO_P;", " _n = 0; trpt->tau &= ~(16|32|64);", " goto Again; /* do full search */", " } /* else accept reduction */", " } else", " { From = FROM_P; To = UPTO_P;", " _n = 0; trpt->tau &= ~(16|32|64);", " if (MORE_P) /* II already decremented */", " goto Resume;", " else", " goto Again;", " } }", "#endif", "#endif", " if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))", " {", "#ifdef DEBUG", " cpu_printf(\"%%3ld: no move [II=%%d, tau=%%d, boq=%%d]\\n\",", " depth, II, trpt->tau, boq);", "#endif", "#if SYNC", " /* ok if a rendez-vous fails: */", " if (boq != -1) goto Done;", "#endif", " /* ok if no procs or we're at maxdepth */", " if ((now._nr_pr == 0 && (!strict || qs_empty()))", "#ifdef OTIM", " || endstate()", "#endif", " || depth >= maxdepth-1) goto Done; /* undo change from 5.2.3 */", " if ((trpt->tau&8) && !(trpt->tau&4))", " { trpt->tau &= ~(1|8);", " /* 1=timeout, 8=atomic */", " From = FROM_P; To = UPTO_P;", "#ifdef DEBUG", " cpu_printf(\"%%3ld: atomic step proc %%d unexecutable\\n\", depth, II+1);", "#endif", "#ifdef VERI", " trpt->tau |= 4; /* switch to claim */", "#endif", " goto AllOver;", " }", "#ifdef ETIM", " if (!(trpt->tau&1)) /* didn't try timeout yet */", " {", "#ifdef VERI", " if (trpt->tau&4)", " {", "#ifndef NTIM", " if (trpt->tau&2) /* requested */", "#endif", " { trpt->tau |= 1;", " trpt->tau &= ~2;", "#ifdef DEBUG", " cpu_printf(\"%%d: timeout\\n\", depth);", "#endif", " goto Stutter;", " } }", " else", " { /* only claim can enable timeout */", " if ((trpt->tau&8)", " && !((trpt-1)->tau&4))", "/* blocks inside an atomic */ goto BreakOut;", "#ifdef DEBUG", " cpu_printf(\"%%d: req timeout\\n\",", " depth);", "#endif", " (trpt-1)->tau |= 2; /* request */", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", "#else", "#ifdef DEBUG", " cpu_printf(\"%%d: timeout\\n\", depth);", "#endif", " trpt->tau |= 1;", " goto Again;", "#endif", " }", "#endif", /* old location of atomic block code */ "#ifdef VERI", "BreakOut:", "#ifndef NOSTUTTER", " if (!(trpt->tau&4))", " { trpt->tau |= 4; /* claim stuttering */", " trpt->tau |= 128; /* stutter mark */", "#ifdef DEBUG", " cpu_printf(\"%%d: claim stutter\\n\", depth);", "#endif", " goto Stutter;", " }", "#else", " ;", "#endif", "#else", " if (!noends && !a_cycles && !endstate())", " { depth--; trpt--; /* new 4.2.3 */", " uerror(\"invalid end state\");", " depth++; trpt++;", " }", "#ifndef NOSTUTTER", " else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */", " { depth--; trpt--;", " uerror(\"accept stutter\");", " depth++; trpt++;", " }", "#endif", "#endif", " }", "Done:", " if (!(trpt->tau&8)) /* not in atomic seqs */", " {", "#ifndef MA", "#if defined(FULLSTACK) || defined(CNTRSTACK)", "#ifdef VERI", " if (boq == -1", " && (((trpt->tau&4) && !(trpt->tau&128))", " || ( (trpt-1)->tau&128)))", "#else", " if (boq == -1)", "#endif", " {", "#ifdef DEBUG2", "#if defined(FULLSTACK)", " printf(\"%%d: zapping %%u (%%d)\\n\",", " depth, trpt->ostate,", " (trpt->ostate)?trpt->ostate->tagged:0);", "#endif", "#endif", " onstack_zap();", " }", "#endif", "#else", "#ifdef VERI", " if (boq == -1", " && (((trpt->tau&4) && !(trpt->tau&128))", " || ( (trpt-1)->tau&128)))", "#else", " if (boq == -1)", "#endif", " {", "#ifdef DEBUG", " printf(\"%%d: zapping\\n\", depth);", "#endif", " onstack_zap();", "#ifndef NOREDUCE", " if (trpt->proviso)", " gstore((char *) &now, vsize, 1);", "#endif", " }", "#endif", "#ifndef SAFETY", " if (_n != 0", /* we made a move */ "#ifdef VERI", " /* --after-- a program-step, i.e., */", " /* after backtracking a claim-step */", " && (trpt->tau&4)", " /* with at least one running process */", " /* unless in a stuttered accept state */", " && ((now._nr_pr > 1) || (trpt->o_pm&2))", "#endif", " && !(now._a_t&1))", /* not in 2nd DFS */ " {", "#ifndef NOFAIR", " if (fairness)", /* implies a_cycles */ " {", "#ifdef VERBOSE", " cpu_printf(\"Consider check %%d %%d...\\n\",", " now._a_t, now._cnt[0]);", "#endif", #if 0 the a-bit is set, which means that the fairness counter is running -- it was started in an accepting state. we check that the counter reached 1, which means that all processes moved least once. this means we can start the search for cycles - to be able to return to this state, we should be able to run down the counter to 1 again -- which implies a visit to the accepting state -- even though the Seed state for this search is itself not necessarily accepting #endif " if ((now._a_t&2) /* A-bit */", " && (now._cnt[0] == 1))", " checkcycles();", " } else", "#endif", " if (a_cycles && (trpt->o_pm&2))", " checkcycles();", " }", "#endif", " }", " if (depth > 0)", " {", "#if NCORE>1 && defined(FULL_TRAIL)", " if (upto > 0)", " { Pop_Stack_Tree();", " }", "#endif", " goto Up;", " }", "}\n", "#else", "void new_state(void) { /* place holder */ }", "#endif", /* BFS */ "", "void", "spin_assert(int a, char *s, int ii, int tt, Trans *t)", "{", " if (!a && !noasserts)", " { char bad[1024];", " strcpy(bad, \"assertion violated \");", " if (strlen(s) > 1000)", " { strncpy(&bad[19], (const char *) s, 1000);", " bad[1019] = '\\0';", " } else", " strcpy(&bad[19], s);", " uerror(bad);", " }", "}", "#ifndef NOBOUNDCHECK", "int", "Boundcheck(int x, int y, int a1, int a2, Trans *a3)", "{", " spin_assert((x >= 0 && x < y), \"- invalid array index\",", " a1, a2, a3);", " return x;", "}", "#endif", "void", "wrap_stats(void)", "{", " if (nShadow>0)", " printf(\"%%9.8g states, stored (%%g visited)\\n\",", " nstates - nShadow, nstates);", " else", " printf(\"%%9.8g states, stored\\n\", nstates);", "#ifdef BFS", "#if SYNC", " printf(\" %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);", " printf(\" %%8g rvs succeeded\\n\", midrv-failedrv);", "#else", " printf(\" %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);", "#endif", "#ifdef DEBUG", " printf(\" %%8g midrv\\n\", midrv);", " printf(\" %%8g failedrv\\n\", failedrv);", " printf(\" %%8g revrv\\n\", revrv);", "#endif", "#endif", " printf(\"%%9.8g states, matched\\n\", truncs);", "#ifdef CHECK", " printf(\"%%9.8g matches within stack\\n\",truncs2);", "#endif", " if (nShadow>0)", " printf(\"%%9.8g transitions (= visited+matched)\\n\",", " nstates+truncs);", " else", " printf(\"%%9.8g transitions (= stored+matched)\\n\",", " nstates+truncs);", " printf(\"%%9.8g atomic steps\\n\", nlinks);", " if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);", "", "#ifndef BITSTATE", " #ifndef MA", " printf(\"hash conflicts: %%9.8g (resolved)\\n\", hcmp);", " #ifndef AUTO_RESIZE", " if (hcmp > (double) (1< 100.)\\n\\n\",", " (double)(((double) udmem) * 8.0) / (double) nstates);", " else", " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",", " (double)(1<<(ssize-8)) / (double) nstates * 256.0);", " printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);", " #if 0", " if (udmem)", " { printf(\"total bits available: %%8g (-M%%ld)\\n\",", " ((double) udmem) * 8.0, udmem/(1024L*1024L));", " } else", " { printf(\"total bits available: %%8g (-w%%d)\\n\",", " ((double) (ONE_L << (ssize-4)) * 16.0), ssize);", " }", " #endif", "#endif", "#ifdef BFS_DISK", " printf(\"bfs disk reads: %%ld writes %%ld -- diff %%ld\\n\",", " bfs_dsk_reads, bfs_dsk_writes, bfs_dsk_writes-bfs_dsk_reads);", " if (bfs_dsk_read >= 0) (void) close(bfs_dsk_read);", " if (bfs_dsk_write >= 0) (void) close(bfs_dsk_write);", " (void) unlink(\"pan_bfs_dsk.tmp\");", "#endif", "}", "", "void", "wrapup(void)", "{ double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;", "#if !defined(MA) && (defined(MEMCNT) || defined(MEMLIM))", " int mverbose = 1;", "#else", " int mverbose = verbose;", "#endif", "#if NCORE>1", " if (verbose) cpu_printf(\"wrapup -- %%d error(s)\\n\", errors);", " if (core_id != 0)", " {", "#ifdef USE_DISK", " void dsk_stats(void);", " dsk_stats();", "#endif", " if (search_terminated != NULL)", " { *search_terminated |= 2; /* wrapup */", " }", " exit(0); /* normal termination, not an error */", " }", "#endif", "#if !defined(WIN32) && !defined(WIN64)", " signal(SIGINT, SIG_DFL);", "#endif", " printf(\"\\n(%%s)\\n\", SpinVersion);", " if (!done) printf(\"Warning: Search not completed\\n\");", "#ifdef SC", " (void) unlink((const char *)stackfile);", "#endif", "#if NCORE>1", " if (a_cycles)", " { printf(\" + Multi-Core (NCORE=%%d)\\n\", NCORE);", " } else", " { printf(\" + Multi-Core (NCORE=%%d -z%%ld)\\n\", NCORE, z_handoff);", " }", "#endif", "#ifdef BFS", " printf(\" + Using Breadth-First Search\\n\");", "#endif", "#ifndef NOREDUCE", " printf(\" + Partial Order Reduction\\n\");", "#endif", "#ifdef REVERSE", " printf(\" + Reverse Depth-First Search Order\\n\");", "#endif", "#ifdef T_REVERSE", " printf(\" + Reverse Transition Ordering\\n\");", "#endif", "#ifdef T_RAND", " printf(\" + Randomized Transition Ordering\\n\");", "#endif", "#ifdef P_RAND", " printf(\" + Randomized Process Ordering\\n\");", "#endif", "#ifdef BCS", " printf(\" + Scheduling Restriction (-L%%d)\\n\", sched_max);", "#endif", "#ifdef TRIX", " printf(\" + Tree Index Compression\\n\");", "#endif", "#ifdef COLLAPSE", " printf(\" + Compression\\n\");", "#endif", "#ifdef MA", " printf(\" + Graph Encoding (-DMA=%%d)\\n\", MA);", " #ifdef R_XPT", " printf(\" Restarted from checkpoint %%s.xpt\\n\", PanSource);", " #endif", "#endif", "#ifdef CHECK", " #ifdef FULLSTACK", " printf(\" + FullStack Matching\\n\");", " #endif", " #ifdef CNTRSTACK", " printf(\" + CntrStack Matching\\n\");", " #endif", "#endif", "#ifdef BITSTATE", " printf(\"\\nBit statespace search for:\\n\");", "#else", " #ifdef HC", " printf(\"\\nHash-Compact %%d search for:\\n\", HC);", " #else", " printf(\"\\nFull statespace search for:\\n\");", " #endif", "#endif", "#ifdef EVENT_TRACE", "#ifdef NEGATED_TRACE", " printf(\"\tnotrace assertion \t+\\n\");", "#else", " printf(\"\ttrace assertion \t+\\n\");", "#endif", "#endif", "#ifdef VERI", " printf(\"\tnever claim \t+\");", " printf(\" (%%s)\\n\", procname[((Pclaim *)pptr(0))->_t]);", " printf(\"\tassertion violations\t\");", " if (noasserts)", " printf(\"- (disabled by -A flag)\\n\");", " else", " printf(\"+ (if within scope of claim)\\n\");", "#else", "#ifdef NOCLAIM", " printf(\"\tnever claim \t- (not selected)\\n\");", "#else", " printf(\"\tnever claim \t- (none specified)\\n\");", "#endif", " printf(\"\tassertion violations\t\");", " if (noasserts)", " printf(\"- (disabled by -A flag)\\n\");", " else", " printf(\"+\\n\");", "#endif", "#ifndef SAFETY", "#ifdef NP", " printf(\"\tnon-progress cycles \t\");", "#else", " printf(\"\tacceptance cycles \t\");", "#endif", " if (a_cycles)", " printf(\"+ (fairness %%sabled)\\n\",", " fairness?\"en\":\"dis\");", " else printf(\"- (not selected)\\n\");", "#else", " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");", "#endif", "#ifdef VERI", " printf(\"\tinvalid end states\t- \");", " printf(\"(disabled by \");", " if (noends)", " printf(\"-E flag)\\n\\n\");", " else", " printf(\"never claim)\\n\\n\");", "#else", " printf(\"\tinvalid end states\t\");", " if (noends)", " printf(\"- (disabled by -E flag)\\n\\n\");", " else", " printf(\"+\\n\\n\");", "#endif", " printf(\"State-vector %%d byte, depth reached %%ld\", hmax,", "#if NCORE>1", " (nr_handoffs * z_handoff) +", "#endif", " mreached);", " printf(\", errors: %%d\\n\", errors);", " fflush(stdout);", "#ifdef MA", " if (done)", " { extern void dfa_stats(void);", " if (maxgs+a_cycles+2 < MA)", " printf(\"MA stats: -DMA=%%d is sufficient\\n\",", " maxgs+a_cycles+2);", " dfa_stats();", " }", "#endif", " wrap_stats();", "#ifdef CHECK", " printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);", " printf(\"stats: fa %%ld, fh %%ld, zh %%ld, zn %%ld - \",", " Fa, Fh, Zh, Zn);", " printf(\"check %%ld holds %%ld\\n\", Ccheck, Cholds);", " printf(\"stack stats: puts %%ld, probes %%ld, zaps %%ld\\n\",", " PUT, PROBE, ZAPS);", "#else", " printf(\"\\n\");", "#endif", "", "#if !defined(BITSTATE) && defined(NOCOMP)", " if (!verbose) { goto jump_here; }", /* added 5.2.0 */ "#endif", "", "#if 1", /* omitted 5.2.0: defined(BITSTATE) || !defined(NOCOMP) */ " nr1 = (nstates-nShadow)*", " (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));", " #ifdef BFS", " nr2 = 0.0;", " #else", " nr2 = (double) ((maxdepth+3)*sizeof(Trail));", " #endif", " #ifndef BITSTATE", "#if !defined(MA) || defined(COLLAPSE)", " nr3 = (double) (ONE_L<1 && !defined(SEP_STATE)", " tmp_nr -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;", " #endif", " if (tmp_nr < 0.0) tmp_nr = 0.;", " printf(\"Stats on memory usage (in Megabytes):\\n\");", " printf(\"%%9.3f\tequivalent memory usage for states\",", " nr1/1048576.); /* 1024*1024=1048576 */", " printf(\" (stored*(State-vector + overhead))\\n\");", " #if NCORE>1 && !defined(WIN32) && !defined(WIN64)", " printf(\"%%9.3f\tshared memory reserved for state storage\\n\",", " mem_reserved/1048576.);", " #ifdef SEP_HEAP", " printf(\"\t\tin %%d local heaps of %%7.3f MB each\\n\",", " NCORE, mem_reserved/(NCORE*1048576.));", " #endif", " printf(\"\\n\");", " #endif", "#ifdef BITSTATE", " if (udmem)", " printf(\"%%9.3f\tmemory used for hash array (-M%%ld)\\n\",", " nr3/1048576., udmem/(1024L*1024L));", " else", " printf(\"%%9.3f\tmemory used for hash array (-w%%d)\\n\",", " nr3/1048576., ssize);", " if (nr5 > 0.0)", " printf(\"%%9.3f\tmemory used for bit stack\\n\",", " nr5/1048576.);", " remainder = remainder - nr3 - nr5;", "#else", " printf(\"%%9.3f\tactual memory usage for states\",", " tmp_nr/1048576.);", " remainder -= tmp_nr;", " printf(\" (\");", " if (tmp_nr > 0.)", " { if (tmp_nr > nr1) printf(\"unsuccessful \");", " printf(\"compression: %%.2f%%%%)\\n\",", " (100.0*tmp_nr)/nr1);", " } else", " printf(\"less than 1k)\\n\");", "#ifndef MA", " if (tmp_nr > 0.)", " { printf(\" \tstate-vector as stored = %%.0f byte\",", " (tmp_nr)/(nstates-nShadow) -", " (double) (sizeof(struct H_el) - sizeof(unsigned)));", " printf(\" + %%ld byte overhead\\n\",", " (long int) sizeof(struct H_el)-sizeof(unsigned));", " }", "#endif", "#if !defined(MA) || defined(COLLAPSE)", " printf(\"%%9.3f\tmemory used for hash table (-w%%d)\\n\",", " nr3/1048576., ssize);", " remainder -= nr3;", "#endif", "#endif", " #ifndef BFS", " printf(\"%%9.3f\tmemory used for DFS stack (-m%%ld)\\n\",", " nr2/1048576., maxdepth);", " remainder -= nr2;", " #endif", "#if NCORE>1", " remainder -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;", " printf(\"%%9.3f\tshared memory used for work-queues\\n\",", " (GWQ_SIZE + (double) NCORE * LWQ_SIZE) /1048576.);", " printf(\"\t\tin %%d queues of %%7.3f MB each\",", " NCORE, (double) LWQ_SIZE /1048576.);", " #ifndef NGQ", " printf(\" + a global q of %%7.3f MB\\n\",", " (double) GWQ_SIZE / 1048576.);", " #else", " printf(\"\\n\");", " #endif", " #endif", " if (remainder - fragment > 1048576.)", " printf(\"%%9.3f\tother (proc and chan stacks)\\n\",", " (remainder-fragment)/1048576.);", " if (fragment > 1048576.)", " printf(\"%%9.3f\tmemory lost to fragmentation\\n\",", " fragment/1048576.);", " printf(\"%%9.3f\ttotal actual memory usage\\n\\n\",", " memcnt/1048576.);", " }", " #ifndef MA", " else", " #endif", "#endif", "#if !defined(BITSTATE) && defined(NOCOMP)", "jump_here:", "#endif", "#ifndef MA", " printf(\"%%9.3f\tmemory usage (Mbyte)\\n\\n\",", " memcnt/1048576.);", "#endif", "#ifdef COLLAPSE", " printf(\"nr of templates: [ globals chans procs ]\\n\");", " printf(\"collapse counts: [ \");", " { int i; for (i = 0; i < 256+2; i++)", " if (ncomps[i] != 0)", " printf(\"%%d \", (int) ncomps[i]);", " printf(\"]\\n\");", " }", "#endif", " #ifdef TRIX", " if (mverbose)", " { int i;", " printf(\"TRIX counts:\\n\");", " printf(\" processes: \");", " for (i = 0; i < MAXPROC; i++)", " if (_p_count[i] != 0)", " { printf(\"%%3d:%%ld \",", " i, _p_count[i]);", " }", " printf(\"\\n channels : \");", " for (i = 0; i < MAXQ; i++)", " if (_c_count[i] != 0)", " { printf(\"%%3d:%%ld \",", " i, _c_count[i]);", " }", " printf(\"\\n\\n\");", " }", " #endif", " if ((done || verbose) && !no_rck) do_reach();", "#ifdef PEG", " { int i;", " printf(\"\\nPeg Counts (transitions executed):\\n\");", " for (i = 1; i < NTRANS; i++)", " { if (peg[i]) putpeg(i, peg[i]);", " } }", "#endif", "#ifdef VAR_RANGES", " dumpranges();", "#endif", "#ifdef SVDUMP", " if (vprefix > 0) close(svfd);", "#endif", "#ifdef LOOPSTATE", " printf(\"%%g loopstates hit\\n\", cnt_loops);", "#endif", "#ifdef NSUCC", " dump_succ();", "#endif", "#if NCORE>1 && defined(T_ALERT)", " crash_report();", "#endif", " pan_exit(0);", "}\n", "void", "stopped(int arg)", "{ printf(\"Interrupted\\n\");", "#if NCORE>1", " was_interrupted = 1;", "#endif", " wrapup();", " pan_exit(0);", "}", "", "#ifdef SFH", "/*", " * super fast hash, based on Paul Hsieh's function", " * http://www.azillionmonkeys.com/qed/hash.html", " */", "#include ", /* for uint32_t etc */ " #undef get16bits", " #if (defined(__GNUC__) && defined(__i386__)) || defined(__WATCOMC__) \\", " || defined(_MSC_VER) || defined (__BORLANDC__) || defined (__TURBOC__)", " #define get16bits(d) (*((const uint16_t *) (d)))", " #endif", "", " #ifndef get16bits", " #define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\", " +(uint32_t)(((const uint8_t *)(d))[0]) )", " #endif", "", "void", "d_sfh(const char *s, int len)", "{ uint32_t h = len, tmp;", " int rem;", "", " rem = len & 3;", " len >>= 2;", "", " for ( ; len > 0; len--)", " { h += get16bits(s);", " tmp = (get16bits(s+2) << 11) ^ h;", " h = (h << 16) ^ tmp;", " s += 2*sizeof(uint16_t);", " h += h >> 11;", " }", " switch (rem) {", " case 3: h += get16bits(s);", " h ^= h << 16;", " h ^= s[sizeof(uint16_t)] << 18;", " h += h >> 11;", " break;", " case 2: h += get16bits(s);", " h ^= h << 11;", " h += h >> 17;", " break;", " case 1: h += *s;", " h ^= h << 10;", " h += h >> 1;", " break;", " }", " h ^= h << 3;", " h += h >> 5;", " h ^= h << 4;", " h += h >> 17;", " h ^= h << 25;", " h += h >> 6;", "", " K1 = h;", "}", "#endif", /* SFH */ "", "#include ", /* uint32_t etc. */ "#if defined(HASH64) || defined(WIN64)", "/* 64-bit Jenkins hash, 1997", " * http://burtleburtle.net/bob/c/lookup8.c", " */", "#define mix(a,b,c) \\", "{ a -= b; a -= c; a ^= (c>>43); \\", " b -= c; b -= a; b ^= (a<<9); \\", " c -= a; c -= b; c ^= (b>>8); \\", " a -= b; a -= c; a ^= (c>>38); \\", " b -= c; b -= a; b ^= (a<<23); \\", " c -= a; c -= b; c ^= (b>>5); \\", " a -= b; a -= c; a ^= (c>>35); \\", " b -= c; b -= a; b ^= (a<<49); \\", " c -= a; c -= b; c ^= (b>>11); \\", " a -= b; a -= c; a ^= (c>>12); \\", " b -= c; b -= a; b ^= (a<<18); \\", " c -= a; c -= b; c ^= (b>>22); \\", "}", "#else", "/* 32-bit Jenkins hash, 2006", " * http://burtleburtle.net/bob/c/lookup3.c", " */", "#define rot(x,k) (((x)<<(k))|((x)>>(32-(k))))", "", "#define mix(a,b,c) \\", "{ a -= c; a ^= rot(c, 4); c += b; \\", " b -= a; b ^= rot(a, 6); a += c; \\", " c -= b; c ^= rot(b, 8); b += a; \\", " a -= c; a ^= rot(c,16); c += b; \\", " b -= a; b ^= rot(a,19); a += c; \\", " c -= b; c ^= rot(b, 4); b += a; \\", "}", "", "#define final(a,b,c) \\", "{ c ^= b; c -= rot(b,14); \\", " a ^= c; a -= rot(c,11); \\", " b ^= a; b -= rot(a,25); \\", " c ^= b; c -= rot(b,16); \\", " a ^= c; a -= rot(c,4); \\", " b ^= a; b -= rot(a,14); \\", " c ^= b; c -= rot(b,24); \\", "}", "#endif", "", "void", "d_hash(uchar *kb, int nbytes)", "{ uint8_t *bp;", "#if defined(HASH64) || defined(WIN64)", " uint64_t a = 0, b, c, n;", " uint64_t *k = (uint64_t *) kb;", "#else", " uint32_t a = 0, b, c, n;", " uint32_t *k = (uint32_t *) kb;", "#endif", " n = nbytes/WS; /* nr of words */", " /* extend to multiple of words, if needed */", " a = WS - (nbytes %% WS);", " if (a > 0 && a < WS)", " { n++;", " bp = kb + nbytes;", " switch (a) {", "#if defined(HASH64) || defined(WIN64)", " case 7: *bp++ = 0; /* fall thru */", " case 6: *bp++ = 0; /* fall thru */", " case 5: *bp++ = 0; /* fall thru */", " case 4: *bp++ = 0; /* fall thru */", "#endif", " case 3: *bp++ = 0; /* fall thru */", " case 2: *bp++ = 0; /* fall thru */", " case 1: *bp = 0;", " case 0: break;", " } }", "#if defined(HASH64) || defined(WIN64)", " b = HASH_CONST[HASH_NR];", " c = 0x9e3779b97f4a7c13LL; /* arbitrary value */", " while (n >= 3)", " { a += k[0];", " b += k[1];", " c += k[2];", " mix(a,b,c);", " n -= 3;", " k += 3;", " }", " c += (((uint64_t) nbytes)<<3);", " switch (n) {", " case 2: b += k[1];", " case 1: a += k[0];", " case 0: break;", " }", " mix(a,b,c);", "#else", /* 32 bit version: */ " a = c = 0xdeadbeef + (n<<2);", " b = HASH_CONST[HASH_NR];", " while (n > 3)", " { a += k[0];", " b += k[1];", " c += k[2];", " mix(a,b,c);", " n -= 3;", " k += 3;", " }", " switch (n) { ", " case 3: c += k[2];", " case 2: b += k[1];", " case 1: a += k[0];", " final(a,b,c);", " case 0: break;", " }", "#endif", " j1_spin = c&nmask; j3 = a&7; /* 1st bit */", " j2 = b&nmask; j4 = (a>>3)&7; /* 2nd bit */", " K1 = c; K2 = b;", "}", "", "void", "s_hash(uchar *cp, int om)", "{", "#if defined(SFH)", " d_sfh((const char *) cp, om); /* sets K1 */", "#else", " d_hash(cp, om); /* sets K1 etc */", "#endif", "#ifdef BITSTATE", " if (S_Tab == H_tab)", /* state stack in bitstate search */ " j1_spin = K1 %% omaxdepth;", " else", "#endif", /* if (S_Tab != H_Tab) */ " if (ssize < 8*WS)", " j1_spin = K1&mask;", " else", " j1_spin = K1;", "}", "#ifndef RANDSTOR", "int *prerand;", "void", "inirand(void)", "{ int i;", " srand(123); /* fixed startpoint */", " prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));", " for (i = 0; i < omaxdepth+3; i++)", " prerand[i] = rand();", "}", "int", "pan_rand(void)", "{ if (!prerand) inirand();", " return prerand[depth];", "}", "#endif", "", "void", "set_masks(void) /* 4.2.5 */", "{", " if (WS == 4 && ssize >= 32)", " { mask = 0xffffffff;", "#ifdef BITSTATE", " switch (ssize) {", " case 34: nmask = (mask>>1); break;", " case 33: nmask = (mask>>2); break;", " default: nmask = (mask>>3); break;", " }", "#else", " nmask = mask;", "#endif", " } else if (WS == 8)", " { mask = ((ONE_L<>3;", "#else", " nmask = mask;", "#endif", " } else if (WS != 4)", " { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", (long int) WS);", " exit(1);", " } else /* WS == 4 and ssize < 32 */", " { mask = ((ONE_L<>3);", " }", "}", "", "static long reclaim_size;", "static char *reclaim_mem;", "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)", "#if NCORE>1", " #error cannot combine AUTO_RESIZE with NCORE>1 yet", "#endif", "static struct H_el **N_tab;", "void", "reverse_capture(struct H_el *p)", "{ if (!p) return;", " reverse_capture(p->nxt);", " /* last element of list moves first */", " /* to preserve list-order */", " j2 = p->m_K1;", " if (ssize < 8*WS) /* probably always true */", " { j2 &= mask;", " }", " p->nxt = N_tab[j2];", " N_tab[j2] = p;", "}", "void", "resize_hashtable(void)", "{", " if (WS == 4 && ssize >= 27 - 1)", " { return; /* cannot increase further */", " }", "", " ssize += 2; /* 4x size @htable ssize */", "", " printf(\"pan: resizing hashtable to -w%%d.. \", ssize);", "", " N_tab = (struct H_el **)", " emalloc((ONE_L<1", "int", "find_claim(char *s)", "{ int i, j;", " for (i = 0; procname[i] != \":np_:\"; i++)", " { if (strcmp(s, procname[i]) == 0)", " { for (j = 0; j < NCLAIMS; j++)", " { if (spin_c_typ[j] == i)", " { return j;", " } }", " break;", " } }", " printf(\"pan: error: cannot find claim '%%s'\\n\", s);", " exit(1);", " return -1; /* unreachable */", "}", "#endif", "", "int", "main(int argc, char *argv[])", "{ void to_compile(void);\n", " efd = stderr; /* default */", "", " if (G_long != sizeof(long)", " || G_int != sizeof(int))", " { printf(\"spin: error, the version of spin \");", " printf(\"that generated this pan.c assumed a different \");", " printf(\"wordsize (%%d iso %%d)\\n\", G_long, (int) sizeof(long));", " exit(1);", " }", "", "#if defined(T_RAND) && (T_RAND>0)", " s_rand = T_RAND;", /* so that -RS can override */ "#elif defined(P_RAND) && (P_RAND>0)", " s_rand = P_RAND;", "#endif", /* else, could use time as seed... */ "", "#ifdef PUTPID", " { char *ptr = strrchr(argv[0], '/');", " if (ptr == NULL)", " { ptr = argv[0];", " } else", " { ptr++;", " }", " progname = emalloc(strlen(ptr));", " strcpy(progname, ptr);", " /* printf(\"progname: %%s\\n\", progname); */", " }", "#endif", "", "#ifdef BITSTATE", " bstore = bstore_reg; /* default */", "#endif", "#if NCORE>1", " { int i, j;", " strcpy(o_cmdline, \"\");", " for (j = 1; j < argc; j++)", " { strcat(o_cmdline, argv[j]);", " strcat(o_cmdline, \" \");", " }", " /* printf(\"Command Line: %%s\\n\", o_cmdline); */", " if (strlen(o_cmdline) >= sizeof(o_cmdline))", " { Uerror(\"option list too long\");", " } }", "#endif", " while (argc > 1 && argv[1][0] == '-')", " { switch (argv[1][1]) {", "#ifndef SAFETY", "#ifdef NP", " case 'a': fprintf(efd, \"error: -a disabled\");", " usage(efd); break;", "#else", " case 'a': a_cycles = 1; break;", "#endif", "#endif", " case 'A': noasserts = 1; break;", " case 'b': bounded = 1; break;", "#ifdef HAS_CODE", " case 'C': coltrace = 1; goto samething;", "#endif", " case 'c': upto = atoi(&argv[1][2]); break;", " case 'D': dodot++; state_tables++; break;", " case 'd': state_tables++; break;", " case 'e': every_error = 1; upto = 0; Nr_Trails = 1; break;", " case 'E': noends = 1; break;", "#ifdef SC", " case 'F': if (strlen(argv[1]) > 2)", " stackfile = &argv[1][2];", " break;", "#endif", "#if !defined(SAFETY) && !defined(NOFAIR)", " case 'f': fairness = 1; break;", "#endif", "#ifdef HAS_CODE", " case 'g': gui = 1; goto samething;", "#endif", " case 'h': if (!argv[1][2]) usage(efd); else", " HASH_NR = atoi(&argv[1][2])%%100; break;", " case 'I': iterative = 2; every_error = 1; break;", " case 'i': iterative = 1; every_error = 1; break;", " case 'J': like_java = 1; break; /* Klaus Havelund */", "#ifdef BITSTATE", " case 'k': hfns = atoi(&argv[1][2]); break;", "#endif", "#ifdef BCS", " case 'L':", " sched_max = atoi(&argv[1][2]);", " if (sched_max > 255) /* stored as one byte */", " { fprintf(efd, \"warning: using max bound (255)\\n\");", " sched_max = 255;", " }", " #ifndef NOREDUCE", " if (sched_max == 0)", " { fprintf(efd, \"warning: with (default) bound -L0, \");", " fprintf(efd, \"using -DNOREDUCE performs better\\n\");", " }", " #endif", " break;", "#endif", "#ifndef SAFETY", "#ifdef NP", " case 'l': a_cycles = 1; break;", "#else", " case 'l': fprintf(efd, \"error: -l disabled\");", " usage(efd); break;", "#endif", "#endif", "#ifdef BITSTATE", " case 'M': udmem = atoi(&argv[1][2]); break;", " case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;", "#else", " case 'M': case 'G':", " fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");", " break;", "#endif", " case 'm': maxdepth = atoi(&argv[1][2]); break;", "#ifndef NOCLAIM", " case 'N':", "#if NCLAIMS>1", " if (isdigit(argv[1][2]))", " whichclaim = atoi(&argv[1][2]);", " else if (isalpha(argv[1][2]))", " { claimname = &argv[1][2];", " } else if (argc > 2 && argv[2][0] != '-') /* check next arg */", " { claimname = argv[2];", " argc--; argv++; /* skip next arg */", " }", "#else", " #if NCLAIMS==1", " fprintf(stderr, \"warning: only one claim defined, -N ignored\\n\");", " #else", " fprintf(stderr, \"warning: no claims defined, -N ignored\\n\");", " #endif", " if (!isdigit(argv[1][2]) && argc > 2 && argv[2][0] != '-')", " { argc--; argv++;", " }", "#endif", "#endif", " break;\n", " case 'n': no_rck = 1; break;", " case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]);", " if (argv[2][0] != '-') /* check next arg */", " { trailfilename = argv[2];", " argc--; argv++; /* skip next arg */", " }", " break;", "#ifdef SVDUMP", " case 'p': vprefix = atoi(&argv[1][2]); break;", "#endif", "#if NCORE==1", " case 'Q': quota = (double) 60.0 * (double) atoi(&argv[1][2]);", " #ifndef FREQ", " freq /= 10.; /* for better resolution */", " #endif", " break;", "#endif", " case 'q': strict = 1; break;", " case 'R':", "#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)", " if (argv[1][2] == 'S') /* e.g., -RS76842 */", " { s_rand = atoi(&argv[1][3]);", " } else", "#endif", " { Nrun = atoi(&argv[1][2]);", " }", " break;", "#ifdef HAS_CODE", " case 'r':", "samething: readtrail = 1;", " if (isdigit(argv[1][2]))", " whichtrail = atoi(&argv[1][2]);", " else if (argc > 2 && argv[2][0] != '-') /* check next arg */", " { trailfilename = argv[2];", " argc--; argv++; /* skip next arg */", " }", " break;", " case 'S': silent = 1; goto samething;", "#endif", "#ifdef BITSTATE", " case 's': hfns = 1; break;", "#endif", " case 'T': TMODE = 0444; break;", " case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;", " case 'V': start_timer(); printf(\"Generated by %%s\\n\", SpinVersion);", " to_compile(); pan_exit(2); break;", " case 'v': verbose++; break;", " case 'w': ssize = atoi(&argv[1][2]); break;", " case 'Y': signoff = 1; break;", " case 'X': efd = stdout; break;", " case 'x': exclusive = 1; break;", "#if NCORE>1", " /* -B ip is passthru to proxy of remote ip address: */", " case 'B': argc--; argv++; break;", " case 'Q': worker_pids[0] = atoi(&argv[1][2]); break;", " /* -Un means that the nth worker should be instantiated as a proxy */", " case 'U': proxy_pid = atoi(&argv[1][2]); break;", " /* -W means that this copy is started by a cluster-server as a remote */", " /* this flag is passed to ./pan_proxy, which interprets it */", " case 'W': remote_party++; break;", " case 'Z': core_id = atoi(&argv[1][2]);", " if (verbose)", " { printf(\"cpu%%d: pid %%d parent %%d\\n\",", " core_id, getpid(), worker_pids[0]);", " }", " break;", " case 'z': z_handoff = atoi(&argv[1][2]); break;", "#else", " case 'z': break; /* ignored for single-core */", "#endif", " default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;", " }", " argc--; argv++;", " }", " if (iterative && TMODE != 0666)", " { TMODE = 0666;", " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");", " }", "#if defined(HASH32) && !defined(SFH)", " if (WS > 4)", " { fprintf(efd, \"strong warning: compiling -DHASH32 on a 64-bit machine\\n\");", " fprintf(efd, \" without -DSFH can slow down performance a lot\\n\");", " }", "#endif", "#if defined(WIN32) || defined(WIN64)", " if (TMODE == 0666)", " TMODE = _S_IWRITE | _S_IREAD;", " else", " TMODE = _S_IREAD;", "#endif", "#if NCORE>1", " store_proxy_pid = proxy_pid; /* for checks in mem_file() and someone_crashed() */", " if (core_id != 0) { proxy_pid = 0; }", " #ifndef SEP_STATE", " if (core_id == 0 && a_cycles)", " { fprintf(efd, \"hint: this search may be more efficient \");", " fprintf(efd, \"if pan.c is compiled -DSEP_STATE\\n\");", " }", " #endif", " if (z_handoff < 0)", " { z_handoff = 20; /* conservative default - for non-liveness checks */", " }", "#if defined(NGQ) || defined(LWQ_FIXED)", " LWQ_SIZE = (double) (128.*1048576.);", "#else", " LWQ_SIZE = (double) ( z_handoff + 2.) * (double) sizeof(SM_frame);", /* the added margin of +2 is not really necessary */ "#endif", " #if NCORE>2", " if (a_cycles)", " { fprintf(efd, \"warning: the intended nr of cores to be used in liveness mode is 2\\n\");", " #ifndef SEP_STATE", " fprintf(efd, \"warning: without -DSEP_STATE there is no guarantee that all liveness violations are found\\n\");", " #endif", " }", /* it still works though, the later cores get states from the global q */ " #endif", " #ifdef HAS_HIDDEN", " #error cannot use hidden variables when compiling multi-core", " #endif", "#endif", "#ifdef BITSTATE", " if (hfns <= 0)", " { hfns = 1;", " fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);", " }", "#endif", " omaxdepth = maxdepth;", "#ifdef BITSTATE", " if (WS == 4 && ssize > 34)", /* 32-bit word size */ " { ssize = 34;", " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);", "/*", " * -w35 would not work: 35-3 = 32 but 1^31 is the largest", " * power of 2 that can be represented in an unsigned long", " */", " }", "#else", " if (WS == 4 && ssize > 27)", " { ssize = 27;", " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);", "/*", " * for emalloc, the lookup table size multiplies by 4 for the pointers", " * the largest power of 2 that can be represented in a ulong is 1^31", " * hence the largest number of lookup table slots is 31-4 = 27", " */", " }", "#endif", "#ifdef SC", " hiwater = HHH = maxdepth-10;", " DDD = HHH/2;", " if (!stackfile)", " { stackfile = (char *) emalloc(strlen(PanSource)+4+1);", " sprintf(stackfile, \"%%s._s_\", PanSource);", " }", " if (iterative)", " { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");", " pan_exit(1);", " }", "#endif", "#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)", " #warning -DR_XPT and -DW_XPT assume -DMA (ignored)", "#endif", " if (iterative && a_cycles)", " fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");", "#ifdef BFS", " #ifdef SC", " #error -DBFS not compatible with -DSC", " #endif", " #ifdef HAS_LAST", " #error -DBFS not compatible with _last", " #endif", " #ifdef HAS_STACK", " #error cannot use c_track UnMatched with BFS", " #endif", " #ifdef BCS", " #error -DBFS not compatible with -DBCS", " #endif", " #ifdef REACH", " #warning -DREACH is redundant when -DBFS is used", " #endif", "#endif", "#ifdef TRIX", " #ifdef BITSTATE", " #error cannot combine -DTRIX and -DBITSTATE", " #endif", " #ifdef COLLAPSE", " #error cannot combine -DTRIX and -DCOLLAPSE", " #endif", " #ifdef MA", " #error cannot combine -DTRIX and -DMA", " #endif", "#endif", "#ifdef BCS", " #ifdef P_RAND", " #error cannot combine -DBCS and -DP_RAND", " #endif", " #ifdef BFS", " #error cannot combine -DBCS and -DBFS", " #endif", "#endif", "#if defined(MERGED) && defined(PEG)", " #error to use -DPEG use: spin -o3 -a", "#endif", "#ifdef HC", " #ifdef SFH", /* cannot happen -- undef-ed in this case */ " #error cannot combine -DHC and -DSFH", " /* use of NOCOMP is the real reason */", " #else", " #ifdef NOCOMP", " #error cannot combine -DHC and -DNOCOMP", " #endif", " #endif", " #ifdef BITSTATE", " #error cannot combine -DHC and -DBITSTATE", " #endif", "#endif", "#if defined(SAFETY) && defined(NP)", " #error cannot combine -DNP and -DBFS or -DSAFETY", "#endif", "#ifdef MA", " #ifdef BITSTATE", " #error cannot combine -DMA and -DBITSTATE", " #endif", " #if MA <= 0", " #error usage: -DMA=N with N > 0 and N < VECTORSZ", " #endif", "#endif", "#ifdef COLLAPSE", " #ifdef BITSTATE", " #error cannot combine -DBITSTATE and -DCOLLAPSE", " #endif", " #ifdef SFH", " #error cannot combine -DCOLLAPSE and -DSFH", " /* use of NOCOMP is the real reason */", " #else", " #ifdef NOCOMP", " #error cannot combine -DCOLLAPSE and -DNOCOMP", " #endif", " #endif", "#endif", " if (maxdepth <= 0 || ssize <= 1) usage(efd);", "#if SYNC>0 && !defined(NOREDUCE)", " if (a_cycles && fairness)", " { fprintf(efd, \"error: p.o. reduction not compatible with \");", " fprintf(efd, \"fairness (-f) in models\\n\");", " fprintf(efd, \" with rendezvous operations: \");", " fprintf(efd, \"recompile with -DNOREDUCE\\n\");", " pan_exit(1);", " }", "#endif", "#if defined(REM_VARS) && !defined(NOREDUCE)", " #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)", "#endif", "#if defined(NOCOMP) && !defined(BITSTATE)", " if (a_cycles)", " { fprintf(efd, \"error: use of -DNOCOMP voids -l and -a\\n\");", " pan_exit(1);", " }", "#endif", "#ifdef MEMLIM", " memlim = ((double) MEMLIM) * (double) (1<<20); /* size in Mbyte */", "#endif", "#ifndef BITSTATE", " if (Nrun > 1) HASH_NR = Nrun - 1;", "#endif", " if (Nrun < 1 || Nrun > 32)", " { fprintf(efd, \"error: invalid arg for -R\\n\");", " usage(efd);", " }", "#ifndef SAFETY", " if (fairness && !a_cycles)", " { fprintf(efd, \"error: -f requires -a or -l\\n\");", " usage(efd);", " }", " #if ACCEPT_LAB==0", " if (a_cycles)", " { fprintf(efd, \"error: no accept labels defined \");", " fprintf(efd, \"in model (for option -a)\\n\");", " usage(efd);", " }", " #endif", "#endif", "#ifndef NOREDUCE", " #ifdef HAS_ENABLED", " #error use of enabled() requires -DNOREDUCE", " #endif", " #ifdef HAS_PCVALUE", " #error use of pcvalue() requires -DNOREDUCE", " #endif", " #ifdef HAS_BADELSE", " #error use of 'else' combined with i/o stmnts requires -DNOREDUCE", " #endif", " #if defined(HAS_LAST) && !defined(BCS)", " #error use of _last requires -DNOREDUCE", " #endif", "#endif", "#if SYNC>0 && !defined(NOREDUCE)", " #ifdef HAS_UNLESS", " fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");", " fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");", " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");", " #ifdef BFS", " fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");", " #endif", " #endif", "#endif", "#if SYNC>0 && defined(BFS)", " #warning use of rendezvous with BFS does not preserve all invalid endstates", "#endif", "#if !defined(REACH) && !defined(BITSTATE)", " if (iterative != 0 && a_cycles == 0)", " { fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");", " }", "#endif", "#if defined(BITSTATE) && defined(REACH)", " #warning -DREACH is voided by -DBITSTATE", "#endif", "#if defined(MA) && defined(REACH)", " #warning -DREACH is voided by -DMA", "#endif", "#if defined(FULLSTACK) && defined(CNTRSTACK)", " #error cannot combine -DFULLSTACK and -DCNTRSTACK", "#endif", "#if defined(VERI)", " #if ACCEPT_LAB>0", " #ifndef BFS", " if (!a_cycles", " #ifdef HAS_CODE", " && !readtrail", " #endif", " #if NCORE>1", " && core_id == 0", " #endif", " && !state_tables)", " { fprintf(efd, \"warning: never claim + accept labels \");", " fprintf(efd, \"requires -a flag to fully verify\\n\");", " }", " #else", " if (!state_tables", " #ifdef HAS_CODE", " && !readtrail", " #endif", " )", " { fprintf(efd, \"warning: verification in BFS mode \");", " fprintf(efd, \"is restricted to safety properties\\n\");", " }", " #endif", " #endif", "#endif", "#ifndef SAFETY", " if (!a_cycles", " #ifdef HAS_CODE", " && !readtrail", " #endif", " #if NCORE>1", " && core_id == 0", " #endif", " && !state_tables)", " { fprintf(efd, \"hint: this search is more efficient \");", " fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");", " }", " #ifndef NOCOMP", " if (!a_cycles)", " { S_A = 0;", " } else", " { if (!fairness)", " { S_A = 1; /* _a_t */", " #ifndef NOFAIR", " } else /* _a_t and _cnt[NFAIR] */", " { S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;", " /* -2 because first two uchars in now are masked */", " #endif", " } }", " #endif", "#endif", " signal(SIGINT, stopped);", " set_masks();", "#ifdef BFS", " trail = (Trail *) emalloc(6*sizeof(Trail));", " trail += 3;", "#else", " trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));", " trail++; /* protect trpt-1 refs at depth 0 */", "#endif", "#ifdef SVDUMP", " if (vprefix > 0)", " { char nm[64];", " sprintf(nm, \"%%s.svd\", PanSource);", " if ((svfd = creat(nm, TMODE)) < 0)", " { fprintf(efd, \"couldn't create %%s\\n\", nm);", " vprefix = 0;", " } }", "#endif", "#ifdef RANDSTOR", " srand(s_rand);", "#endif", "#if SYNC>0 && ASYNC==0", " set_recvs();", "#endif", " run();", " done = 1;", " wrapup();", " return 0;", "}", /* end of main() */ "", "void", "usage(FILE *fd)", "{", " fprintf(fd, \"%%s\\n\", SpinVersion);", " fprintf(fd, \"Valid Options are:\\n\");", "#ifndef SAFETY", "#ifdef NP", " fprintf(fd, \"\t-a -> is disabled by -DNP \");", " fprintf(fd, \"(-DNP compiles for -l only)\\n\");", "#else", " fprintf(fd, \"\t-a find acceptance cycles\\n\");", "#endif", "#else", " fprintf(fd, \"\t-a,-l,-f -> are disabled by -DSAFETY\\n\");", "#endif", " fprintf(fd, \"\t-A ignore assert() violations\\n\");", " fprintf(fd, \"\t-b consider it an error to exceed the depth-limit\\n\");", " fprintf(fd, \"\t-cN stop at Nth error \");", " fprintf(fd, \"(defaults to -c1)\\n\");", " fprintf(fd, \"\t-D print state tables in dot-format and stop\\n\");", " fprintf(fd, \"\t-d print state tables and stop\\n\");", " fprintf(fd, \"\t-e create trails for all errors\\n\");", " fprintf(fd, \"\t-E ignore invalid end states\\n\");", "#ifdef SC", " fprintf(fd, \"\t-Ffile use 'file' to store disk-stack\\n\");", "#endif", "#ifndef NOFAIR", " fprintf(fd, \"\t-f add weak fairness (to -a or -l)\\n\");", "#endif", " fprintf(fd, \"\t-hN use different hash-seed N:1..32\\n\");", " fprintf(fd, \"\t-i search for shortest path to error\\n\");", " fprintf(fd, \"\t-I like -i, but approximate and faster\\n\");", " fprintf(fd, \"\t-J reverse eval order of nested unlesses\\n\");", "#ifdef BITSTATE", " fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");", "#endif", "#ifdef BCS", " fprintf(fd, \"\t-LN set scheduling restriction to N (default 0)\\n\");", "#endif", "#ifndef SAFETY", "#ifdef NP", " fprintf(fd, \"\t-l find non-progress cycles\\n\");", "#else", " fprintf(fd, \"\t-l find non-progress cycles -> \");", " fprintf(fd, \"disabled, requires \");", " fprintf(fd, \"compilation with -DNP\\n\");", "#endif", "#endif", "#ifdef BITSTATE", " fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");", " fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");", "#endif", " fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");", "#if NCLAIMS>1", " fprintf(fd, \"\t-N cn -- use the claim named cn\\n\");", " fprintf(fd, \"\t-Nn -- use claim number n\\n\");", "#endif", " fprintf(fd, \"\t-n no listing of unreached states\\n\");", "#ifdef SVDUMP", " fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");", "#endif", " fprintf(fd, \"\t-QN set time-limit on execution of N minutes\\n\");", " fprintf(fd, \"\t-q require empty chans in valid end states\\n\");", "#ifdef HAS_CODE", " fprintf(fd, \"\t-r read and execute trail - can add -v,-n,-PN,-g,-C\\n\");", " fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");", " fprintf(fd, \"\t-C read and execute trail - columnated output (can add -v,-n)\\n\");", " fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");", " fprintf(fd, \"\t-g read and execute trail + msc gui support\\n\");", " fprintf(fd, \"\t-S silent replay: only user defined printfs show\\n\");", "#endif", "#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)", " fprintf(fd, \"\t-RSN use randomization seed N\\n\");", "#endif", "#ifdef BITSTATE", " fprintf(fd, \"\t-RN repeat run Nx with N \");", " fprintf(fd, \"[1..32] independent hash functions\\n\");", " fprintf(fd, \"\t-s same as -k1 (single bit per state)\\n\");", "#endif", " fprintf(fd, \"\t-T create trail files in read-only mode\\n\");", " fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");", " fprintf(fd, \"\t-V print SPIN version number\\n\");", " fprintf(fd, \"\t-v verbose -- filenames in unreached state listing\\n\");", " fprintf(fd, \"\t-wN hashtable of 2^N entries \");", " fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);", " fprintf(fd, \"\t-x do not overwrite an existing trail file\\n\");", "#if NCORE>1", " fprintf(fd, \"\t-zN handoff states below depth N to 2nd cpu (multi_core)\\n\");", "#endif", "#ifdef HAS_CODE", " fprintf(fd, \"\\n\toptions -r, -C, -PN, -g, and -S can optionally be followed by\\n\");", " fprintf(fd, \"\ta filename argument, as in \'-r filename\', naming the trailfile\\n\");", "#endif", "#if NCORE>1", " multi_usage(fd);", "#endif", " exit(1);", "}", "", "char *", "Malloc(unsigned long n)", "{ char *tmp;", "#ifdef MEMLIM", " if (memcnt + (double) n > memlim)", " { printf(\"pan: reached -DMEMLIM bound\\n\");", " goto err;", " }", "#endif", " tmp = (char *) malloc(n);", " if (!tmp)", " { printf(\"pan: out of memory\\n\");", "#ifdef MEMLIM", "err:", " printf(\"\t%%g bytes used\\n\", memcnt);", " printf(\"\t%%g bytes more needed\\n\", (double) n);", " printf(\"\t%%g bytes limit\\n\", memlim);", "#endif", "#ifdef COLLAPSE", " printf(\"hint: to reduce memory, recompile with\\n\");", "#ifndef MA", " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);", "#endif", " printf(\" -DBITSTATE # supertrace, approximation\\n\");", "#else", "#ifndef BITSTATE", " printf(\"hint: to reduce memory, recompile with\\n\");", "#ifndef HC", " printf(\" -DCOLLAPSE # good, fast compression, or\\n\");", "#ifndef MA", " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);", "#endif", " printf(\" -DHC # hash-compaction, approximation\\n\");", "#endif", " printf(\" -DBITSTATE # supertrace, approximation\\n\");", "#endif", "#endif", "#if NCORE>1", " #ifdef FULL_TRAIL", " printf(\" omit -DFULL_TRAIL or use pan -c0 to reduce memory\\n\");", " #endif", " #ifdef SEP_STATE", " printf(\"hint: to reduce memory, recompile without\\n\");", " printf(\" -DSEP_STATE # may be faster, but uses more memory\\n\");", " #endif", "#endif", " wrapup();", " }", " memcnt += (double) n;", " return tmp;", "}", "", "#define CHUNK (100*VECTORSZ)", "", "char *", "emalloc(unsigned long n) /* never released or reallocated */", "{ char *tmp;", " if (n == 0)", " return (char *) NULL;", " if (n&(sizeof(void *)-1)) /* for proper alignment */", " n += sizeof(void *)-(n&(sizeof(void *)-1));", " if ((unsigned long) left < n)", /* was: (left < (long)n) */ " { grow = (n < CHUNK) ? CHUNK : n;", #if 1 " have = Malloc(grow);", #else " /* gcc's sbrk can give non-aligned result */", " grow += sizeof(void *); /* allow realignment */", " have = Malloc(grow);", " if (((unsigned) have)&(sizeof(void *)-1))", " { have += (long) (sizeof(void *) ", " - (((unsigned) have)&(sizeof(void *)-1)));", " grow -= sizeof(void *);", " }", #endif " fragment += (double) left;", " left = grow;", " }", " tmp = have;", " have += (long) n;", " left -= (long) n;", " memset(tmp, 0, n);", " return tmp;", "}", "void", "Uerror(char *str)", "{ /* always fatal */", " uerror(str);", "#if NCORE>1", " sudden_stop(\"Uerror\");", "#endif", " wrapup();", "}\n", "#if defined(MA) && !defined(SAFETY)", "int", "Unwind(void)", "{ Trans *t; uchar ot, _m; int tt; short II;", "#ifdef VERBOSE", " int i;", "#endif", " uchar oat = now._a_t;", " now._a_t &= ~(1|16|32);", " memcpy((char *) &comp_now, (char *) &now, vsize);", " now._a_t = oat;", "Up:", "#ifdef SC", " trpt = getframe(depth);", "#endif", "#ifdef VERBOSE", " printf(\"%%d State: \", depth);", " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",", " ((char *)&now)[i], Mask[i]?\"*\":\"\");", " printf(\"\\n\");", "#endif", "#ifndef NOFAIR", " if (trpt->o_pm&128) /* fairness alg */", " { now._cnt[now._a_t&1] = trpt->bup.oval;", " depth--;", "#ifdef SC", " trpt = getframe(depth);", "#else", " trpt--;", "#endif", " goto Q999;", " }", "#endif", "#ifdef HAS_LAST", "#ifdef VERI", " { int d; Trail *trl;", " now._last = 0;", " for (d = 1; d < depth; d++)", " { trl = getframe(depth-d); /* was trl = (trpt-d); */", " if (trl->pr != 0)", " { now._last = trl->pr - BASE;", " break;", " } } }", "#else", " now._last = (depth<1)?0:(trpt-1)->pr;", "#endif", "#endif", "#ifdef EVENT_TRACE", " now._event = trpt->o_event;", "#endif", " if ((now._a_t&1) && depth <= A_depth)", " { now._a_t &= ~(1|16|32);", " if (fairness) now._a_t |= 2; /* ? */", " A_depth = 0;", " goto CameFromHere; /* checkcycles() */", " }", " t = trpt->o_t;", " ot = trpt->o_ot; II = trpt->pr;", " tt = trpt->o_tt; this = pptr(II);", " _m = do_reverse(t, II, trpt->o_m);", "#ifdef VERBOSE", " printf(\"%%3ld: proc %%d \", depth, II);", " printf(\"reverses %%d, %%d to %%d,\",", " t->forw, tt, t->st);", " printf(\" %%s [abit=%%d,adepth=%%d,\", ", " t->tp, now._a_t, A_depth);", " printf(\"tau=%%d,%%d] \\n\", ", " trpt->tau, (trpt-1)->tau);", "#endif", " depth--;", "#ifdef SC", " trpt = getframe(depth);", "#else", " trpt--;", "#endif", " /* reached[ot][t->st] = 1; 3.4.13 */", " ((P0 *)this)->_p = tt;", "#ifndef NOFAIR", " if ((trpt->o_pm&32))", " {", "#ifdef VERI", " if (now._cnt[now._a_t&1] == 0)", " now._cnt[now._a_t&1] = 1;", "#endif", " now._cnt[now._a_t&1] += 1;", " }", "Q999:", " if (trpt->o_pm&8)", " { now._a_t &= ~2;", " now._cnt[now._a_t&1] = 0;", " }", " if (trpt->o_pm&16)", " now._a_t |= 2;", "#endif", "CameFromHere:", " if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)", " return depth;", " if (depth > 0) goto Up;", " return 0;", "}", "#endif", "static char unwinding;", "void", "uerror(char *str)", "{ static char laststr[256];", " int is_cycle;", "", " if (unwinding) return; /* 1.4.2 */", " if (strncmp(str, laststr, 254))", "#if NCORE>1", " cpu_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,", "#else", " printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,", "#endif", "#if NCORE>1", " (nr_handoffs * z_handoff) + ", "#endif", " ((depthfound==-1)?depth:depthfound));", " strncpy(laststr, str, 254);", " errors++;", "#ifdef HAS_CODE", " if (readtrail) { wrap_trail(); return; }", "#endif", " is_cycle = (strstr(str, \" cycle\") != (char *) 0);", " if (!is_cycle)", " { depth++; trpt++;", /* include failed step */ " }", " if ((every_error != 0)", " || errors == upto)", " {", "#if defined(MA) && !defined(SAFETY)", " if (is_cycle)", " { int od = depth;", " unwinding = 1;", " depthfound = Unwind();", " unwinding = 0;", " depth = od;", " }", "#endif", "#if NCORE>1", " writing_trail = 1;", "#endif", "#ifdef BFS", " if (depth > 1) trpt--;", " nuerror(str);", " if (depth > 1) trpt++;", "#else", " putrail();", "#endif", "#if defined(MA) && !defined(SAFETY)", " if (strstr(str, \" cycle\"))", " { if (every_error)", " printf(\"sorry: MA writes 1 trail max\\n\");", " wrapup(); /* no recovery from unwind */", " }", "#endif", "#if NCORE>1", " if (search_terminated != NULL)", " { *search_terminated |= 4; /* uerror */", " }", " writing_trail = 0;", "#endif", " }", " if (!is_cycle)", " { depth--; trpt--; /* undo */", " }", "#ifndef BFS", " if (iterative != 0 && maxdepth > 0)", " { if (maxdepth > depth)", " { maxdepth = (iterative == 1)?(depth+1):(depth/2);", " }", " warned = 1;", " printf(\"pan: reducing search depth to %%ld\\n\",", " maxdepth);", " } else", "#endif", " if (errors >= upto && upto != 0)", " {", "#if NCORE>1", " sudden_stop(\"uerror\");", "#endif", " wrapup();", " }", " depthfound = -1;", "}\n", "int", "xrefsrc(int lno, S_F_MAP *mp, int M, int i)", "{ Trans *T; int j, retval=1;", " for (T = trans[M][i]; T; T = T->nxt)", " if (T && T->tp)", " { if (strcmp(T->tp, \".(goto)\") == 0", " || strncmp(T->tp, \"goto :\", 6) == 0)", " return 1; /* not reported */", "", " for (j = 0; j < sizeof(mp); j++)", " if (i >= mp[j].from && i <= mp[j].upto)", " { printf(\"\\t%%s:%%d\", mp[j].fnm, lno);", " break;", " }", " if (j >= sizeof(mp)) /* fnm not found in list */", " { printf(\"\\t%%s:%%d\", PanSource, lno); /* use default */", " }", " printf(\", state %%d\", i);", " if (strcmp(T->tp, \"\") != 0)", " { char *q;", " q = transmognify(T->tp);", " printf(\", \\\"%%s\\\"\", q?q:\"\");", " } else if (stopstate[M][i])", " printf(\", -end state-\");", " printf(\"\\n\");", " retval = 0; /* reported */", " }", " return retval;", "}\n", "void", "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)", "{ int i, m=0;", "", " if ((enum btypes) Btypes[M] == N_CLAIM", " && claimname != NULL && strcmp(claimname, procname[M]) != 0)", " { return;", " }", "", " switch ((enum btypes) Btypes[M]) {", " case P_PROC:", " case A_PROC:", " printf(\"unreached in proctype %%s\\n\", procname[M]);", " break;", " case I_PROC:", " printf(\"unreached in init\\n\");", " break;", " case E_TRACE:", " case N_TRACE:", " case N_CLAIM:", " default:", " printf(\"unreached in claim %%s\\n\", procname[M]);", " break;", " }", " for (i = 1; i < N; i++)", " { if (which[i] == 0", " && (mapstate[M][i] == 0", " || which[mapstate[M][i]] == 0))", " { m += xrefsrc((int) src[i], mp, M, i);", " } else", " { m++;", " } }", " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);", "}", "#if NCORE>1 && !defined(SEP_STATE)", "static long rev_trail_cnt;", "", "#ifdef FULL_TRAIL", "void", "rev_trail(int fd, volatile Stack_Tree *st_tr)", "{ long j; char snap[64];", "", " if (!st_tr)", " { return;", " }", " rev_trail(fd, st_tr->prv);", "#ifdef VERBOSE", " printf(\"%%d (%%d) LRT [%%d,%%d] -- %%9u (root %%9u)\\n\",", " depth, rev_trail_cnt, st_tr->pr, st_tr->t_id, st_tr, stack_last[core_id]);", "#endif", " if (st_tr->pr != 255)", /* still needed? */ " { sprintf(snap, \"%%ld:%%d:%%d\\n\", ", " rev_trail_cnt++, st_tr->pr, st_tr->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", " { printf(\"pan: error writing trailfile\\n\");", " close(fd);", " wrapup();", " return;", " }", " } else /* handoff point */", " { if (a_cycles)", " { (void) write(fd, \"-1:-1:-1\\n\", 9);", " } }", "}", "#endif", /* FULL_TRAIL */ "#endif", /* NCORE>1 */ "", "void", "putrail(void)", "{ int fd;", "#if defined VERI || defined(MERGED)", " char snap[64];", "#endif", "#if NCORE==1 || defined(SEP_STATE) || !defined(FULL_TRAIL)", " long i, j;", " Trail *trl;", "#endif", " fd = make_trail();", " if (fd < 0) return;", "#ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);", " if (write(fd, snap, strlen(snap)) < 0) return;", "#endif", "#ifdef MERGED", " sprintf(snap, \"-4:-4:-4\\n\");", " if (write(fd, snap, strlen(snap)) < 0) return;", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && defined(FULL_TRAIL)", " rev_trail_cnt = 1;", " enter_critical(GLOBAL_LOCK);", " rev_trail(fd, stack_last[core_id]);", " leave_critical(GLOBAL_LOCK);", "#else", " i = 1; /* trail starts at position 1 */", " #if NCORE>1 && defined(SEP_STATE)", " if (cur_Root.m_vsize > 0) { i++; depth++; }", " #endif", " for ( ; i <= depth; i++)", " { if (i == depthfound+1)", " { if (write(fd, \"-1:-1:-1\\n\", 9) != 9)", " { goto notgood;", " } }", " trl = getframe(i);", " if (!trl->o_t) continue;", " if (trl->o_pm&128) continue;", " sprintf(snap, \"%%ld:%%d:%%d\\n\", ", " i, trl->pr, trl->o_t->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", " {", "notgood: printf(\"pan: error writing trailfile\\n\");", " close(fd);", " wrapup();", " } }", "#endif", " close(fd);", "#if NCORE>1", " cpu_printf(\"pan: wrote trailfile\\n\");", "#endif", "}\n", "void", "sv_save(void) /* push state vector onto save stack */", "{ if (!svtack->nxt)", " { svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));", " svtack->nxt->body = emalloc(vsize*sizeof(char));", " svtack->nxt->lst = svtack;", " svtack->nxt->m_delta = vsize;", " svmax++;", " } else if (vsize > svtack->nxt->m_delta)", " { svtack->nxt->body = emalloc(vsize*sizeof(char));", " svtack->nxt->lst = svtack;", " svtack->nxt->m_delta = vsize;", " svmax++;", " }", " svtack = svtack->nxt;", "#if SYNC", " svtack->o_boq = boq;", "#endif", "#ifdef TRIX", " sv_populate();", "#endif", " svtack->o_delta = vsize; /* don't compress */", " memcpy((char *)(svtack->body), (char *) &now, vsize);", "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)", " c_stack((uchar *) &(svtack->c_stack[0]));", "#endif", "#ifdef DEBUG", " cpu_printf(\"%%d: sv_save\\n\", depth);", "#endif", "}\n", "void", "sv_restor(void) /* pop state vector from save stack */", "{", " memcpy((char *)&now, svtack->body, svtack->o_delta);", "#if SYNC", " boq = svtack->o_boq;", "#endif", "#ifdef TRIX", " re_populate();", "#endif", "#if defined(C_States) && (HAS_TRACK==1)", "#ifdef HAS_STACK", " c_unstack((uchar *) &(svtack->c_stack[0]));", "#endif", " c_revert((uchar *) &(now.c_state[0]));", "#endif", " if (vsize != svtack->o_delta)", " Uerror(\"sv_restor\");", " if (!svtack->lst)", " Uerror(\"error: sv_restor\");", " svtack = svtack->lst;", "#ifdef DEBUG", " cpu_printf(\" sv_restor\\n\");", "#endif", "}\n", "void", "p_restor(int h)", "{ int i;", " char *z = (char *) &now;\n", "#ifndef TRIX", " proc_offset[h] = stack->o_offset;", " proc_skip[h] = (uchar) stack->o_skip;", "#else", " char *oi;", " #ifdef V_TRIX", " printf(\"%%4d: p_restor %%d\\n\", depth, h);", " #endif", "#endif", "#ifndef XUSAFE", " p_name[h] = stack->o_name;", "#endif", "#ifdef TRIX", " vsize += sizeof(char *);", " #ifndef BFS", " if (processes[h] != NULL || freebodies == NULL)", " { Uerror(\"processes error\");", " }", " processes[h] = freebodies;", " freebodies = freebodies->nxt;", " processes[h]->nxt = (TRIX_v6 *) 0;", " processes[h]->modified = 1; /* p_restor */", " #endif", " processes[h]->parent_pid = stack->parent;", " processes[h]->psize = stack->o_delta;", " memcpy((char *)pptr(h), stack->b_ptr, stack->o_delta);", " oi = stack->b_ptr;", "#else", " #ifndef NOCOMP", " for (i = vsize + stack->o_skip; i > vsize; i--)", " Mask[i-1] = 1; /* align */", " #endif", " vsize += stack->o_skip;", " memcpy(z+vsize, stack->body, stack->o_delta);", " vsize += stack->o_delta;", " #ifndef NOCOMP", " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)", " Mask[vsize - i] = 1; /* pad */", " Mask[proc_offset[h]] = 1; /* _pid */", " #endif", " if (BASE > 0 && h > 0)", " ((P0 *)pptr(h))->_pid = h-BASE;", " else", " ((P0 *)pptr(h))->_pid = h;", "#endif", " now._nr_pr += 1;", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", " i = stack->o_delqs;", " if (!stack->lst)", " Uerror(\"error: p_restor\");", " stack = stack->lst;", " this = pptr(h);", " while (i-- > 0)", " q_restor();", "#ifdef TRIX", " re_mark_all(1); /* p_restor - all chans move up in _ids_ */", " now._ids_[h] = oi; /* restor the original contents */", "#endif", "}\n", "void", "q_restor(void)", "{ int h = now._nr_qs;", "#ifdef TRIX", " #ifdef V_TRIX", " printf(\"%%4d: q_restor %%d\\n\", depth, h);", " #endif", " vsize += sizeof(char *);", " #ifndef BFS", " if (channels[h] != NULL || freebodies == NULL)", " { Uerror(\"channels error\");", " }", " channels[h] = freebodies;", " freebodies = freebodies->nxt;", " channels[h]->nxt = (TRIX_v6 *) 0;", " channels[h]->modified = 1; /* q_restor */", " #endif", " channels[h]->parent_pid = stack->parent;", " channels[h]->psize = stack->o_delta;", " memcpy((char *)qptr(h), stack->b_ptr, stack->o_delta);", " now._ids_[now._nr_pr + h] = stack->b_ptr;", "#else", " char *z = (char *) &now;", " #ifndef NOCOMP", " int k, k_end;", " #endif", " q_offset[h] = stack->o_offset;", " q_skip[h] = (uchar) stack->o_skip;", " vsize += stack->o_skip;", " memcpy(z+vsize, stack->body, stack->o_delta);", " vsize += stack->o_delta;", "#endif", "#ifndef XUSAFE", " q_name[h] = stack->o_name;", "#endif", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", " now._nr_qs += 1;", "#ifndef NOCOMP", "#ifndef TRIX", " k_end = stack->o_offset;", " k = k_end - stack->o_skip;", " #if SYNC", " #ifndef BFS", " if (q_zero(now._nr_qs)) k_end += stack->o_delta;", " #endif", " #endif", " for ( ; k < k_end; k++)", " Mask[k] = 1;", "#endif", "#endif", " if (!stack->lst)", " Uerror(\"error: q_restor\");", " stack = stack->lst;", "}", "typedef struct IntChunks {", " int *ptr;", " struct IntChunks *nxt;", "} IntChunks;", "IntChunks *filled_chunks[512];", "IntChunks *empty_chunks[512];", "int *", "grab_ints(int nr)", "{ IntChunks *z;", " if (nr >= 512) Uerror(\"cannot happen grab_int\");", " if (filled_chunks[nr])", " { z = filled_chunks[nr];", " filled_chunks[nr] = filled_chunks[nr]->nxt;", " } else ", " { z = (IntChunks *) emalloc(sizeof(IntChunks));", " z->ptr = (int *) emalloc(nr * sizeof(int));", " }", " z->nxt = empty_chunks[nr];", " empty_chunks[nr] = z;", " return z->ptr;", "}", "void", "ungrab_ints(int *p, int nr)", "{ IntChunks *z;", " if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");", " z = empty_chunks[nr];", " empty_chunks[nr] = empty_chunks[nr]->nxt;", " z->ptr = p;", " z->nxt = filled_chunks[nr];", " filled_chunks[nr] = z;", "}", "int", "delproc(int sav, int h)", "{ int d, i=0;", "#ifndef NOCOMP", " int o_vsize = vsize;", "#endif", " if (h+1 != (int) now._nr_pr)", " { return 0;", " }", "#ifdef TRIX", " #ifdef V_TRIX", " printf(\"%%4d: delproc %%d -- parent %%d\\n\", depth, h, processes[h]->parent_pid);", " if (now._nr_qs > 0)", " printf(\" top channel: %%d -- parent %%d\\n\", now._nr_qs-1, channels[now._nr_qs-1]->parent_pid);", " #endif", " while (now._nr_qs > 0", " && channels[now._nr_qs-1]->parent_pid == processes[h]->parent_pid)", " { delq(sav);", " i++;", " }", " d = processes[h]->psize;", " if (sav)", " { if (!stack->nxt)", " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));", " stack->nxt->lst = stack;", " smax++;", " }", " stack = stack->nxt;", " #ifndef XUSAFE", " stack->o_name = p_name[h];", " #endif", " stack->parent = processes[h]->parent_pid;", " stack->o_delta = d;", " stack->o_delqs = i;", " stack->b_ptr = now._ids_[h];", /* new 6.1 */ " }", " memset((char *)pptr(h), 0, d);", " #ifndef BFS", " processes[h]->nxt = freebodies;", " freebodies = processes[h];", " processes[h] = (TRIX_v6 *) 0;", " #endif", " vsize -= sizeof(char *);", " now._nr_pr -= 1;", " re_mark_all(-1); /* delproc - all chans move down in _ids_ */", "#else", " while (now._nr_qs", " && q_offset[now._nr_qs-1] > proc_offset[h])", " { delq(sav);", " i++;", " }", " d = vsize - proc_offset[h];", " if (sav)", " { if (!stack->nxt)", " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));", " stack->nxt->body = emalloc(Maxbody * sizeof(char));", " stack->nxt->lst = stack;", " smax++;", " }", " stack = stack->nxt;", " stack->o_offset = proc_offset[h];", " #if VECTORSZ>32000", " stack->o_skip = (int) proc_skip[h];", " #else", " stack->o_skip = (short) proc_skip[h];", " #endif", " #ifndef XUSAFE", " stack->o_name = p_name[h];", " #endif", " stack->o_delta = d;", " stack->o_delqs = i;", " memcpy(stack->body, (char *)pptr(h), d);", " }", " vsize = proc_offset[h];", " now._nr_pr -= 1;", " memset((char *)pptr(h), 0, d);", " vsize -= (int) proc_skip[h];", " #ifndef NOCOMP", " for (i = vsize; i < o_vsize; i++)", " Mask[i] = 0; /* reset */", " #endif", "#endif", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", " return 1;", "}\n", "void", "delq(int sav)", "{ int h = now._nr_qs - 1;", "#ifdef TRIX", " int d = channels[now._nr_qs - 1]->psize;", "#else", " int d = vsize - q_offset[now._nr_qs - 1];", "#endif", "#ifndef NOCOMP", " int k, o_vsize = vsize;", "#endif", " if (sav)", " { if (!stack->nxt)", " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));", "#ifndef TRIX", " stack->nxt->body = emalloc(Maxbody * sizeof(char));", "#endif", " stack->nxt->lst = stack;", " smax++;", " }", " stack = stack->nxt;", "#ifdef TRIX", " stack->parent = channels[h]->parent_pid;", " stack->b_ptr = now._ids_[h];", /* new 6.1 */ "#else", " stack->o_offset = q_offset[h];", " #if VECTORSZ>32000", " stack->o_skip = (int) q_skip[h];", " #else", " stack->o_skip = (short) q_skip[h];", " #endif", "#endif", " #ifndef XUSAFE", " stack->o_name = q_name[h];", " #endif", " stack->o_delta = d;", "#ifndef TRIX", " memcpy(stack->body, (char *)qptr(h), d);", "#endif", " }", "#ifdef TRIX", " vsize -= sizeof(char *);", " #ifdef V_TRIX", " printf(\"%%4d: delq %%d parent %%d\\n\", depth, h, channels[h]->parent_pid);", " #endif", "#else", " vsize = q_offset[h];", " vsize -= (int) q_skip[h];", " #ifndef NOCOMP", " for (k = vsize; k < o_vsize; k++)", " Mask[k] = 0; /* reset */", " #endif", "#endif", " now._nr_qs -= 1;", " memset((char *)qptr(h), 0, d);", "#ifdef TRIX", " #ifndef BFS", " channels[h]->nxt = freebodies;", " freebodies = channels[h];", " channels[h] = (TRIX_v6 *) 0;", " #endif", "#endif", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", "}\n", "int", "qs_empty(void)", "{ int i;", " for (i = 0; i < (int) now._nr_qs; i++)", " { if (q_sz(i) > 0)", " return 0;", " }", " return 1;", "}\n", "int", "endstate(void)", "{ int i; P0 *ptr;", " for (i = BASE; i < (int) now._nr_pr; i++)", " { ptr = (P0 *) pptr(i);", " if (!stopstate[ptr->_t][ptr->_p])", " return 0;", " }", " if (strict) return qs_empty();", "#if defined(EVENT_TRACE) && !defined(OTIM)", " if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)", " { printf(\"pan: event_trace not completed\\n\");", " return 0;", " }", "#endif", " return 1;", "}\n", "#ifndef SAFETY", "void", "checkcycles(void)", "{ uchar o_a_t = now._a_t;", "#ifndef NOFAIR", " uchar o_cnt = now._cnt[1];", "#endif", "#ifdef FULLSTACK", "#ifndef MA", " struct H_el *sv = trpt->ostate; /* save */", "#else", " uchar prov = trpt->proviso; /* save */", "#endif", "#endif", "#ifdef DEBUG", " { int i; uchar *v = (uchar *) &now;", " printf(\" set Seed state \");", "#ifndef NOFAIR", " if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",", " now._cnt[0], now._cnt[1], now._nr_pr);", "#endif", " /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */", " printf(\"\\n\");", " }", " printf(\"%%ld: cycle check starts\\n\", depth);", "#endif", " now._a_t |= (1|16|32);", " /* 1 = 2nd DFS; (16|32) to help hasher */", "#ifndef NOFAIR", " now._cnt[1] = now._cnt[0];", "#endif", " memcpy((char *)&A_Root, (char *)&now, vsize);", " A_depth = depthfound = depth;", "#if NCORE>1", " mem_put_acc();", /* handoff accept states */ "#else", " new_state(); /* start 2nd DFS */", "#endif", " now._a_t = o_a_t;", "#ifndef NOFAIR", " now._cnt[1] = o_cnt;", "#endif", " A_depth = 0; depthfound = -1;", "#ifdef DEBUG", " printf(\"%%ld: cycle check returns\\n\", depth);", "#endif", "#ifdef FULLSTACK", "#ifndef MA", " trpt->ostate = sv; /* restore */", "#else", " trpt->proviso = prov;", "#endif", "#endif", "}", "#endif\n", "#if defined(FULLSTACK) && defined(BITSTATE)", "struct H_el *Free_list = (struct H_el *) 0;", "void", "onstack_init(void) /* to store stack states in a bitstate search */", "{ S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));", "}", "struct H_el *", "grab_state(int n)", "{ struct H_el *v, *last = 0;", " if (H_tab == S_Tab)", " { for (v = Free_list; v && ((int) v->tagged >= n); v=v->nxt)", " { if ((int) v->tagged == n)", " { if (last)", " last->nxt = v->nxt;", " else", "gotcha: Free_list = v->nxt;", " v->tagged = 0;", " v->nxt = 0;", "#ifdef COLLAPSE", " v->ln = 0;", "#endif", " return v;", " }", " Fh++; last=v;", " }", " /* new: second try */", " v = Free_list;", /* try to avoid emalloc */ " if (v && ((int) v->tagged >= n))", " goto gotcha;", " ngrabs++;", " }", " return (struct H_el *)", " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));", "}\n", "#else", "#if NCORE>1", "struct H_el *", "grab_state(int n)", "{ struct H_el *grab_shared(int);", " return grab_shared(sizeof(struct H_el)+n-sizeof(unsigned));", "}", "#else", " #ifndef AUTO_RESIZE", " #define grab_state(n) (struct H_el *) \\", " emalloc(sizeof(struct H_el)+n-sizeof(unsigned long));", " #else", " struct H_el *", " grab_state(int n)", " { struct H_el *p;", " int cnt = sizeof(struct H_el)+n-sizeof(unsigned long);", "", " if (reclaim_size >= cnt+WS)", " { if ((cnt & (WS-1)) != 0) /* alignment */", " { cnt += WS - (cnt & (WS-1));", " }", " p = (struct H_el *) reclaim_mem;", " reclaim_mem += cnt;", " reclaim_size -= cnt;", " memset(p, 0, cnt);", " } else", " { p = (struct H_el *) emalloc(cnt);", " }", " return p;", " }", " #endif", "#endif", "#endif", "#ifdef COLLAPSE", "unsigned long", "ordinal(char *v, long n, short tp)", "{ struct H_el *tmp, *ntmp; long m;", " struct H_el *olst = (struct H_el *) 0;", " s_hash((uchar *)v, n);", "#if NCORE>1 && !defined(SEP_STATE)", " enter_critical(CS_ID); /* uses spinlock - 1..128 */", "#endif", " tmp = H_tab[j1_spin];", " if (!tmp)", " { tmp = grab_state(n);", " H_tab[j1_spin] = tmp;", " } else", " for ( ;; olst = tmp, tmp = tmp->nxt)", " { if (n == tmp->ln)", " { m = memcmp(((char *)&(tmp->state)), v, n);", " if (m == 0)", " goto done;", " if (m < 0)", " {", "Insert: ntmp = grab_state(n);", " ntmp->nxt = tmp;", " if (!olst)", " H_tab[j1_spin] = ntmp;", " else", " olst->nxt = ntmp;", " tmp = ntmp;", " break;", " } else if (!tmp->nxt)", " {", "Append: tmp->nxt = grab_state(n);", " tmp = tmp->nxt;", " break;", " }", " continue;", " }", " if (n < tmp->ln)", " goto Insert;", " else if (!tmp->nxt)", " goto Append;", " }", "#if NCORE>1 && !defined(SEP_STATE)", " enter_critical(GLOBAL_LOCK);", "#endif", " m = ++ncomps[tp];", "#if NCORE>1 && !defined(SEP_STATE)", " leave_critical(GLOBAL_LOCK);", "#endif", "#ifdef FULLSTACK", " tmp->tagged = m;", "#else", " tmp->st_id = m;", "#endif", "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", " tmp->m_K1 = K1;", "#endif", " memcpy(((char *)&(tmp->state)), v, n);", " tmp->ln = n;", "done:", "#if NCORE>1 && !defined(SEP_STATE)", " leave_critical(CS_ID); /* uses spinlock */", "#endif", "#ifdef FULLSTACK", " return tmp->tagged;", "#else", " return tmp->st_id;", "#endif", "}", "", "int", "compress(char *vin, int nin) /* collapse compression */", "{ char *w, *v = (char *) &comp_now;", " int i, j;", " unsigned long n;", " static char *x;", " static uchar nbytes[513]; /* 1 + 256 + 256 */", " static unsigned short nbytelen;", " long col_q(int, char *);", " long col_p(int, char *);", "#ifndef SAFETY", " if (a_cycles)", " *v++ = now._a_t;", "#ifndef NOFAIR", " if (fairness)", " for (i = 0; i < NFAIR; i++)", " *v++ = now._cnt[i];", "#endif", "#endif", " nbytelen = 0;", "#ifndef JOINPROCS", " for (i = 0; i < (int) now._nr_pr; i++)", " { n = col_p(i, (char *) 0);", "#ifdef NOFIX", " nbytes[nbytelen] = 0;", "#else", " nbytes[nbytelen] = 1;", " *v++ = ((P0 *) pptr(i))->_t;", "#endif", " *v++ = n&255;", " if (n >= (1<<8))", " { nbytes[nbytelen]++;", " *v++ = (n>>8)&255;", " }", " if (n >= (1<<16))", " { nbytes[nbytelen]++;", " *v++ = (n>>16)&255;", " }", " if (n >= (1<<24))", " { nbytes[nbytelen]++;", " *v++ = (n>>24)&255;", " }", " nbytelen++;", " }", "#else", " x = scratch;", " for (i = 0; i < (int) now._nr_pr; i++)", " x += col_p(i, x);", " n = ordinal(scratch, x-scratch, 2); /* procs */", " *v++ = n&255;", " nbytes[nbytelen] = 0;", " if (n >= (1<<8))", " { nbytes[nbytelen]++;", " *v++ = (n>>8)&255;", " }", " if (n >= (1<<16))", " { nbytes[nbytelen]++;", " *v++ = (n>>16)&255;", " }", " if (n >= (1<<24))", " { nbytes[nbytelen]++;", " *v++ = (n>>24)&255;", " }", " nbytelen++;", "#endif", "#ifdef SEPQS", " for (i = 0; i < (int) now._nr_qs; i++)", " { n = col_q(i, (char *) 0);", " nbytes[nbytelen] = 0;", " *v++ = n&255;", " if (n >= (1<<8))", " { nbytes[nbytelen]++;", " *v++ = (n>>8)&255;", " }", " if (n >= (1<<16))", " { nbytes[nbytelen]++;", " *v++ = (n>>16)&255;", " }", " if (n >= (1<<24))", " { nbytes[nbytelen]++;", " *v++ = (n>>24)&255;", " }", " nbytelen++;", " }", "#endif", "#ifdef NOVSZ", " /* 3 = _a_t, _nr_pr, _nr_qs */", " w = (char *) &now + 3 * sizeof(uchar);", "#ifndef NOFAIR", " w += NFAIR;", "#endif", "#else", "#if VECTORSZ<65536", " w = (char *) &(now._vsz) + sizeof(unsigned short);", "#else", " w = (char *) &(now._vsz) + sizeof(unsigned long);", "#endif", "#endif", " x = scratch;", " *x++ = now._nr_pr;", " *x++ = now._nr_qs;", " if (now._nr_qs > 0 && qptr(0) < pptr(0))", " n = qptr(0) - (uchar *) w;", " else", " n = pptr(0) - (uchar *) w;", " j = w - (char *) &now;", " for (i = 0; i < (int) n; i++, w++)", " if (!Mask[j++]) *x++ = *w;", "#ifndef SEPQS", " for (i = 0; i < (int) now._nr_qs; i++)", " x += col_q(i, x);", "#endif", " x--;", " for (i = 0, j = 6; i < nbytelen; i++)", " { if (j == 6)", " { j = 0;", " *(++x) = 0;", " } else", " j += 2;", " *x |= (nbytes[i] << j);", " }", " x++;", " for (j = 0; j < WS-1; j++)", " *x++ = 0;", " x -= j; j = 0;", " n = ordinal(scratch, x-scratch, 0); /* globals */", " *v++ = n&255;", " if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }", " if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }", " if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }", " *v++ = j; /* add last count as a byte */", " for (i = 0; i < WS-1; i++)", " *v++ = 0;", " v -= i;", "#if 0", " printf(\"collapse %%d -> %%d\\n\",", " vsize, v - (char *)&comp_now);", "#endif", " return v - (char *)&comp_now;", "}", "#else", "#if !defined(NOCOMP)", "int", "compress(char *vin, int n) /* default compression */", "{", "#ifdef HC", " int delta = 0;", " s_hash((uchar *)vin, n); /* sets K1 and K2 */", "#ifndef SAFETY", " if (S_A)", " { delta++; /* _a_t */", "#ifndef NOFAIR", " if (S_A > NFAIR)", " delta += NFAIR; /* _cnt[] */", "#endif", " }", "#endif", " memcpy((char *) &comp_now + delta, (char *) &K1, WS);", " delta += WS;", "#if HC>0", " memcpy((char *) &comp_now + delta, (char *) &K2, HC);", " delta += HC;", "#endif", " return delta;", "#else", " char *vv = vin;", " char *v = (char *) &comp_now;", " int i;", " #ifndef NO_FAST_C", /* disable faster compress */ " int r = 0, unroll = n/8;", /* most sv are much longer */ " if (unroll > 0)", " { i = 0;", " while (r++ < unroll)", " { /* unroll 8 times, avoid ifs */", " /* 1 */ *v = *vv++; v += 1 - Mask[i++];", " /* 2 */ *v = *vv++; v += 1 - Mask[i++];", " /* 3 */ *v = *vv++; v += 1 - Mask[i++];", " /* 4 */ *v = *vv++; v += 1 - Mask[i++];", " /* 5 */ *v = *vv++; v += 1 - Mask[i++];", " /* 6 */ *v = *vv++; v += 1 - Mask[i++];", " /* 7 */ *v = *vv++; v += 1 - Mask[i++];", " /* 8 */ *v = *vv++; v += 1 - Mask[i++];", " }", " r = n - i; /* the rest, at most 7 */", " switch (r) {", " case 7: *v = *vv++; v += 1 - Mask[i++];", " case 6: *v = *vv++; v += 1 - Mask[i++];", " case 5: *v = *vv++; v += 1 - Mask[i++];", " case 4: *v = *vv++; v += 1 - Mask[i++];", " case 3: *v = *vv++; v += 1 - Mask[i++];", " case 2: *v = *vv++; v += 1 - Mask[i++];", " case 1: *v = *vv++; v += 1 - Mask[i++];", " case 0: break;", " }", "#if 1", " n = i = v - (char *)&comp_now; /* bytes written so far */", "#endif", " r = (n+WS-1)/WS; /* in words, rounded up */", " r *= WS; /* total bytes to fill */", " i = r - i; /* remaining bytes */", " switch (i) {", /* fill word */ " case 7: *v++ = 0; /* fall thru */", " case 6: *v++ = 0;", " case 5: *v++ = 0;", " case 4: *v++ = 0;", " case 3: *v++ = 0;", " case 2: *v++ = 0;", " case 1: *v++ = 0;", " case 0: break;", " default: Uerror(\"unexpected wordsize\");", " }", " v -= i;", " } else", " #endif", " { for (i = 0; i < n; i++, vv++)", " if (!Mask[i]) *v++ = *vv;", " for (i = 0; i < WS-1; i++)", " *v++ = 0;", " v -= i;", " }", "#if 0", " printf(\"compress %%d -> %%d\\n\",", " n, v - (char *)&comp_now);", "#endif", " return v - (char *)&comp_now;", "#endif", "}", "#endif", "#endif", "#if defined(FULLSTACK) && defined(BITSTATE)", "#if defined(MA)", "#if !defined(onstack_now)", "int onstack_now(void) {}", /* to suppress compiler errors */ "#endif", "#if !defined(onstack_put)", "void onstack_put(void) {}", /* for this invalid combination */ "#endif", "#if !defined(onstack_zap)", "void onstack_zap(void) {}", /* of directives */ "#endif", "#else", "void", "onstack_zap(void)", "{ struct H_el *v, *w, *last = 0;", " struct H_el **tmp = H_tab;", " char *nv; int n, m;", " static char warned = 0;", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " uchar was_last = now._last;", " now._last = 0;", "#endif", "", " H_tab = S_Tab;", "#ifndef NOCOMP", " nv = (char *) &comp_now;", " n = compress((char *)&now, vsize);", "#else", "#if defined(BITSTATE) && defined(LC)", " nv = (char *) &comp_now;", " n = compact_stack((char *)&now, vsize);", "#else", " nv = (char *) &now;", " n = vsize;", "#endif", "#endif", "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))", " s_hash((uchar *)nv, n);", "#endif", " H_tab = tmp;", " for (v = S_Tab[j1_spin]; v; Zh++, last=v, v=v->nxt)", " { m = memcmp(&(v->state), nv, n);", " if (m == 0)", " goto Found;", " if (m < 0)", " break;", " }", "/* NotFound: */", "#ifndef ZAPH", " /* seen this happen, likely harmless in multicore */", " if (warned == 0)", " { /* Uerror(\"stack out of wack - zap\"); */", " cpu_printf(\"pan: warning, stack incomplete\\n\");", " warned = 1;", " }", "#endif", " goto done;", "Found:", " ZAPS++;", " if (last)", " last->nxt = v->nxt;", " else", " S_Tab[j1_spin] = v->nxt;", " v->tagged = (unsigned) n;", "#if !defined(NOREDUCE) && !defined(SAFETY)", " v->proviso = 0;", "#endif", " v->nxt = last = (struct H_el *) 0;", " for (w = Free_list; w; Fa++, last=w, w = w->nxt)", " { if ((int) w->tagged <= n)", " { if (last)", " { v->nxt = w;", " last->nxt = v;", " } else", " { v->nxt = Free_list;", " Free_list = v;", " }", " goto done;", " }", " if (!w->nxt)", " { w->nxt = v;", " goto done;", " } }", " Free_list = v;", "done:", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " now._last = was_last;", "#endif", " return;", "}", "void", "onstack_put(void)", "{ struct H_el **tmp = H_tab;", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " uchar was_last = now._last;", " now._last = 0;", "#endif", " H_tab = S_Tab;", " if (hstore((char *)&now, vsize) != 0)", "#if defined(BITSTATE) && defined(LC)", " printf(\"pan: warning, double stack entry\\n\");", "#else", " #ifndef ZAPH", " Uerror(\"cannot happen - unstack_put\");", " #endif", "#endif", " H_tab = tmp;", " trpt->ostate = Lstate;", " PUT++;", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " now._last = was_last;", "#endif", "}", "int", "onstack_now(void)", "{ struct H_el *tmp;", " struct H_el **tmp2 = H_tab;", " char *v; int n, m = 1;\n", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " uchar was_last = now._last;", " now._last = 0;", "#endif", " H_tab = S_Tab;", "#ifdef NOCOMP", "#if defined(BITSTATE) && defined(LC)", " v = (char *) &comp_now;", " n = compact_stack((char *)&now, vsize);", "#else", " v = (char *) &now;", " n = vsize;", "#endif", "#else", " v = (char *) &comp_now;", " n = compress((char *)&now, vsize);", "#endif", "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))", " s_hash((uchar *)v, n);", "#endif", " H_tab = tmp2;", " for (tmp = S_Tab[j1_spin]; tmp; Zn++, tmp = tmp->nxt)", " { m = memcmp(((char *)&(tmp->state)),v,n);", " if (m <= 0)", " { Lstate = (struct H_el *) tmp;", " break;", " } }", " PROBE++;", "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " now._last = was_last;", "#endif", " return (m == 0);", "}", "#endif", "#endif", "#ifndef BITSTATE", "void", "hinit(void)", "{", " #ifdef MA", "#ifdef R_XPT", " { void r_xpoint(void);", " r_xpoint();", " }", "#else", " dfa_init((unsigned short) (MA+a_cycles));", "#if NCORE>1 && !defined(COLLAPSE)", " if (!readtrail)", " { void init_HT(unsigned long);", " init_HT(0L);", " }", "#endif", "#endif", " #endif", " #if !defined(MA) || defined(COLLAPSE)", "#if NCORE>1", " if (!readtrail)", " { void init_HT(unsigned long);", " init_HT((unsigned long) (ONE_L<= MA)", " { printf(\"pan: error, MA too small, recompile pan.c\");", " printf(\" with -DMA=N with N>%%d\\n\", n);", " Uerror(\"aborting\");", " }", " if (n > (int) maxgs)", " { maxgs = (unsigned int) n;", " }", " for (i = 0; i < n; i++)", " { Info[i] = v[i];", " }", " for ( ; i < MA-1; i++)", " { Info[i] = 0;", " }", " Info[MA-1] = pbit;", " if (a_cycles) /* place _a_t at the end */", " { Info[MA] = Info[0];", " Info[0] = 0;", " }", "", "#if NCORE>1 && !defined(SEP_STATE)", " enter_critical(GLOBAL_LOCK); /* crude, but necessary */", " /* to make this mode work, also replace emalloc with grab_shared inside store MA routines */", "#endif", "", " if (!dfa_store(Info))", " { if (pbit == 0", " && (now._a_t&1)", " && depth > A_depth)", " { Info[MA] &= ~(1|16|32); /* _a_t */", " if (dfa_member(MA))", /* was !dfa_member(MA) */ " { Info[MA-1] = 4; /* off-stack bit */", " nShadow++;", " if (!dfa_member(MA-1))", " { ret_val = 3;", " #ifdef VERBOSE", " printf(\"intersected 1st dfs stack\\n\");", " #endif", " goto done;", " } } }", " ret_val = 0;", " #ifdef VERBOSE", " printf(\"new state\\n\");", " #endif", " goto done;", " }", "#ifdef FULLSTACK", " if (pbit == 0)", " { Info[MA-1] = 1; /* proviso bit */", "#ifndef BFS", " trpt->proviso = dfa_member(MA-1);", "#endif", " Info[MA-1] = 4; /* off-stack bit */", " if (dfa_member(MA-1))", " { ret_val = 1; /* off-stack */", " #ifdef VERBOSE", " printf(\"old state\\n\");", " #endif", " } else", " { ret_val = 2; /* on-stack */", " #ifdef VERBOSE", " printf(\"on-stack\\n\");", " #endif", " }", " goto done;", " }", "#endif", " ret_val = 1;", "#ifdef VERBOSE", " printf(\"old state\\n\");", "#endif", "done:", "#if NCORE>1 && !defined(SEP_STATE)", " leave_critical(GLOBAL_LOCK);", "#endif", " return ret_val; /* old state */", "}", "#endif", "#if defined(BITSTATE) && defined(LC)", "int", "compact_stack(char *vin, int n)", /* special case of HC4 */ "{ int delta = 0;", " s_hash((uchar *)vin, n); /* sets K1 and K2 */", "#ifndef SAFETY", " delta++; /* room for state[0] |= 128 */", "#endif", " memcpy((char *) &comp_now + delta, (char *) &K1, WS);", " delta += WS;", " memcpy((char *) &comp_now + delta, (char *) &K2, WS);", " delta += WS; /* use all available bits */", " return delta;", "}", "#endif", "#ifdef TRIX", "void", "sv_populate(void)", "{ int i, cnt = 0;", " TRIX_v6 **base = processes;", " int bound = now._nr_pr; /* MAXPROC+1; */", "#ifdef V_TRIX", " printf(\"%%4d: sv_populate\\n\", depth);", "#endif", "again:", " for (i = 0; i < bound; i++)", " { if (base[i] != NULL)", " { struct H_el *tmp;", " int m, n; uchar *v;", "#ifndef BFS", " if (base[i]->modified == 0)", " { cnt++;", " #ifdef V_TRIX", " printf(\"%%4d: %%s %%d not modified\\n\",", " depth, (base == processes)?\"proc\":\"chan\", i);", " #endif", " continue;", " }", " #ifndef V_MOD", " base[i]->modified = 0;", " #endif", "#endif", "#ifdef TRIX_RIX", " if (base == processes)", " { ((P0 *)pptr(i))->_pid = 0;", " }", "#endif", " n = base[i]->psize;", " v = base[i]->body;", " s_hash(v, n); /* sets j1_spin */", " tmp = H_tab[j1_spin];", " if (!tmp) /* new */", " { tmp = grab_state(n);", " H_tab[j1_spin] = tmp;", " m = 1; /* non-zero */", " } else", " { struct H_el *ntmp, *olst = (struct H_el *) 0;", " for (;; hcmp++, olst = tmp, tmp = tmp->nxt)", " { m = memcmp(((char *)&(tmp->state)), v, n);", " if (m == 0) /* match */", " { break;", " } else if (m < 0) /* insert */", " { ntmp = grab_state(n);", " ntmp->nxt = tmp;", " if (!olst)", " H_tab[j1_spin] = ntmp;", " else", " olst->nxt = ntmp;", " tmp = ntmp;", " break;", " } else if (!tmp->nxt) /* append */", " { tmp->nxt = grab_state(n);", " tmp = tmp->nxt;", " break;", " } } }", " if (m != 0)", " { memcpy((char *)&(tmp->state), v, n);", "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", " tmp->m_K1 = K1; /* set via s_hash */", "#endif", " if (base == processes)", " { _p_count[i]++;", " } else", " { _c_count[i]++;", " } }", " now._ids_[cnt++] = (char *)&(tmp->state);", "#ifdef TRIX_RIX", " if (base == processes)", " { ((P0 *)pptr(i))->_pid = i;", " }", "#endif", " } }", #if 0 if a process appears or disappears: always secure a full sv_populate (channels come and go only with a process) only one process can disappear per step but any nr of channels can be removed at the same time if a process disappears, all subsequent entries are then in the wrong place in the _ids_ list and need to be recomputed but we do not need to fill out with zeros because vsize prevents them being used #endif " /* do the same for all channels */", " if (base == processes)", " { base = channels;", " bound = now._nr_qs; /* MAXQ+1; */", " goto again;", " }", "}", "#endif\n", "int", "hstore(char *vin, int nin) /* hash table storage */", "{ struct H_el *ntmp;", " struct H_el *tmp, *olst = (struct H_el *) 0;", " char *v; int n, m=0;", "#ifdef HC", " uchar rem_a;", "#endif", "#ifdef TRIX", " sv_populate(); /* update proc and chan ids */", "#endif", "#ifdef NOCOMP", /* defined by BITSTATE */ " #if defined(BITSTATE) && defined(LC)", " if (S_Tab == H_tab)", " { v = (char *) &comp_now;", " n = compact_stack(vin, nin);", " } else", " { v = vin; n = nin;", " }", " #else", " v = vin; n = nin;", " #endif", "#else", " v = (char *) &comp_now;", " #ifdef HC", " rem_a = now._a_t;", /* new 5.0 */ " now._a_t = 0;", /* for hashing/state matching to work right */ " #endif", " n = compress(vin, nin);", /* with HC, this calls s_hash -- but on vin, not on v... */ " #ifdef HC", " now._a_t = rem_a;", /* new 5.0 */ " #endif", /* with HC4 -a, compress copies K1 and K2 into v[], leaving v[0] free for the a-bit */ "#ifndef SAFETY", " if (S_A)", " { v[0] = 0; /* _a_t */", "#ifndef NOFAIR", " if (S_A > NFAIR)", " for (m = 0; m < NFAIR; m++)", " v[m+1] = 0; /* _cnt[] */", "#endif", " m = 0;", " }", " #endif", "#endif", "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))", " s_hash((uchar *)v, n);", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " enter_critical(CS_ID); /* uses spinlock */", "#endif", " tmp = H_tab[j1_spin];", " if (!tmp)", " { tmp = grab_state(n);", "#if NCORE>1", " if (!tmp)", " { /* if we get here -- we've already issued a warning */", " /* but we want to allow the normal distributed termination */", " /* to collect the stats on all cpus in the wrapup */", " #if !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", " return 1; /* allow normal termination */", " }", "#endif", " H_tab[j1_spin] = tmp;", " } else", " { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)", " { /* skip the _a_t and the _cnt bytes */", "#ifdef COLLAPSE", " if (tmp->ln != 0)", " { if (!tmp->nxt) goto Append;", " continue;", " }", "#endif", " m = memcmp(((char *)&(tmp->state)) + S_A, ", " v + S_A, n - S_A);", " if (m == 0) {", "#ifdef SAFETY", "#define wasnew 0", "#else", " int wasnew = 0;", "#endif", "#ifndef SAFETY", "#ifndef NOCOMP", " if (S_A)", " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)", " { wasnew = 1; nShadow++;", " ((char *)&(tmp->state))[0] |= V_A;", " }", "#ifndef NOFAIR", " if (S_A > NFAIR)", " { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */", " unsigned ci, bp; /* index, bit pos */", " ci = (now._cnt[now._a_t&1] / 8);", " bp = (now._cnt[now._a_t&1] - 8*ci);", " if (now._a_t&1) /* use tail-bits in _cnt */", " { ci = (NFAIR - 1) - ci;", " bp = 7 - bp; /* bp = 0..7 */", " }", " ci++; /* skip over _a_t */", " bp = 1 << bp; /* the bit mask */", " if ((((char *)&(tmp->state))[ci] & bp)==0)", " { if (!wasnew)", " { wasnew = 1;", " nShadow++;", " }", " ((char *)&(tmp->state))[ci] |= bp;", " }", " }", " /* else: wasnew == 0, i.e., old state */", "#endif", " }", "#endif", "#endif", "#if NCORE>1", " Lstate = (struct H_el *) tmp;", "#endif", "#ifdef FULLSTACK", "#ifndef SAFETY", /* or else wasnew == 0 */ " if (wasnew)", " { Lstate = (struct H_el *) tmp;", " tmp->tagged |= V_A;", " if ((now._a_t&1)", " && (tmp->tagged&A_V)", " && depth > A_depth)", " {", "intersect:", "#ifdef CHECK", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"1st dfs-stack intersected on state %%d+\\n\",", " (int) tmp->st_id);", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", "#endif", " return 3;", " }", "#ifdef CHECK", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", "#endif", " return 0;", " } else", "#endif", " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)", " { Lstate = (struct H_el *) tmp;", "#ifndef SAFETY", " /* already on current dfs stack */", " /* but may also be on 1st dfs stack */", " if ((now._a_t&1)", " && (tmp->tagged&A_V)", " && depth > A_depth", /* new (Zhang's example) */ "#ifndef NOFAIR", " && (!fairness || now._cnt[1] <= 1)", "#endif", " )", " goto intersect;", "#endif", "#ifdef CHECK", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"\tStack state %%d\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", "#endif", " return 2; /* match on stack */", " }", "#else", " if (wasnew)", " {", "#ifdef CHECK", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(1, (char *)&(tmp->state), n, 0);", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", "#endif", " return 0;", " }", "#endif", "#ifdef CHECK", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(0, (char *)&(tmp->state), n, 0);", "#endif", "#if defined(BCS)", " #ifdef CONSERVATIVE", " if (tmp->ctx_low > trpt->sched_limit)", " { tmp->ctx_low = trpt->sched_limit;", " tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%8); /* new */", " #ifdef CHECK", " #if NCORE>1", " printf(\"cpu%%d: \", core_id);", " #endif", " printf(\"\t\tRevisit with fewer context switches\\n\");", " #endif", " nstates--;", " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", " return 0;", " } else if ((tmp->ctx_low == trpt->sched_limit", " && (tmp->ctx_pid[(now._last)/8] & ( 1 << ((now._last)%8) )) == 0 ))", " { tmp->ctx_pid[(now._last)/8] |= 1 << ((now._last)%8); /* add */", " #ifdef CHECK", " #if NCORE>1", " printf(\"cpu%%d: \", core_id);", " #endif", " printf(\"\t\tRevisit with same nr of context switches\\n\");", " #endif", " nstates--;", " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", " return 0;", " }", " #endif", "#endif", "#ifdef REACH", " if (tmp->D > depth)", " { tmp->D = depth;", " #ifdef CHECK", " #if NCORE>1", " printf(\"cpu%%d: \", core_id);", " #endif", " printf(\"\t\tReVisiting (from smaller depth)\\n\");", " #endif", " nstates--;", " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", #if 0 a possible variation of iterative search for shortest counter-example (pan -i and pan -I) suggested by Pierre Moro (for safety properties): state revisits on shorter depths do not start until after the first counter-example is found. this assumes that the max search depth is set large enough that a first (possibly long) counter-example can be found if set too short, this variant can miss the counter-example, even if it would otherwise be shorter than the depth-limit. (p.m. unsure if this preserves the guarantee of finding the shortest counter-example - so not enabled by default) " if (errors > 0 && iterative)", /* Moro */ #endif " return 0;", " }", "#endif", "#if (defined(BFS) && defined(Q_PROVISO)) || NCORE>1", " Lstate = (struct H_el *) tmp;", "#endif", "#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", "#endif", " return 1; /* match outside stack */", " } else if (m < 0)", " { /* insert state before tmp */", " ntmp = grab_state(n);", "#if NCORE>1", " if (!ntmp)", " {", " #if !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", " return 1; /* allow normal termination */", " }", "#endif", " ntmp->nxt = tmp;", " if (!olst)", " H_tab[j1_spin] = ntmp;", " else", " olst->nxt = ntmp;", " tmp = ntmp;", " break;", " } else if (!tmp->nxt)", " { /* append after tmp */", "#ifdef COLLAPSE", "Append:", "#endif", " tmp->nxt = grab_state(n);", "#if NCORE>1", " if (!tmp->nxt)", " {", " #if !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", " return 1; /* allow normal termination */", " }", "#endif", " tmp = tmp->nxt;", " break;", " } }", " }", "#ifdef CHECK", " tmp->st_id = (unsigned) nstates;", "#if NCORE>1", " printf(\"cpu%%d: \", core_id);", "#endif", "#ifdef BITSTATE", " printf(\" Push state %%d\\n\", ((int) nstates) - 1);", "#else", " printf(\" New state %%d\\n\", (int) nstates);", "#endif", "#endif", "#if defined(BCS)", " tmp->ctx_low = trpt->sched_limit;", " #ifdef CONSERVATIVE", " tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%8); /* new limit */", " #endif", "#endif", "#if !defined(SAFETY) || defined(REACH)", " tmp->D = depth;", "#endif", "#ifndef SAFETY", "#ifndef NOCOMP", " if (S_A)", " { v[0] = V_A;", "#ifndef NOFAIR", " if (S_A > NFAIR)", " { unsigned ci, bp; /* as above */", " ci = (now._cnt[now._a_t&1] / 8);", " bp = (now._cnt[now._a_t&1] - 8*ci);", " if (now._a_t&1)", " { ci = (NFAIR - 1) - ci;", " bp = 7 - bp; /* bp = 0..7 */", " }", " v[1+ci] = 1 << bp;", " }", "#endif", " }", "#endif", "#endif", "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", " tmp->m_K1 = K1;", "#endif", " memcpy(((char *)&(tmp->state)), v, n);", "#ifdef FULLSTACK", " tmp->tagged = (S_A)?V_A:(depth+1);", "#ifdef DEBUG", " dumpstate(-1, v, n, tmp->tagged);", "#endif", " Lstate = (struct H_el *) tmp;", "#else", " #ifdef DEBUG", " dumpstate(-1, v, n, 0);", " #endif", " #if NCORE>1", " Lstate = (struct H_el *) tmp;", " #endif", "#endif", "/* #if NCORE>1 && !defined(SEP_STATE) */", "#if NCORE>1", " #ifdef V_PROVISO", " tmp->cpu_id = core_id;", " #endif", " #if !defined(SEP_STATE) && !defined(BITSTATE)", " leave_critical(CS_ID);", " #endif", "#endif", " return 0;", "}", "#endif", "#include TRANSITIONS", 0, };