ref: 7a503757b1251c2746df7bdcd891814c1518cc28
dir: /sys/src/cmd/spin/pangen1.h/
/***** spin: pangen1.h *****/ /* * This file is part of the public release of Spin. It is subject to the * terms in the LICENSE file that is included in this source directory. * Tool documentation is available at http://spinroot.com */ static const 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", "#ifdef BFS_PAR", " bfs_setup_mem();", " #ifdef COLLAPSE", " /* this must be the very first allocation from the shared heap */", " #ifdef BFS_SEP_HASH", " ncomps = (ulong *) emalloc((ulong)((256+2) * sizeof(ulong)));", " #else", " ncomps = (ulong *) sh_pre_malloc((ulong)((256+2) * sizeof(ulong)));", " #endif", " #endif", "#endif", " iniglobals(258); /* arg outside range of pids */", "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP) && !defined(BFS) && !defined(HAS_LTL)", " 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", " sinit();", "#else", " 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,1); /* pid = 0, priority 1 */", " #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])", /* last entry is 0 */ " { 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(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_PRIORITY", "extern int highest_priority(int, short, Trans *);", "extern int get_priority(int);", "extern int set_priority(int, int);", "#endif", "#ifdef SPIN_HEAP", "void *", "spin_malloc(int n) /* reserved for use by Modex generated models */", "{ char *spin_heap_ptr = &(now.spin_heap[now.spin_heap_n]);", " if (now.spin_heap_n + n >= sizeof(now.spin_heap))", " { Uerror(\"spin_heap limit reached\");", " }", " now.spin_heap_n += n;", " return spin_heap_ptr;", "}", "void", "spin_free(void *unused)", "{ unused; /* ignore */", "}", "#endif", "int", "spin_join(int p, void **unused)", "{ /* fprintf(stderr, \"join %%d when %%d\\n \", p, now._nr_pr); */", " return (now._nr_pr <= p); /* process *p has stopped */", "}", "", "int", "spin_mutex_free(int *m)", "{ return (*m == 0);", "}", "", "int", "spin_mutex_lock(int *m)", "{ *m = 1;", " return 1;", "}", "void", "spin_mutex_destroy(int *m)", "{ *m = 0;", "}", "void", "spin_mutex_unlock(int *m)", "{ *m = 0;", "}", "void", "spin_mutex_init(int *m, void *val)", "{", " if (!val)", /* the 2nd arg must be NULL, for now */ " { *m = 0;", " } else", " { Uerror(\"pthread_mutex_init: unsupported non-default init\");", " }", "}", "", "int", "spin_cond_wait(int *cond, int *lck)", /*release and re-acquire lock *lck */ "{ /* this version does not scale very far alas */", " if (((P0 *)this)->_pid + 1 >= WS*8)", /* 32 or 64 */ " { Uerror(\"pid exceeds range supported by pthread_cond_wait\");", " }", " if (((*cond)&1) == 0)", /* repeatedly tested, so: */ " { spin_mutex_unlock(lck);", /* avoid double counting */ " *cond |= (1<<(((P0 *)this)->_pid + 1));", " return 0;", /* blocked, must test again */ " } else", " { /* if other processes are already waiting */", " /* while our wait flag is 0, then they should go first */", " if (((*cond)&(~(1 | (1<<(((P0 *)this)->_pid + 1))))) != 0)", " { spin_mutex_unlock(lck);", " return 0;", /* wait for the others to go first */ " }", " *cond &= ~1;", /* clear the 'go' bit andy wait flag */ " *cond &= ~(1<<(((P0 *)this)->_pid + 1));", " return 1;", /* okay to proceed */ " }", "}", "void", "spin_cond_signal(int *cond)", "{", " if ( ((*cond)&(~1)) != 0 )", /* procs are waiting */ " { *cond |= 1;", /* set the 'go' bit */ " }", "}", "", "#ifdef HAS_PROVIDED", " int provided(int, uchar, int, Trans *);", "#endif", "#ifdef BFS_PAR", " extern void bfs_shutdown(const char *);", "#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", "", " #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", " #define enter_critical(w) /* none */", " #define leave_critical(w) /* none */", "", " 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(long 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 NCORE>1", "extern void cleanup_shm(int);", "volatile uint *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(int);", "#ifdef BFS_PAR", " extern void bfs_mark_done(int);", " extern void bfs_drop_shared_memory(void);", "#endif", " 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", "#ifdef BFS_PAR", " if (who_am_i != 0)", " { bfs_mark_done(3); /* stopped */", " }", " bfs_drop_shared_memory();", "#endif", " if (val == 2)", " { val = 0;", " }", "#ifdef BFS_PAR", " if (who_am_i == 0)", "#endif", " stop_timer(1);", "", "#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);", "#ifdef PERMUTED", "void set_permuted(int);", "void set_reversed(int);", "void set_rotated(int);", "void set_randrot(int);", "void (*p_reorder)(int) = set_permuted;", "short p_rotate;", "#endif", "", "void", "getrail(void)", "{ FILE *fd;", " char *q, *pnm;", " int i, t_id, lastnever = -1; short II;", " Trans *t;", " P0 *z;", "#ifdef PERMUTED", " char sbuf[128];", " memset(sbuf, 0, sizeof(sbuf));", "#endif", " fd = findtrail(); /* exits if unsuccessful */", " while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)", " { if (depth == -1)", " { printf(\"<<<<<START OF CYCLE>>>>>\\n\");", " }", "#ifdef PERMUTED", " if (depth < 0)", " { switch (depth) {", " case -5:", " if (i && !t_reverse)", " { strcat(sbuf, \"-t_reverse \");", " }", " break;", " case -6:", " if (i && p_reorder != set_permuted)", " { strcat(sbuf, \"-p_permute \");", " } else", " if (t_id && p_reorder != set_reversed)", " { strcat(sbuf, \"-p_reverse \");", " }", " break;", " case -7:", " if (i", " && (p_reorder != set_rotated || p_rotate != t_id))", " { char tmp[32];", " sprintf(tmp, \"-p_rotate%%d \", t_id);", " strcat(sbuf, tmp);", " }", " break;", " case -8:", " if (i && p_reorder != set_randrot)", " { strcat(sbuf, \"-p_randrot \");", " }", " if (s_rand != ++t_id)", " { char tmp[32];", " sprintf(tmp, \"-RS%%u \", (uint) t_id-1);", " strcat(sbuf, tmp);", " }", " break;", " default:", " continue;", " }", " }", "#endif", " if (depth < 0)", " { continue;", " }", "#ifdef PERMUTED", " if (strlen(sbuf) > 0)", " { fprintf(efd, \"add: %%s\\n\", sbuf);", " exit(1);", " }", "#endif", " 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\';", " pnm = procname[z->_t];", " this = pptr(II);", " trpt->tau |= 1;", /* timeout always possible */ " if (!do_transit(t, II))", " { if (onlyproc >= 0 && II != onlyproc)", " goto moveon;", " if (!verbose) break;", " 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, pnm);", " 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):\", pnm, II);", " printf(\"[%%s]\\n\", q?q:\"\");", " } else if (!silent)", " { if (strlen(simvals) > 0) {", " printf(\"%%3ld: proc %%2d (%%s)\", ", " depth, II, pnm);", " 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, pnm);", " 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 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 */", "{ ulong x, y;", " uint i = 1;", "#if defined(MURMUR) && (WS==8)", " m_hash((uchar *) v, n); /* bstore_mod - sets j3_spin, j4_spin, K1, K2 */", "#else", " d_hash((uchar *) v, n); /* bstore_mod - sets j3_spin, j4_spin, K1, K2 */", "#endif", " x = K1; y = j3_spin;", /* was K2 before 5.1.1 */ " for (;;)", " { if (!(SS[x%%udmem]&(1<<y))) break;", /* take the hit in speed */ " if (i == hfns) {", "#ifdef DEBUG", " printf(\"Old bitstate\\n\");", "#endif", " return 1;", " }", " x = (x + K2 + i);", /* no mask, using mod - was K1 before 5.1.1 */ " y = (y + j4_spin) & 7;", " i++;", " }", "#ifdef RANDSTOR", " if (rand()%%100 > RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x%%udmem] |= (1<<y);", " if (i == hfns) break;", /* done */ " x = (x + K2 + i);", /* no mask - was K1 before 5.1.1 */ " y = (y + j4_spin) & 7;", " i++;", " }", "#ifdef DEBUG", " printf(\"New bitstate\\n\");", "#endif", " if (now._a_t&1)", " { nShadow++;", " }", " return 0;", "}", "int", "bstore_reg(char *v, int n) /* extended hashing, Peter Dillinger, 2004 */", "{ ulong x, y;", " uint i = 1;", "#if defined(MURMUR) && (WS==8)", " m_hash((uchar *) v, n); /* bstore_reg - sets j1_spin-j4_spin */", "#else", " d_hash((uchar *) v, n); /* bstore_reg - sets j1_spin-j4_spin */", "#endif", " x = j2_spin; y = j3_spin;", " for (;;)", " { if (!(SS[x]&(1<<y))) break;", /* at least one bit not set */ " if (i == hfns) {", "#ifdef DEBUG", " printf(\"Old bitstate\\n\");", "#endif", " return 1;", " }", " x = (x + j1_spin + i) & nmask;", " y = (y + j4_spin) & 7;", " i++;", " }", "#ifdef RANDSTOR", " if (rand()%%100 > RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x] |= (1<<y);", " if (i == hfns) break;", /* done */ " x = (x + j1_spin + i) & nmask;", " y = (y + j4_spin) & 7;", " i++;", " }", "#ifdef DEBUG", " printf(\"New bitstate\\n\");", "#endif", " if (now._a_t&1)", " { nShadow++;", " }", " return 0;", "}", "#endif", /* BITSTATE */ "ulong TMODE = 0666; /* file permission bits for trail files */", "", "int trcnt=1;", "char snap[64], fnm[512];", "", "int", "make_trail(void)", "{ int fd;", " char *q;", " char MyFile[512];", " int w_flags = O_CREAT|O_WRONLY|O_TRUNC;", "", " if (exclusive == 1 && iterative == 0)", " { w_flags |= O_EXCL;", " }", "", " q = strrchr(TrailFile, \'/\');", " if (q == NULL) q = TrailFile; else q++;", " strcpy(MyFile, q); /* TrailFile is not a writable string */", "", " if (iterative == 0 && Nr_Trails++ > 0)", " {", "#ifdef PUTPID", " sprintf(fnm, \"%%s_%%s_%%d_%%d.%%s\",", " MyFile, progname, getpid(), Nr_Trails-1, tprefix);", "#else", " sprintf(fnm, \"%%s%%d.%%s\",", " MyFile, Nr_Trails-1, tprefix);", "#endif", " } 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;", " if (BASE > 0 && h > 0)", " { ((P0 *)pptr(i))->_pid -= BASE;", " }", "#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 */ " #ifndef BFS_PAR", " BFS_State *bfs_trail, *bfs_bot, *bfs_free;", " SV_Hold *svfree;", " #else", " static ulong bfs_pre_allocated;", " #endif", " #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)", " #define RWFLAGS (O_RDWR|O_BINARY)", " #else", " #define RFLAGS (O_RDONLY)", " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)", " #define RWFLAGS (O_RDWR)", " #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);", "#if 0", "void", "select_claim(int x) /* ignored in BFS mode */", "{ if (verbose)", " { printf(\"select %%d (ignored)\\n\", x);", " }", "}", "#endif", "Trail *ntrpt;", "", "#ifndef BFS_PAR", "SV_Hold *", "getsv(int n)", "{ SV_Hold *h;", "", " if (svfree && n <= svfree->sz)", " { h = svfree;", " svfree = h->nxt;", " h->nxt = (SV_Hold *) 0;", " } else", " { 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", "#if !defined(NOCOMP) && !defined(HC)", " && (memcmp((char *) Mask, (char *) h->sv, n) == 0)", "#endif", " && (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));", "#if !defined(NOCOMP) && !defined(HC)", " memcpy((char *) h->sv, (char *) Mask, n);", "#endif", " #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 (p->sz >= h->sz)", " break;", " }", " if (!oh)", " { p->nxt = svfree;", " svfree = p;", " } else", " { p->nxt = h;", " oh->nxt = p;", " }", "}", "", "BFS_State *", "get_bfs_frame(void)", "{ BFS_State *t;", "", " if (bfs_free)", " { t = bfs_free;", " bfs_free = bfs_free->nxt;", " t->nxt = (BFS_State *) 0;", " } else", " { t = (BFS_State *) emalloc(sizeof(BFS_State));", " }", " 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_State *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; /* bfs */", " #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", " #ifdef VERBOSE", " printf(\"PUSH %%lu (depth %%d, nr %%lu)\\n\", (ulong) t->frame, d, t->nr);", " #else", " printf(\"PUSH %%lu (depth %%d)\\n\", (ulong) t->frame, d);", " #endif", " #endif", "}", "", "Trail *", "pop_bfs(void)", "{ BFS_State *t;", "", " if (!bfs_trail)", " { return (Trail *) 0;", " }", " t = bfs_trail;", " bfs_trail = t->nxt;", " if (!bfs_trail)", " { bfs_bot = (BFS_State *) 0;", " }", " #if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)", " if (t->lstate) /* bfs */", " { t->lstate->tagged = 0; /* bfs */", " }", " #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);", " #ifndef NOVSZ", " vsize = now._vsz;", " #endif", " }", "#if !defined(NOCOMP) && !defined(HC)", " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);", "#endif", " #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", " #ifdef VERBOSE", " printf(\"POP %%lu (depth %%d, nr %%lu)\\n\", (ulong) t->frame, t->frame->o_tt, t->nr);", " #else", " printf(\"POP %%lu (depth %%d)\\n\", (ulong) t->frame, t->frame->o_tt);", " #endif", " #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 (!b_store((char *)&now, vsize))", " #elif defined(MA)", " if (!g_store((char *)&now, vsize, 0))", " #else", " if (!h_store((char *)&now, vsize))", " #endif", " { static long sdone = (long) 0; long ndone;", " nstates++;", " #ifndef NOREDUCE", " trpt->tau |= 64;", /* bfs: succ definitely outside stack */ " #endif", " ndone = (ulong) (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(Q_PROVISO) && !defined(NOREDUCE) && defined(FULLSTACK)", " #if !defined(BITSTATE)", " if (Lstate && Lstate->tagged)", " { trpt->tau |= 64;", " }", " #else", " if (trpt->tau&32)", " { BFS_State *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", "}", "", "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 = (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_PRIORITY", " if (!highest_priority(((P0 *)this)->_pid, II, t))", " { continue;", " }", " #else", " #ifdef HAS_PROVIDED", " if (!provided(II, ot, tt, t))", " { continue;", " }", " #endif", " #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 = (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", " enter_critical(GLOBAL_LOCK); /* verbose mode */", " #if NCORE>1", " printf(\"cpu%%d: \", core_id);", " #endif", " printf(\"%%3lu: proc %%d \", depth, II);", " printf(\"reverses %%d, %%d to %%d,\",", " t->forw, tt, t->st);", " printf(\" %%s [abit=%%d,adepth=%%ld,\",", " t->tp, now._a_t, A_depth);", " printf(\"tau=%%d,%%d]\\n\",", " trpt->tau, (trpt-1)->tau);", " leave_critical(GLOBAL_LOCK);", " #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(\"%%ld: timeout\\n\", depth);", " #endif", " goto MainLoop;", " }", " #ifndef VERI", " if (!noends && !a_cycles && !endstate())", " { uerror(\"invalid end state\");", " }", " #endif", " } }", "}", "#endif", /* !BFS_PAR */ "", "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", "n_ewrite(int fd, char *s, int n)", "{ if (write(fd, s, strlen(s)) != strlen(s))", " { printf(\"pan: error writing %%s\\n\", fnm);", " pan_exit(1);", " }", "}", "", "void", "nuerror(void)", "{ int fd = make_trail();", " int j;", "", " if (fd < 0) return;", " #ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);", " n_ewrite(fd, snap, strlen(snap));", " #endif", " #ifdef MERGED", " sprintf(snap, \"-4:-4:-4\\n\");", " n_ewrite(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);", " n_ewrite(fd, snap, j);", " }", " close(fd);", " if (errors >= upto && upto != 0)", " { wrapup();", " }", "}", "#endif", /* BFS */ 0, }; static const char *Code2d[] = { "clock_t start_time;", "#if NCORE>1", "clock_t crash_stamp;", "#endif", "#if !defined(WIN32) && !defined(WIN64)", "struct tms start_tm;", "#endif", "", "#if SYNC", "extern int q_zero(int);", "extern int not_RV(int);", "#endif", "", "void", "start_timer(void)", "{", "#if defined(WIN32) || defined(WIN64)", " start_time = clock();", "#else", " start_time = times(&start_tm);", "#endif", "}", "", "double delta_time;", "", "void", "report_time(void)", "{", " 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));", " } }", "}", "", "void", "stop_timer(int report)", "{ clock_t stop_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", " if (report)", " { report_time();", " }", "#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", "", "#ifdef BFS_PAR", "int ncores = 0;", "#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;", " break;", " }", "#else", " if (!(trpt->o_pm&4)", " && progstate[ptr->_t][ptr->_p])", " { trpt->o_pm |= 4;", " break;", " }", "#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", "#if !defined(NOCOMP) && !defined(HC)", " 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", "#ifndef BFS_PAR", " start_timer();", "#endif", "#ifdef BFS", " #ifdef BFS_PAR", " bfs_main(ncores,0);", " #else", " bfs();", " #endif", "#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+HASH_NR);", /* do_the_search */ " #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 BACKWARD_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;", "", " pid += BASE;", " 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", "", "#ifdef HAS_PRIORITY", "int", "highest_priority(int pid, short nII, Trans *t)", "{ int i = pid; uchar *othis = this;", "", "#ifdef VERI", " if (nII == 0)", " { return 1;", /* never claim */ " }", "#endif", "#ifdef HAS_PROVIDED", " i = pid+BASE;", /* uncorrected process number */ "#endif", " if (i < 0", " || i >= (int) now._nr_pr", "#ifdef HAS_PROVIDED", " || !provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, t)", "#endif", " )", " { return 0;", " }", "", " for (i = BASE; i < now._nr_pr; i++)", /* all except never, if present */ " { this = pptr(i);", " if (i != pid+BASE", " && ((P0 *)this)->_priority > ((P0 *)pptr(pid+BASE))->_priority", "#ifdef HAS_PROVIDED", " && provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, 0)", "#endif", " && enabled(i+1, i-BASE))", /* enabled adds back BASE in 2nd arg */ " { this = othis;", " return 0;", " } }", " this = othis;", " return 1;", "}", "int", "get_priority(int pid)", "{ pid += BASE; /* 6.2.7 */", " if (pid < 0 || pid >= (int) now._nr_pr)", " return 0;", " return ((P0 *)pptr(pid))->_priority;", "}", "int", "set_priority(int pid, int pr)", "{ pid += BASE; /* 6.2.7 */", " if (pid < 0 || pid >= (int) now._nr_pr)", " {", " #ifdef VERBOSE", " printf(\"warning: bad pid %%d, no such process (set_priority)\\n\", pid);", " #endif", " return 1;", " }", " if (pr < 1 || pr > 255)", " { Uerror(\"priority is out of range\");", " }", " if (!TstOnly)", " { (trpt+1)->o_priority = ", " (((P0 *)pptr(pid))->_priority & 255) | (pid << 8);", " ((P0 *)pptr(pid))->_priority = pr;", " }", " return 1;", /* always executable */ "}", "#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)", "{", "#ifdef BFS_PAR", " e_critical(BFS_GLOB); /* bfs_par / snapshot */", " printf(\"cpu%%d: \", who_am_i);", "#endif", "#if NCORE>1", " enter_critical(GLOBAL_LOCK); /* ncore / 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= %%7lu \", nr_states);", "#endif", " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);", " snap_time();", " fflush(stdout);", "#if NCORE>1", " leave_critical(GLOBAL_LOCK);", "#endif", "#ifdef BFS_PAR", " x_critical(BFS_GLOB);", "#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", "", "#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]);", " } else", " { printf(\"pan: ltl formula %%s\\n\",", " procname[spin_c_typ[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", "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", "", "#ifdef P_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 CNT_P (1 + (To - From))", /* P_RAND start */ " #define NDONE_P (From <= To)", /* P_RAND continue */ " #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 CNT_P (1 + (From - To))", " #define NDONE_P (From >= To)", " #define ALL_P (II = From; II >= To; II--)", "#endif", "", "#ifdef PERMUTED", " #define CONTINUE0 { if (reversing&2) { II = oII; } continue; }", " #define CONTINUE { if (reversing&2) { p_reorder(seed); II = oII; } continue; }", "#else", " #define CONTINUE0 { continue; }", " #define CONTINUE { continue; }", "#endif", "#ifdef PERMUTED", "uchar _permutation_[256];", "void", "set_reversed(int unused)", "{ int i, n = now._nr_pr;", " #ifdef VERBOSE", " printf(\"%%ld: Set_reversed\\n\", depth);", " #endif", " #if defined(VERI) && !defined(NOCLAIM)", " for (i = 1; i < n; i++)", " { _permutation_[i] = n-i;", " }", " #else", " for (i = 0; i < n; i++)", " { _permutation_[i] = n-1-i;", " }", " #endif", "}", "void", "set_rotated(int unused)", "{ int i, n = now._nr_pr;", " #ifdef VERBOSE", " printf(\"%%ld: Set_rotated %%d\\n\", depth, p_rotate);", " #endif", " #if defined(VERI) && !defined(NOCLAIM)", " for (i = 1; i < n; i++)", " { _permutation_[i] = 1+(i-1+p_rotate)%%(n-1);", " }", " #else", " for (i = 0; i < n; i++)", " { _permutation_[i] = (i+p_rotate)%%n;", " }", " #endif", "}", "void", "set_randrot(int unused)", "{", " if (now._nr_pr > 1)", " { p_rotate = 1+rand()%%(now._nr_pr-1);", " } else", " { p_rotate = 0;", " }", " set_rotated(0);", "}", "void", "set_permuted(int T)", "{ /* permute nrs 1..n-1, leave 0 in place */", " int i, j, k, n = now._nr_pr;", " char tmp, *in = &(_permutation_[0]);", " #ifdef VERBOSE", " printf(\"%%ld: Set_permuted %%d\\n\", depth, T);", " #endif", " srand(T);", /* set_permuted */ " for (i = 0; i < n; i++)", " { in[i] = i;", " }", " if (n > 1)", " { for (i = 0; i < n; i++)", " {", " #if defined(VERI) && !defined(NOCLAIM)", " j = 1 + rand()%%(n-1);", " k = 1 + rand()%%(n-1);", " #else", " j = rand()%%(n);", " k = rand()%%(n);", " #endif", " tmp = in[j];", " in[j] = in[k];", " in[k] = tmp;", " } }", "}", "", " #ifdef VERBOSE", " short", " get_permuted(int x)", " { printf(\"%%ld: Get_permuted %%d -> %%d\\n\",", " depth, x, _permutation_[x]);", " return (short) _permutation_[x];", " }", " #else", " #define get_permuted(x) (short) _permutation_[x]", " #endif", "", "#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 PERMUTED", " short oII; uint seed;", "#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 %%ld: %%ld (maxdepth now %%ld)\\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", #if 0 we want to skip nrpr, nrqs, _a_t and cnt[NFAIR] (in the case of fairness) this is calculated in S_A, but S_A subtracts 2 bytes, because nrpr and nrqs are masked in the default state comparisons so we add those two bytes back here -- in default comparisons (h_store) we skip _a_t and cnt in the -- first comparison to find a match on the base-state -- the _a_t and cnt fields are then separately updated if there was -- a match on the base state #endif " if ((now._a_t&1) && depth > A_depth)", " { int delta = S_A + 2;", " if (!memcmp((char *)&A_Root + delta, ", " (char *)&now + delta, vsize - delta))", " {", "#ifndef NOFAIR", " if (fairness && now._cnt[1] != 1) /* was > 1 */", " {", " #ifdef CHECK", " printf(\"\tfairness count non-zero\\n\");", " #endif", " /* treat as new state */", " } else", "#endif", " { 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", " else", " {", " 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 = b_store((char *)&now, vsize);", " trpt->j6 = j1_spin; trpt->j7 = j2_spin;", " JJ = LL[j1_spin] && LL[j2_spin];", " if (II != 0) { break; }", " }", " now._ctx = 0; /* just in case */", " }", " #else", " II = b_store((char *)&now, vsize);", " trpt->j6 = j1_spin; trpt->j7 = j2_spin;", " JJ = LL[j1_spin] && LL[j2_spin];", " #endif", "#else", " #ifdef FULLSTACK", /* b_store 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 = b_store((char *)&now, vsize);", /* sets j1-j4 */ " if (II != 0) { break; }", " }", " now._ctx = 0;", " }", " #else", " JJ = onstack_now();", /* mangles j1 */ " II = b_store((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 = b_store((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 = b_store((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 = g_store((char *)&now, vsize, 0);", "#ifndef FULLSTACK", " JJ = II;", "#else", " JJ = (II == 2)?1:0;", "#endif", "#else", " II = h_store((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", /* with multicore we don't know which stack its on */ /* with HC there's a small chance of a false match - example fifoq 2012 */ "#if !defined(HC) && (NCORE==1 || defined (SEP_STATE))", " if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))", " #ifndef NOFAIR", " if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */", " #endif", " if (depth > A_depth) /* forum example by adl */", " {", " 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 > 1 */", " {", " #ifdef CHECK", " 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 = (ulong) (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((uchar *) &now, vsize); /* SHO - set K1 */", " HASH_NR = oh;", " }", " if (write(svfd, (uchar *) &K1, sizeof(ulong)) != sizeof(ulong))", " #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 ((ulong) 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\",", " (int) depth, now._a_t);", "#endif", " }", " #endif", " II = 0; /* never */", " goto Veri0;", " }", "#endif", "#ifdef PERMUTED", " if (reversing&2)", " { seed = rand();", " p_reorder(seed);", " }", "#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 {", /* PO preselect */ "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++;", " }", " 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;", " } else", " { continue;", " } } }", " 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", " trpt->p_left = CNT_P;", " 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", " for ALL_P {", /* Main Loop */ "#ifdef PERMUTED", " if (reversing&2)", " { oII = II;", " if (From != To)", /* not atomic or preselected */ " { II = get_permuted(II);", " } }", "#endif", "#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", " CONTINUE0;", " }", " 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)", " { CONTINUE0;", " }", "#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", " CONTINUE0;", /* 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", " CONTINUE0;", " }", " 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", " CONTINUE0; /* 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;", " }", " CONTINUE0; /* 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_PRIORITY", " if (!highest_priority(((P0 *)this)->_pid, II, t))", " { CONTINUE0;", " }", "#else", " #ifdef HAS_PROVIDED", " if (!provided(II, ot, tt, t))", " { CONTINUE0;", " }", " #endif", "#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 if (ooi > 0)", " { 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 PERMUTED", " if (reversing&2)", " { trpt->seed = seed;", " trpt->oII = oII;", " }", "#endif", "#if defined(T_RAND) && !defined(BFS)", " 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 %%ld: %%ld\\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", " { long 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 PERMUTED", " if (reversing&2)", " { seed = trpt->seed;", " oII = trpt->oII;", " }", "#endif", "#if defined(T_RAND) && !defined(BFS)", " ooi = trpt->oo_i;", "#endif", "#ifdef INLINE_REV", " _m = do_reverse(t, II, _m);", "#else", "#include BACKWARD_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=%%ld,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", " CONTINUE;", " } /* ALL_P */", "#ifdef NSUCC", " tally_succ(trpt->n_succ);", "#endif", "#ifdef P_RAND", " if (trpt->p_left > 0 && NDONE_P)", " { 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 ETIM", " && (trpt->tau&1) /* already tried timeout */", "#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; /* undo From == To */", " #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 restored and updated */", " { 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 updated */", " { 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()))", " || 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(\"%%ld: 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(\"%%ld: zapping\\n\", depth);", "#endif", " onstack_zap();", "#ifndef NOREDUCE", " if (trpt->proviso)", " g_store((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", "int do_hashgen = 0;", "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_PAR", " if (bfs_punt > 0)", " printf(\"%%9.8g states lost (lack of queue memory)\\n\", (double) bfs_punt);", "#endif", "#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);", " #if !defined(AUTO_RESIZE) && !defined(BFS_PAR)", " if (hcmp > (double) (1<<ssize))", " { printf(\"hint: increase hashtable-size (-w) to reduce runtime\\n\");", " }", " #endif", " #if defined(BFS_PAR) && defined(HC)", " { double fp = (100. * (double) nstates)/((double) ((ulong) (1<<ssize)));", " int fi = 0;", " printf(\"the hash table is %%3.3g %%%% filled\", fp);", " if (fp > 1.0)", " { fp = 100. / fp;", " while (fp > 2.) { fi++; fp /= 2.; }", " if (fi > 0)", " { printf(\" (hint: rerun with -w%%d to reduce runtime)\",", " ssize-fi);", " } }", " printf(\"\\n\");", " }", " #endif", " #endif", "#else", "#ifdef CHECK", " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);", "#endif", " if (udmem)", " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",", " (double)(((double) udmem) * 8.0) / (double) nstates);", " else", " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",", " ((double)(((ulong)1)<<(ssize-10)) / (double) nstates) * 1024.0);", /* the -10 and *1024 stuff is to avoid overflow */ " printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);", " if (do_hashgen)", " printf(\"hash polynomial used: 0x%%.8x\\n\", HASH_CONST[HASH_NR]);", " if (s_rand != 12345)", " printf(\"random seed used: %%u\\n\", (uint) (s_rand-1));", "#endif", "#if defined(BFS_DISK) && !defined(BFS_PAR)", " 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;", "#ifdef BFS_PAR", " if (who_am_i != 0)", " { pan_exit(0);", " }", "#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\");", "#if defined(BFS_PAR) && !defined(BITSTATE)", " if (bfs_punt > 0) printf(\"Warning: Search incomplete\\n\");", "#endif", "#ifdef SC", " (void) unlink((const char *)stackfile);", "#endif", "#ifdef BFS_PAR", " printf(\" + Multi-Core (using %%d cores)\\n\", Cores);", " #ifdef BFS_SEP_HASH", " printf(\" + Separate Hash Tables\\n\");", " #endif", " #ifdef BFS_DISK", " printf(\" + Disk storage\\n\");", " #endif", "#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(\" + Breadth-First Search\\n\");", "#endif", "#ifndef NOREDUCE", " printf(\" + Partial Order Reduction\\n\");", "#endif", "#ifdef PERMUTED", " printf(\" + Process Scheduling Permutation\\n\");", "#endif", "#ifdef P_REVERSE", " printf(\" + Reverse Depth-First Search Order\\n\");", "#endif", " if (t_reverse)", " printf(\" + Reverse Transition Ordering\\n\");", "#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 PERMUTED", " if (reversing & 2)", " { if (p_reorder == set_permuted)", " { printf(\" + Permuted\\n\");", " }", " if (p_reorder == set_reversed)", " { printf(\" + Reversed\\n\");", " }", " if (p_reorder == set_rotated)", " { printf(\" + Rotated %%d\\n\", p_rotate);", " }", " if (p_reorder == set_randrot)", " { printf(\" + RandRotated\\n\");", " } }", "#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", " #if !defined(BFS_PAR) || !defined(L_BOUND)", " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");", " #else", " printf(\"\tcycle checks \t+ (bound %%d)\\n\", L_bound);", " #endif", "#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(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<<ssize)*sizeof(H_el *);", "#endif", " #else", " if (udmem)", " nr3 = (double) (udmem);", " else", " nr3 = (double) (ONE_L<<(ssize-3));", "#ifdef CNTRSTACK", " nr5 = (double) (ONE_L<<(ssize-3));", "#endif", "#ifdef FULLSTACK", " nr5 = (double) (maxdepth*sizeof(H_el *));", "#endif", " #endif", " nr4 = (double) (svmax * (sizeof(Svtack) + hmax))", " + (double) (smax * (sizeof(_Stack) + Maxbody * sizeof(char)));", "#ifndef MA", " if (1 /* verbose || memcnt < nr1+nr2+nr3+nr4+nr5 */)", "#endif", " { double remainder = memcnt;", " double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;", "", " #if NCORE>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", " #ifndef USE_TDH", " printf(\"%%9.3f\tactual memory usage for states\",", " tmp_nr/1048576.);", " remainder -= tmp_nr;", " if (tmp_nr > 0.)", " { if (tmp_nr < nr1) ", " { printf(\" (compression: %%.2f%%%%)\\n\",", " (100.0*tmp_nr)/nr1);", " } else", " { printf(\"\\n\");", " }", " } else", " { printf(\" (less than 1k)\\n\");", " }", " #ifndef MA", " if (tmp_nr > 0. && tmp_nr < nr1)", " { printf(\" \tstate-vector as stored = %%.0f byte\",", " (tmp_nr)/(nstates-nShadow) -", " (double) (sizeof(H_el) - sizeof(unsigned)));", " printf(\" + %%ld byte overhead\\n\",", " (long int) sizeof(H_el)-sizeof(unsigned));", " }", " #endif", " #endif", " #if !defined(MA) || defined(COLLAPSE)", " #ifdef BFS_PAR", " printf(\"%%9.3f\tshared memory used for hash table (-w%%d)\\n\",", " ((double) bfs_pre_allocated)/1048576., ssize);", " #else", " printf(\"%%9.3f\tmemory used for hash table (-w%%d)\\n\",", " nr3/1048576., ssize);", " remainder -= nr3;", " #endif", " #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.);", " }", " #ifdef BFS_PAR", " printf(\"%%9.3f\ttotal non-shared memory usage\\n\\n\",", " memcnt/1048576.);", " #else", " printf(\"%%9.3f\ttotal actual memory usage\\n\\n\",", " memcnt/1048576.);", " #endif", " }", " #ifndef MA", " else", " #endif", "#endif", "#if !defined(BITSTATE) && defined(NOCOMP)", "jump_here:", "#endif", "#ifndef MA", " printf(\"%%9.3f\tmemory usage (Mbyte)\\n\",", " memcnt/1048576.);", "#endif", "#ifdef BFS_PAR", " bfs_report_mem();", "#else", " printf(\"\\n\");", "#endif", "#ifdef COLLAPSE", " printf(\"nr of templates: [ 0:globals 1:chans 2:procs ]\\n\");", " printf(\"collapse counts: [ \");", " { int i; for (i = 0; i < 256+2; i++)", " if (ncomps[i] != 0)", " printf(\"%%d:%%lu \", i, ncomps[i]);", " printf(\"]\\n\");", " }", "#endif", " #ifdef TRIX", " if (verbose)", " { 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", "#ifndef BFS_PAR", " pan_exit(0);", "#endif", "}\n", "void", "stopped(int arg)", "{", "#ifdef BFS_PAR", " bfs_shutdown(\"interrupted\");", "#endif", " printf(\"Interrupted\\n\");", "#if NCORE>1", " was_interrupted = 1;", "#endif", " wrapup();", " pan_exit(0);", "}", "", "/*", " * super fast hash, based on Paul Hsieh's function", " * http://www.azillionmonkeys.com/qed/hash.html", " */", "#include <stdint.h>", /* for uint32_t etc */ " #undef get16bits", " #if defined(__GNUC__) && defined(__i386__)", " #define get16bits(d) (*((const uint16_t *) (d)))", " #else", " #define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\", " +(uint32_t)(((const uint8_t *)(d))[0]) )", " #endif", "", "void", "d_sfh(uchar *s, int len)", /* sets one 32-bit number, in K1 */ "{ 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;", "}", "", "#if WS>4", "/* 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)", /* sets two 64-bit or 32-bit nrs, depending on WS */ "{ uint8_t *bp;", "#if WS>4", " uint64_t a = 0, b, c, n;", " const uint64_t *k = (uint64_t *) kb;", "#else", " uint32_t a = 0, b, c, n;", " const 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 WS>4", " 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 WS>4", " 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_spin = a&7; /* 1st bit */", " j2_spin = b&nmask; j4_spin = (a>>3)&7; /* 2nd bit */", " K1 = c; K2 = b;", "}", "", "#if defined(MURMUR) && (WS==8)", "/* public-domain, 64-bit MurmurHash3, by Austin Appleby */", "/* https://code.google.com/p/smhasher/wiki/MurmurHash3 */", "void", "m_hash(uchar *v, int len)", "{ uint8_t *bp, *data = (uint8_t*) v;", " int i, nblocks = len / 16;", "", " uint64_t h1 = HASH_CONST[HASH_NR];", " uint64_t h2 = 0x9e3779b97f4a7c13LL;", "", " uint64_t c1 = 0x87c37b91114253d5;", " uint64_t c2 = 0x4cf5ad432745937f;", "", " uint64_t *blocks = (uint64_t *)(data);", "", " /* guarantee a multiple of 16 bytes */", " i = 16 - (len %% 16);", " if (i > 0 && i < 16)", " { nblocks++;", " bp = v + len;", " switch (i) {", " case 15: *bp++ = 0; /* fall thru */", " case 14: *bp++ = 0;", " case 13: *bp++ = 0;", " case 12: *bp++ = 0;", " case 11: *bp++ = 0;", " case 10: *bp++ = 0;", " case 9: *bp++ = 0;", " case 8: *bp++ = 0;", " case 7: *bp++ = 0;", " case 6: *bp++ = 0;", " case 5: *bp++ = 0;", " case 4: *bp++ = 0;", " case 3: *bp++ = 0;", " case 2: *bp++ = 0;", " case 1: *bp = 0;", " case 0: break;", " } }", "", " for (i = 0; i < nblocks; i++)", " { uint64_t k1 = blocks[i*2];", " uint64_t k2 = blocks[i*2+1];", "", " k1 *= c1;", " k1 = (k1 << 31) | (k1 >> 33);", " k1 *= c2;", " h1 ^= k1;", "", " h1 = (h1 << 27) | (h1 >> 37);", " h1 += h2;", " h1 = h1 * 5 + 0x52dce729;", "", " k2 *= c2;", " k2 = (k2 << 33) | (k2 >> 31);", " k2 *= c1;", " h2 ^= k2;", "", " h2 = (h2 << 31) | (h2 >> 33);", " h2 += h1;", " h2 = h2 * 5 + 0x38495ab5;", " }", "", " uint8_t *tail = (uint8_t*)(data + (nblocks * 16));", "", " uint64_t k1 = 0;", " uint64_t k2 = 0;", "", " switch(len & 15) {", " case 15: k2 ^= ((uint64_t) tail[14]) << 48; break;", " case 14: k2 ^= ((uint64_t) tail[13]) << 40; break;", " case 13: k2 ^= ((uint64_t) tail[12]) << 32; break;", " case 12: k2 ^= ((uint64_t) tail[11]) << 24; break;", " case 11: k2 ^= ((uint64_t) tail[10]) << 16; break;", " case 10: k2 ^= ((uint64_t) tail[ 9]) << 8; break;", " case 9: k2 ^= ((uint64_t) tail[ 8]) << 0; break;", " k2 *= c2;", " k2 = (k2 << 33) | (k2 >> 31);", " k2 *= c1;", " h2 ^= k2; break;", " case 8: k1 ^= ((uint64_t) tail[7]) << 56; break;", " case 7: k1 ^= ((uint64_t) tail[6]) << 48; break;", " case 6: k1 ^= ((uint64_t) tail[5]) << 40; break;", " case 5: k1 ^= ((uint64_t) tail[4]) << 32; break;", " case 4: k1 ^= ((uint64_t) tail[3]) << 24; break;", " case 3: k1 ^= ((uint64_t) tail[2]) << 16; break;", " case 2: k1 ^= ((uint64_t) tail[1]) << 8; break;", " case 1: k1 ^= ((uint64_t) tail[0]) << 0; break;", " k1 *= c1;", " k1 = (k1 << 31) | (k1 >> 33);", " k1 *= c2;", " h1 ^= k1;", " };", "", " h1 ^= len; h2 ^= len;", " h1 += h2;", " h2 += h1;", " h1 ^= h1 >> 33;", " h1 *= 0xff51afd7ed558ccd;", " h1 ^= h1 >> 33;", " h1 *= 0xc4ceb9fe1a85ec53;", " h1 ^= h1 >> 33;", " h2 ^= h2 >> 33;", " h2 *= 0xff51afd7ed558ccd;", " h2 ^= h2 >> 33;", " h2 *= 0xc4ceb9fe1a85ec53;", " h2 ^= h2 >> 33;", " h1 += h2;", " h2 += h1;", "", " j1_spin = h1&nmask; j3_spin = (h1>>48)&7;", " j2_spin = h2&nmask; j4_spin = (h2>>48)&7;", " K1 = h1; K2 = h2;", "}", "#endif", "", "void", "s_hash(uchar *cp, int om)", /* uses either d_sfh (1x32bit), or d_hash (2x64bit) */ "{", /* depending on ssize ie the -w parameter */ " hasher(cp, om); /* sets K1 */", "#ifdef BITSTATE", " if (S_Tab == H_tab)", /* state stack in bitstate search */ " j1_spin = K1 %% omaxdepth;", " else", "#endif", " if (ssize < 8*WS)", " j1_spin = K1&mask;", " else", " j1_spin = K1;", "}", "#ifndef RANDSTOR", "int *prerand;", "void", "inirand(void)", "{ int i;", " srand(s_rand+HASH_NR);", /* inirand */ " 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)", "{", " 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<<ssize)-1); /* hash init */", "#ifdef BITSTATE", " nmask = mask>>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<<ssize)-1); /* hash init */", " nmask = (mask>>3);", " }", "}", "", "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)", "#if NCORE>1", " #error cannot combine AUTO_RESIZE with NCORE>1", "#endif", "static long reclaim_size;", "static char *reclaim_mem;", "static H_el **N_tab;", "void", "reverse_capture(H_el *p)", "{ if (!p) return;", " reverse_capture(p->nxt);", " /* last element of list moves first */", " /* to preserve list-order */", " j2_spin = p->m_K1;", " if (ssize < 8*WS) /* probably always true */", " { j2_spin &= mask;", " }", " p->nxt = N_tab[j2_spin];", " N_tab[j2_spin] = p;", "}", "void", "resize_hashtable(void)", "{", "#ifndef BFS_PAR", /* ssize and mask/nmask are not in shared mem */ " if (WS == 4 && ssize >= 27 - 1)", "#endif", " { return; /* cannot increase further */", " }", "", " ssize += 2; /* 4x size @htable ssize */", "", " printf(\"pan: resizing hashtable to -w%%d.. \", ssize);", "", " N_tab = (H_el **) emalloc((ONE_L<<ssize)*sizeof(H_el *));", " set_masks(); /* they changed */", "", " for (j1_spin = 0; j1_spin < (ONE_L << (ssize - 2)); j1_spin++)", " { reverse_capture(H_tab[j1_spin]);", " }", " reclaim_mem = (char *) H_tab;", " reclaim_size = (ONE_L << (ssize - 2));", " H_tab = N_tab;", "", " printf(\" done\\n\");", "}", "#endif", "#if defined(ZAPH) && defined(BITSTATE)", "void", "zap_hashtable(void)", "{ cpu_printf(\"pan: resetting hashtable\\n\");", " if (udmem)", " { memset(SS, 0, udmem);", " } else", " { memset(SS, 0, ONE_L<<(ssize-3));", " }", "}", "#endif", "", "#if NCLAIMS>1", "int", "find_claim(char *s)", "{ int i, j;", " for (i = 0; strncmp(procname[i], \":np_:\", 5) != 0; 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", "", "#if defined(BFS_PAR) && defined(BFS_SEP_HASH)", "int /* to avoid having to include <math.h> and compile with -lm */", "blog2(int n) /* n >= 1 */", "{ int m=1, r=2;", " if (n == 1) { return 0; }", " if (n == 2) { return 1; }", " while (n > r) { m++; r *= 2; }", " return m;", "}", "#endif", "", "uint pp[33];", "", "uint ", "mul(uint a, uint b, uint p)", "{ int c = 0;", " while (a)", " { if (a&1)", " { a ^= 1;", " c ^= b;", " }", " a = (a>>1);", " if (b & 0x80000000)", " { b += b;", " b ^= p;", " } else", " { b += b;", " } }", " return c;", "}", "", "uint", "ppow(int n, uint p)", "{ uint t = 1; int i;", " for (i = 0; i < 32; i++)", " { if (n & (1<<i))", " { t = mul(t, pp[i], p);", " } }", " return t;", "}", "", "void", "hashgen(void) /* courtesy Jim Reeds, 1995 */", "{ uint x, y, p; int i, cnt;", " int ff[5] = { 3, 5, 17, 257, 65537 };", " int nn[5];", "", " srand(s_rand); /* was: srandom(s_rand) */", " nn[0] = ff[1]*ff[2]*ff[3]*ff[4];", " nn[1] = ff[0]*ff[2]*ff[3]*ff[4];", " nn[2] = ff[0]*ff[1]*ff[3]*ff[4];", " nn[3] = ff[0]*ff[1]*ff[2]*ff[4];", " nn[4] = ff[0]*ff[1]*ff[2]*ff[3];", " for (cnt = 0; cnt < 5000; cnt++)", " { x = 2;", " p = ((rand()<<13)^rand()) | 1; /* used random() before */", " pp[0] = x;", " for (i = 0; i < 32; i++)", " { pp[i+1] = mul(pp[i], pp[i], p);", " }", " if (pp[32] == x)", " { for (i = 0; i < 5; i++)", " { y = ppow(nn[i], p);", " if (y == 1)", " { break;", " } }", " if (y != 1)", " { HASH_CONST[0] = p;", /* 32 bit */ " if (verbose)", " { printf(\"polynomial: 0x%%.8x (%%d tries)\\n\",", " p, cnt);", " }", " return;", /* success */ " } } }", " fprintf(efd, \"pan: could not find a polynomial in %%d tries\\n\", cnt);", " fprintf(efd, \"pan: try a different seed with -RSn\\n\");", " exit(1);", "}", "", "int", "main(int argc, char *argv[])", "{ void to_compile(void);\n", " efd = stderr; /* default */", "#if defined(BFS_PAR) && defined(BFS_SEP_HASH)", " uchar used_w = 0;", "#endif", " 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", "", "#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", " b_store = 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, \"warning: -a is disabled by -DNP, ignored\");", " break;", " #else", " case 'a': a_cycles = 1; break;", " #endif", "#else", " #if defined(BFS_PAR) && defined(L_BOUND)", " case 'a': if (isdigit(argv[1][2]))", " { L_bound = atoi(&argv[1][2]);", " if (L_bound < 1 || L_bound > 255)", " { printf(\"usage: -aN with 0<N<256\\n\");", " exit(1);", " } }", " break;", " #endif", "#endif", " case 'A': noasserts = 1; break;", " case 'b': bounded = 1; break;", "#ifdef HAS_CODE", " #if HAS_CODE>0", " case 'C': coltrace = 1; goto samething;", " #endif", "#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", " #if HAS_CODE>0", " case 'g': gui = 1; goto samething;", " #endif", "#endif", " case 'h':", " if (strncmp(&argv[1][1], \"hash\", strlen(\"hash\")) == 0)", " { do_hashgen = 1;", " break;", " }", " if (!argv[1][2] || !isdigit((int) argv[1][2]))", " { usage(efd); /* exits */", " }", " HASH_NR = atoi(&argv[1][2])%%(sizeof(HASH_CONST)/sizeof(uint));", " break;", " case 'I': iterative = 2; every_error = 1; break;", " case 'i':", " if (strncmp(&argv[1][1], \"i_reverse\", strlen(\"i_reverse\")) == 0)", " { reversing |= 1;", " } else", " { 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 not available (compile with -DNP)\");", " 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((int)argv[1][2]))", " { whichclaim = atoi(&argv[1][2]);", " } else if (isalpha((int)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((int)argv[1][2]) && argc > 2 && argv[2][0] != '-')", " { argc--; argv++;", " }", " #endif", "#endif", " break;\n", " case 'n': no_rck = 1; break;", "", " case 'P':", " if (!readtrail", " && isdigit((int) argv[1][2]))", /* was argv[1][2] == '_' */ " { int x = atoi(&argv[1][2]);", " if (x != 0 && x != 1)", " { fprintf(efd, \"pan: bad option -P[01], ignored\\n\");", " }", " if (x == 0)", " { reversing &= ~1;", " break;", " }", " if (x == 1)", " { reversing |= 1;", " break;", " }", " if (verbose)", " fprintf(efd, \"pan: reversed *active* process creation %%s\\n\",", " reversing&1?\"on\":\"off\");", " break;", " } /* else */", "#ifdef HAS_CODE", " #if HAS_CODE>0", " readtrail = 1; onlyproc = atoi(&argv[1][2]);", " if (argc > 2 && argv[2][0] != '-') /* check next arg */", " { trailfilename = argv[2];", " argc--; argv++; /* skip next arg */", " }", " #else", " fprintf(efd, \"pan: option -P not recognized, ignored\\n\");", " #endif", "#else", " fprintf(efd, \"pan: option -P not recognized, ignored\\n\");", "#endif", " break;", "", " case 'p':", " #if !defined(BFS) && !defined(BFS_PAR)", " #ifdef PERMUTED", " if (strncmp(&argv[1][1], \"p_normal\", strlen(\"p_normal\")) == 0)", " { reversing &= ~2;", " break;", " }", " reversing |=2;", " if (strncmp(&argv[1][1], \"p_permute\", strlen(\"p_permute\")) == 0)", " { p_reorder = set_permuted;", " break;", " }", " if (strncmp(&argv[1][1], \"p_rotate\", strlen(\"p_rotate\")) == 0)", " { p_reorder = set_rotated;", " if (isdigit((int) argv[1][9]))", " { p_rotate = atoi(&argv[1][9]);", " } else", " { p_rotate = 1;", " }", " break;", " }", " if (strncmp(&argv[1][1], \"p_randrot\", strlen(\"p_randrot\")) == 0)", " { p_reorder = set_randrot;", " break;", " }", " if (strncmp(&argv[1][1], \"p_reverse\", strlen(\"p_reverse\")) == 0)", " { p_reorder = set_reversed;", " break;", " }", " #else", " if (strncmp(&argv[1][1], \"p_permute\", strlen(\"p_permute\")) == 0", " || strncmp(&argv[1][1], \"p_rotate\", strlen(\"p_rotate\")) == 0", " || strncmp(&argv[1][1], \"p_randrot\", strlen(\"p_randrot\")) == 0", " || strncmp(&argv[1][1], \"p_reverse\", strlen(\"p_reverse\")) == 0)", " { fprintf(efd, \"option %%s required compilation with -DPERMUTED\\n\",", " argv[1]);", " exit(1);", " }", " #endif", " #endif", "#ifdef SVDUMP", " vprefix = atoi(&argv[1][2]);", "#else", " fprintf(efd, \"invalid option '%%s' -- ignored\\n\", argv[1]);", "#endif", " break;", "#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 (argv[1][2] == 'S') /* e.g., -RS76842 */", " { s_rand = atoi(&argv[1][3]);", /* RS */ " break;", " }", "#ifdef BITSTATE", " Nrun = atoi(&argv[1][2]);", " if (Nrun > 100)", " { Nrun = 100;", " } else if (Nrun < 1)", " { Nrun = 1;", " }", "#else", " usage(efd);", " break;", "#endif", " case 'r':", " if (strncmp(&argv[1][1], \"rhash\", strlen(\"rhash\")) == 0)", " { if (s_rand == 12345) /* default seed */", " {", "#if defined(WIN32) || defined(WIN64)", " s_rand = (uint) clock();", "#else", " struct tms dummy_tm;", " s_rand = (uint) times(&dummy_tm);", "#endif", " }", " srand(s_rand++);", " #ifdef PERMUTED", " do_hashgen = 1;", /* + randomize p_rotate, p_reverse, p_permute */ " switch (rand()%%5) {", " case 0: p_reorder = set_permuted;", " reversing |=2;", " break;", " case 1: p_reorder = set_reversed;", " reversing |=2;", " break;", " /* fully randomize p_rotate: */", " case 2: p_reorder = set_randrot;", " reversing |=2;", " break;", " /* choose once, then keep p_rotate fixed: */", " case 3: p_reorder = set_rotated;", " p_rotate = rand()%%3;", " reversing |=2;", " break;", " default: /* standard search */ break;", " }", " if (rand()%%2 == 0)", " { t_reverse = 1;", " }", " break;", " #else", " fprintf(efd, \"option -rhash requires compilation with -DPERMUTED\\n\");", " exit(1);", " #endif", " }", "#if defined(HAS_CODE) && HAS_CODE>0", "samething: readtrail = 1;", " if (isdigit((int)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;", "#else", " fprintf(efd, \"options -r is for models with embedded C code\\n\");", " break;", "#endif", " case 'T':", " if (isdigit((int) argv[1][2]))", /* was argv[1][2] == '_' */ " { t_reverse = atoi(&argv[1][2]);", " if (verbose)", " printf(\"pan: reverse transition ordering %%s\\n\",", " t_reverse?\"on\":\"off\");", " break;", " }", " TMODE = 0444;", " break;", " case 't':", " if (strncmp(&argv[1][1], \"t_reverse\", strlen(\"t_reverse\")) == 0)", " { t_reverse = 1;", " break;", " }", /* i.e., a trail prefix cannot be '_reverse' */ " if (argv[1][2])", " { tprefix = &argv[1][2];", " }", " break;", " case 'u':", " #ifdef BFS_PAR", " ncores = atoi(&argv[1][2]);", " #endif", " 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]);", " #if defined(BFS_PAR) && defined(BFS_SEP_HASH)", " used_w = 1;", " #endif", " 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 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 defined(BFS_PAR) && defined(BFS_SEP_HASH)", " if (used_w == 0)", " { if (ncores == 0) /* all cores used, by default */", " { ssize -= blog2(BFS_MAXPROCS - 1);", " } else", " { ssize -= blog2(ncores);", " } }", "#endif", " if (do_hashgen)", " { hashgen();", /* placed here so that -RSn can appear after -hash */ " }", "#ifndef SAFETY", " if (fairness && !a_cycles)", " { fprintf(efd, \"error: -f requires the use of -a or -l\\n\");", " usage(efd);", " }", " #if ACCEPT_LAB==0", " if (a_cycles)", " { fprintf(efd, \"warning: no accept labels are defined, \");", " fprintf(efd, \"so option -a has no effect (ignored)\\n\");", " a_cycles = 0;", " }", " #endif", "#endif", "", "#ifdef BFS_PAR", " uerror = bfs_uerror;", " Uerror = bfs_Uerror;", "#else", " uerror = dfs_uerror;", " Uerror = dfs_Uerror;", "#endif", " if (ssize <= 32) /* 6.2.0 */", " { hasher = d_sfh;", "#if !defined(BITSTATE) && defined(USE_TDH)", " o_hash = o_hash32;", "#endif", " } else", " { hasher = d_hash;", "#if !defined(BITSTATE) && defined(USE_TDH)", " o_hash = o_hash64;", "#endif", " }", " if (iterative && TMODE != 0666)", " { TMODE = 0666;", " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");", " }", "#if defined(WIN32) || defined(WIN64)", " #ifndef _S_IWRITE", " #define S_IWRITE 0000200 /* write permission, owner */", " #endif", " #ifndef _S_IREAD", " #define S_IREAD 0000400 /* read permission, owner */", " #endif", " 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", "#if defined(T_RAND) && defined(ELSE_IN_GUARD)", " #error cannot hide 'else' as guard in d_step, when using -DT_RAND", "#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 ulong", " */", " }", "#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", " #if defined(BFS_PAR) && defined(BFS_SEP_HEAP)", " #error cannot combined -DBFS_SEP_HEAP with -DTRIX", " #endif", "#endif", "#ifdef BFS_PAR", " #ifdef NP", " #error cannot combine -DBFS_PAR and -DNP", " #undef NP", " #endif", "#endif", "#ifdef NOCLAIM", " #ifdef NP", " #warning using -DNP overrides -DNOCLAIM", " #undef NOCLAIM", " #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", "#if defined(HC) && !defined(BFS_PAR)", " #ifdef NOCOMP", " #error cannot combine -DHC and -DNOCOMP", " #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 NOCOMP", " #error cannot combine -DCOLLAPSE and -DNOCOMP", " #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", "#if SYNC>0", " #ifdef HAS_PRIORITY", " #error use of priorities cannot be combined with rendezvous", " #elif HAS_ENABLED", " #error use of enabled() cannot be combined with rendezvous", " #endif", "#endif", "#ifndef NOREDUCE", " #ifdef HAS_PRIORITY", " #warning use of priorities requires -DNOREDUCE", " #elif 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)", " if (!noends)", " fprintf(efd, \"warning: use of rendezvous with BFS does not preserve all invalid endstates\\n\");", "#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 (verbose && !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 0", " 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\");", " }", " #endif", " #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();", "#if defined(BFS) || defined(BFS_PAR)", " 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", " trpt = &trail[0]; /* precaution -- in case uerror is called early */", "#ifdef BFS", " ntrpt = trpt;", "#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+HASH_NR);", /* main - RANDSTOR */ "#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:0..499 (defaults to -h0)\\n\");", " fprintf(fd, \"\t-hash generate a random hash-polynomial for -h0 (see also -rhash)\\n\");", " fprintf(fd, \"\t using a seed set with -RSn (default %%u)\\n\", s_rand);", " 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 PERMUTED", " fprintf(fd, \"\t-p_permute randomize order in which processes are scheduled (see also -rhash)\\n\");", " fprintf(fd, \"\t-p_reverse reverse order in which processes are scheduled (see also -rhash)\\n\");", " fprintf(fd, \"\t-p_rotateN rotate by N the process scheduling order (see also -rhash)\\n\");", "#endif", "#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-r trailfilename read and execute trail in file\\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-r -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", " fprintf(fd, \"\t-RSn use randomization seed n\\n\");", " fprintf(fd, \"\t-rhash use random hash-polynomial and randomly choose -p_rotateN, -p_permute, or p_reverse\\n\");", "#ifdef BITSTATE", " fprintf(fd, \"\t-Rn run n times n: [1..100] using n \");", " fprintf(fd, \" different hash functions\\n\");", "#endif", " fprintf(fd, \"\t-T create trail files in read-only mode\\n\");", " fprintf(fd, \"\t-t_reverse reverse order in which transitions are explored\\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(ulong 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)", " {", "#ifdef BFS_PAR", " Uerror(\"out of non-shared memory\");", "#endif", " 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(ulong 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 ((ulong) 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", "dfs_Uerror(char *str)", "{ /* always fatal */", " uerror(str);", "#if NCORE>1", " sudden_stop(\"Uerror\");", "#endif", "#ifdef BFS_PAR", " bfs_shutdown(\"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(\"%%ld State: \", depth);", "#if !defined(NOCOMP) && !defined(HC)", " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",", " ((char *)&now)[i], Mask[i]?\"*\":\"\");", "#else", " for (i = 0; i < vsize; i++)", " printf(\"%%d,\", ((char *)&now)[i]);", "#endif", " 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", " { long 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=%%ld,\", ", " t->tp, now._a_t, A_depth);", " printf(\"tau=%%d,%%d] <unwind>\\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", "dfs_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();", " 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)", " {", "#ifdef BFS_PAR", " bfs_shutdown(\"uerror\"); /* no return */", "#endif", "#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", "#ifdef PERMUTED", " sprintf(snap, \"-5:%%d:%%d\\n\", t_reverse, reversing&2);", " if (write(fd, snap, strlen(snap)) < 0) return;", "", " sprintf(snap, \"-6:%%d:%%d\\n\", p_reorder==set_permuted, p_reorder==set_reversed);", " if (write(fd, snap, strlen(snap)) < 0) return;", "", " sprintf(snap, \"-7:%%d:%%d\\n\", p_reorder==set_rotated, p_rotate);", " if (write(fd, snap, strlen(snap)) < 0) return;", "", " sprintf(snap, \"-8:%%d:%%d\\n\", p_reorder==set_randrot, --s_rand);", " 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", "}", "", "void", "p_restor(int h)", "{ int i;", " char *z = (char *) &now;\n", "", "#ifdef BFS_PAR", " bfs_prepmask(1); /* p_restor */", "#endif", "#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", " #if !defined(NOCOMP) && !defined(HC)", " 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;", " #if !defined(NOCOMP) && !defined(HC)", " 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;", " #ifdef BFS_PAR", " bfs_fixmask(1); /* p_restor */", " #endif", "#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", " #ifdef BFS_PAR", " bfs_prepmask(2); /* q_restor */", " #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 TRIX", " #if !defined(NOCOMP) && !defined(HC)", " 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", " #ifdef BFS_PAR", " bfs_fixmask(2); /* q_restor */", " #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];", " #if !defined(NOCOMP) && !defined(HC)", " #ifdef BFS_PAR", " bfs_prepmask(3); /* delproc - no chance in proc_offset or proc_skip */", " #endif", " for (i = vsize; i < o_vsize; i++)", " Mask[i] = 0; /* reset */", " #ifdef BFS_PAR", " bfs_fixmask(3); /* delproc */", " #endif", " #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];", " #if !defined(NOCOMP) && !defined(HC)", " #ifdef BFS_PAR", " bfs_prepmask(3); /* delq - no change in q_offset or q_skip */", " #endif", " for (k = vsize; k < o_vsize; k++)", " Mask[k] = 0; /* reset */", " #ifdef BFS_PAR", " bfs_fixmask(3); /* delq */", " #endif", " #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)", " if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)", " { printf(\"pan: event_trace not completed\\n\");", " return 0;", " }", "#endif", " return 1;", "}\n", "#if !defined(SAFETY) && !defined(BFS)", "void", "checkcycles(void)", "{ uchar o_a_t = now._a_t;", " #ifndef NOFAIR", " uchar o_cnt = now._cnt[1];", " #endif", " #ifdef FULLSTACK", " #ifndef MA", " 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 improve hashing */", " #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", "", "#if defined(FULLSTACK) && defined(BITSTATE)", "H_el *Free_list = (H_el *) 0;", "void", "onstack_init(void) /* to store stack states in a bitstate search */", "{ S_Tab = (H_el **) emalloc(maxdepth*sizeof(H_el *));", "}", "#endif", "#if !defined(BFS_PAR)", " #if defined(FULLSTACK) && defined(BITSTATE)", "H_el *", "grab_state(int n)", "{ 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 (H_el *) emalloc(sizeof(H_el)+n-sizeof(unsigned));", "}", " #else", /* !FULLSTACK || !BITSTATE */ "#if NCORE>1", "H_el *", "grab_state(int n)", "{ H_el *grab_shared(int);", " return grab_shared(sizeof(H_el)+n-sizeof(unsigned));", "}", "#else", /* ! NCORE>1 */ "#ifndef AUTO_RESIZE", " #define grab_state(n) (H_el *) \\", " emalloc(sizeof(H_el)+n-sizeof(ulong));", "#else", /* AUTO_RESIZE */ "H_el *", "grab_state(int n)", "{ H_el *p;", " int cnt = sizeof(H_el)+n-sizeof(ulong);", "#ifndef MA", " if (reclaim_size >= cnt+WS)", " { if ((cnt & (WS-1)) != 0) /* alignment */", " { cnt += WS - (cnt & (WS-1));", " }", " p = (H_el *) reclaim_mem;", " reclaim_mem += cnt;", " reclaim_size -= cnt;", " memset(p, 0, cnt);", " } else", "#endif", " { p = (H_el *) emalloc(cnt);", " }", " return p;", "}", "#endif", /* AUTO_RESIZE */ "#endif", /* NCORE>1 */ " #endif", /* FULLSTACK && !BITSTATE */ "#else", /* BFS_PAR */ " extern volatile uchar *sh_pre_malloc(ulong);", " extern volatile uchar *sh_malloc(ulong);", " H_el *", " grab_state(int n) /* bfs_par */", " { volatile uchar *rval = NULL;", " int m = sizeof(H_el) + n - sizeof(unsigned);", "", " if (n == 0) m = m/n;", " #ifdef BFS_SEP_HASH", " rval = emalloc((ulong) m);", " #else", " rval = sh_malloc((ulong) m);", " #endif", " memset((void *) rval, 0, (size_t) m);", "", " return (H_el *) rval;", " }", "#endif", /* BFS_PAR */ "#ifdef COLLAPSE", "ulong", "ordinal(char *v, long n, short tp)", "{ H_el *tmp, *ntmp; long m;", " H_el *olst = (H_el *) 0;", " s_hash((uchar *)v, n);", "#if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " e_critical(BFS_ID); /* bfs_par / collapse */", "#endif", "#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", "#ifdef BFS_PAR", " e_critical(BFS_ORD); /* bfs_par */", "#endif", " m = ++ncomps[tp];", "#ifdef BFS_PAR", " x_critical(BFS_ORD);", "#endif", "#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);", "#endif", "#if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", "#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;", " ulong 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(ulong);", "#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;", "", "#if !defined(NOCOMP) && !defined(HC)", " for (i = 0; i < (int) n; i++, w++)", " if (!Mask[j++]) *x++ = *w;", "#else", " memcpy(x, w, n); x += n;", "#endif", "", "#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", /* !COLLAPSE */ "#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;", " }", " n = i = v - (char *)&comp_now; /* bytes written so far */", " 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", /* COLLAPSE */ "#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)", "{ H_el *v, *w, *last = 0;", " 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 = (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;", "}", "", "#ifndef BFS_PAR", " void", " onstack_put(void)", " { 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 (h_store((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)", " { H_el *tmp;", " 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 = (H_el *) tmp; /* onstack_now */", " break;", " } }", " PROBE++;", " #if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)", " now._last = was_last;", " #endif", " return (m == 0);", " }", "#endif", /* !BFS_PAR */ "#endif", /* !MA */ "#endif", /* FULLSTACK && BITSTATE */ "#ifdef BITSTATE", "void init_SS(ulong);", "", "void", "sinit(void)", "{", " if (udmem)", " { udmem *= 1024L*1024L;", " #if NCORE>1", " if (!readtrail)", " { init_SS((ulong) udmem);", " } else", " #endif", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " SS = (uchar *) sh_pre_malloc((ulong) udmem);", " #else", " SS = (uchar *) emalloc(udmem);", " #endif", " b_store = bstore_mod;", " } else", " {", " #if NCORE>1", " init_SS(ONE_L<<(ssize-3));", " #else", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " SS = (uchar *) sh_pre_malloc((ulong)(ONE_L<<(ssize-3)));", " #else", " SS = (uchar *) emalloc(ONE_L<<(ssize-3));", " #endif", " #endif", " }", "}", "#else", " #if !defined(MA) || defined(COLLAPSE)", " void", " set_H_tab(void)", " {", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " H_tab = (H_el **) sh_pre_malloc((ulong)((ONE_L<<ssize)*sizeof(H_el *)));", " #else", " H_tab = (H_el **) emalloc((ONE_L<<ssize)*sizeof(H_el *));", " #endif", " }", " #endif", "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(ulong);", " init_HT(0L);", " }", " #endif", " #endif", " #endif", " #if !defined(MA) || defined(COLLAPSE)", " #if NCORE>1 || (defined(BFS_PAR) && defined(USE_TDH) && !defined(WIN32) && !defined(WIN64))", " if (!readtrail)", " { void init_HT(ulong);", " init_HT((ulong) (ONE_L<<ssize)*sizeof(H_el *));", " #if defined(TRIX) || (defined(BFS_PAR) && defined(COLLAPSE))", " set_H_tab(); /* need both */", " #endif", " } else", " #endif", " { set_H_tab(); /* @htable ssize */", " }", " #endif", /* !defined(MA) || defined(COLLAPSE) */ "}", "#endif\n", "#if !defined(BITSTATE) || defined(FULLSTACK)", "#ifdef DEBUG", "void", "dumpstate(int wasnew, char *v, int n, int tag)", "{ int i;", "#ifndef SAFETY", " if (S_A)", " { printf(\"\tstate tags %%d (%%d::%%d): \",", " V_A, wasnew, v[0]);", "#ifdef FULLSTACK", " printf(\" %%d \", tag);", "#endif", " printf(\"\\n\");", " }", "#endif", "#ifdef SDUMP", " printf(\"\t State: \");", "#if !defined(NOCOMP) && !defined(HC)", " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",", " ((char *)&now)[i], Mask[i]?\"*\":\"\");", "#else", " for (i = 0; i < vsize; i++)", " printf(\"%%d,\", ((char *)&now)[i]);", "#endif", " printf(\"\\n\tVector: \");", " for (i = 0; i < n; i++)", " printf(\"%%d,\", v[i]);", " printf(\"\\n\");", "#endif", "}", "#endif", "#ifdef MA", "int", "g_store(char *vin, int nin, uchar pbit)", "{ int n, i;", " int ret_val = 1;", " uchar *v;", " static uchar Info[MA+1];", "#ifndef NOCOMP", " n = compress(vin, nin);", " v = (uchar *) &comp_now;", "#else", " n = nin;", " v = (uchar *) vin;", "#endif", " if (n >= 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 = (uint) 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;", " }", "", "#ifdef BFS_PAR", " e_critical(BFS_STATE); /* bfs_par / g_store */", "#endif", "#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:", "#ifdef BFS_PAR", " x_critical(BFS_STATE);", "#endif", "#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)", " { 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", " { H_el *ntmp, *olst = (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 (verbose)", " { 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;", " if (BASE > 0 && i > 0)", " { ((P0 *)pptr(i))->_pid -= BASE;", " } }", "#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", "#if !defined(BFS_PAR) || (!defined(BITSTATE) && !defined(USE_TDH))", "int", "h_store(char *vin, int nin) /* hash table storage */", "{ H_el *ntmp;", " H_el *tmp, *olst = (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", " /* for BFS_PAR we can only get here in BITSTATE mode */", " /* and in that case we don't use locks */", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " e_critical(BFS_ID); /* bfs_par / h_store */", " #endif", " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)", " enter_critical(CS_ID);", " #endif", " tmp = H_tab[j1_spin];", " if (!tmp)", " { tmp = grab_state(n);", /* no zero-returns with bfs_par */ " #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", " #if !defined(SAFETY) && !defined(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 */", " uint 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", " #if NCORE>1", " Lstate = (H_el *) tmp; /* h_store */", " #endif", "#ifdef FULLSTACK", "#ifndef SAFETY", /* or else wasnew == 0 */ " if (wasnew)", " { Lstate = (H_el *) tmp; /* h_store */", " 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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #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 = (H_el *) tmp; /* h_store */", "#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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #endif", " #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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #endif", " #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 defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #endif", " #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 = (H_el *) tmp; /* h_store */", " #endif", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #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", " #if !defined(SAFETY) && !defined(NOCOMP)", " if (S_A)", " { v[0] = V_A;", "#ifndef NOFAIR", " if (S_A > NFAIR)", " { uint 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", " #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 = (H_el *) tmp; /* end of h_store */", " #else", " #ifdef DEBUG", " dumpstate(-1, v, n, 0);", " #endif", " #if NCORE>1", " Lstate = (H_el *) tmp; /* end of h_store */", " #endif", " #endif", " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)", " x_critical(BFS_ID);", " #endif", " #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;", "}", /* end of h_store */ "#endif", /* !BFS_PAR || !USE_TDH */ "", "void", "o_hash32(uchar *s, int len, int h) /* 32-bit, like d_sfh, but with seed */", "{ uint32_t 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;", "}", "void", "o_hash64(uchar *kb, int nbytes, int seed)", /* 64-bit hash */ "{ uint8_t *bp;", " uint64_t a, b, c, n;", " const uint64_t *k = (uint64_t *) kb;", " n = nbytes/WS; /* nr of 8-byte chunks */", " /* extend to multiple of words, if needed */", " a = WS - (nbytes %% WS);", " if (a > 0 && a < WS)", " { n++;", " bp = kb + nbytes;", " switch (a) {", " case 7: *bp++ = 0; /* fall thru */", " case 6: *bp++ = 0; /* fall thru */", " case 5: *bp++ = 0; /* fall thru */", " case 4: *bp++ = 0; /* fall thru */", " case 3: *bp++ = 0; /* fall thru */", " case 2: *bp++ = 0; /* fall thru */", " case 1: *bp = 0;", " case 0: break;", " } }", " a = (uint64_t) seed;", " b = HASH_CONST[HASH_NR];", " c = 0x9e3779b97f4a7c13LL; /* arbitrary */", " 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);", "", " K1 = a;", "}", "", "#if defined(USE_TDH) && !defined(WIN32) && !defined(WIN64)", #if 0 some problems with this storage mode: 0. pre-allocates full hash-table with slots equal to max statevector size e.g. with -w26 we allocate 2^26 (64 M) slots of VECTORSZ large which can accomodate up to 64 M states once you get close to or exceed the max, the search aborts with a 'hashtable full' message in HC mode the max storage needed per state is more modest and independent of the maximum vectorsize; which makes this mode attractive as a default 1. does not support PO reduction through the Lstate->ostate->tagged to distinguish open from closed states - this can reduce states by 50% could add this as another bit from the hash value e.g., could add it in HC mode to the first hash? 2. the same state may be stored multiple times #endif "#ifdef HC", " #ifndef T_HC", " #ifdef BFS_HC", " #define T_HC BFS_HC", " #else", " #define T_HC 2", " #endif", " #endif", " #if T_HC<1 || T_HC>4", " #error \"BFS_HC must be 1, 2, 3, or 4 (default is 2)\"", " #endif", "#endif", "", "#define T_ROW 6", /* related to cache line size */ "#define T_ROW_SIZE (1<<T_ROW)", "#define T_ROW_MASK -(1<<T_ROW)", "#define T_FREE 0", "#define T_STAT 1 /* status bit */", "#ifndef T_VSZ", " #define T_VSZ VECTORSZ/4 /* compressed vectorsize */", "#endif", "", "static volatile char *ohash_sd; /* state data */", "static volatile uint32_t *ohash_hv; /* hash values */", "static ulong ohash_max;", "static ulong ohash_mask;", "", "#if defined(USE_TDH) && defined(Q_PROVISO)", " static volatile uchar *ohash_inq; /* open/closed flag BFS_INQ */", "#endif", "#ifdef HC", " static uint32_t ohash_hc[T_HC];", " static ulong ohash_hc_sz;", "#endif", "", "void", "init_HT(ulong x) /* USE_TDH cygwin/linux */", "{ x = x / (ulong) sizeof(H_el *); /* room for x pointers */", " #ifdef DEBUG", " printf(\"prealloc x %%lu v %%d x*v %%lu\\n\",", " x, T_VSZ, (ulong) (x * (ulong)T_VSZ));", " #endif", "#ifndef HC", " if (!(x * (ulong) T_VSZ > x))", " { Uerror(\"assertion x * (ulong) T_VSZ > x fails\");", " }", " #ifdef BFS_SEP_HASH", " ohash_sd = (char *) emalloc(x * (ulong) T_VSZ);", " #else", " ohash_sd = (volatile char *) sh_pre_malloc(x * (ulong) T_VSZ);", " #endif", "#else", /* assume T_HC >= 1, and normally 2 */ " ohash_hc_sz = (ulong) (T_HC * (ulong) sizeof(uint32_t));", " if (!(x * ohash_hc_sz > x))", /* watch for overflow */ " { Uerror(\"assertion x * ohash_hc_sz > x fails\");", " }", " #ifdef BFS_SEP_HASH", " ohash_sd = (char *) emalloc(x * ohash_hc_sz);", " #else", " ohash_sd = (volatile char *) sh_pre_malloc(x * ohash_hc_sz);", " #endif", "#endif", "#ifdef BFS_SEP_HASH", " ohash_hv = (uint32_t *) emalloc(x * (ulong) sizeof(uint32_t));", "#else", " ohash_hv = (volatile uint32_t *) sh_pre_malloc(x * (ulong) sizeof(uint32_t));", "#endif", " ohash_mask = (((ulong)1)<<ssize)-1;", " ohash_max = (((ulong)1)<<ssize)/100;", "#if defined(USE_TDH) && defined(Q_PROVISO)", " #ifdef BFS_SEP_HASH", " ohash_inq = (uchar *) emalloc(x * (ulong) sizeof(uchar));", " #else", " ohash_inq = (volatile uchar *) sh_pre_malloc(x * (ulong) sizeof(uchar));", " #endif", "#endif", "}", "", "static int h_table_full;", "#ifdef L_BOUND", "void", "bfs_mark_live(void)", "{ int i;", "", " trpt->o_pm &= ~2;", "#ifdef VERBOSE", " bfs_printf(\"check to mark\\n\");", "#endif", " for (i = 0; i < (int) now._nr_pr; i++)", " { P0 *ptr = (P0 *) pptr(i);", " if (accpstate[ptr->_t][ptr->_p])", " { trpt->o_pm |= 2;", " now._l_bnd = L_bound;", " now._l_sds = (uchar *) 0;", "#ifdef VERBOSE", " bfs_printf(\"mark state live\\n\");", "#endif", " break;", " } }", "}", "void", "bfs_check_live(uchar b, uchar *s)", "{ /* assert(b>0); */", " now._l_bnd = b-1; /* decrease bound */", "#ifdef VERBOSE", " bfs_printf(\"check live %%d\\n\", b);", "#endif", " if (b == L_bound && boq == -1)", /* never mid rv */ " { now._l_sds = (uchar *) Lstate; /* new target */", " } else", " { now._l_sds = s; /* restore target */", " if (s == (uchar *) Lstate)", " { depthfound = depth - (BASE+1)*(L_bound - now._l_bnd - 1);", " uerror(\"accept cycle found\");", " depthfound = -1;", " now._l_bnd = 0;", " now._l_sds = (uchar *) 0;", " } }", "#ifdef VERBOSE", " bfs_printf(\"set l_bound to %%d -- sds %%p\\n\", b-1, (void *) now._l_sds);", "#endif", "}", "#endif", "/* closed hashing with locality - similar to ltsmin */", "int", "o_store(const char *vin, int nin)", "{ int i, seed = 0;", " ulong hash_v, ix, ex;", " uint32_t T_BUSY, T_DONE;", " volatile uint32_t *t_entry;", "#ifdef HC", " ulong vs = ohash_hc_sz;", "#else", " ulong vs = (ulong) T_VSZ;", "#endif", "#ifdef L_BOUND", " uchar o_bnd, *o_sds;", "#endif", "#ifndef STOP_ON_FULL", " if (h_table_full)", " { goto done;", " }", "#endif", "#ifdef L_BOUND", " if (now._l_bnd == 0)", " { bfs_mark_live();", " }", " #ifdef VERBOSE", " else", " { bfs_printf(\"non-markable state %%d\\n\", now._l_bnd);", " }", " #endif", " o_bnd = now._l_bnd;", " o_sds = now._l_sds;", " now._l_bnd = (o_bnd)?1:0; /* mark nested phase of bounded search */", " now._l_sds = (uchar *) 0;", "#endif", "#if !defined(HC) && !defined(T_NOCOMP)", " nin = compress((char *)vin, nin);", " vin = (char *) &comp_now;", "#endif", " do { o_hash((uchar *)vin, nin, seed++);", " hash_v = K1;", " } while (hash_v == T_FREE || hash_v == T_STAT); /* unlikely, hash_v 0 or 1 */", "", " T_BUSY = ((uint32_t) hash_v & ~((uint32_t) T_STAT)); /* hash with status bit 0 */", " T_DONE = ((uint32_t) hash_v | ((uint32_t) T_STAT)); /* hash with status bit 1 */", "#ifdef HC", " d_hash((uchar *)vin, nin);", /* HC */ " ohash_hc[0] = (uint32_t) K1;", " #if T_HC>1", " ohash_hc[1] = (uint32_t) (K1>>32);", /* assumes ulong = 64 bits */ " #endif", " #if T_HC>2", " ohash_hc[2] = (uint32_t) K2;", " #endif", " #if T_HC>3", " ohash_hc[3] = (uint32_t) (K2>>32);", " #endif", "#endif", " while (seed < ohash_max)", " { ix = hash_v & ohash_mask;", " ex = (ix & T_ROW_MASK) + T_ROW_SIZE;", " for (i = 0; i < T_ROW_SIZE; i++)", " { t_entry = (uint32_t *) &ohash_hv[ix];", " if (*t_entry == T_FREE && cas(t_entry, T_FREE, T_BUSY))", " {", "#ifndef HC", " memcpy((char *) &ohash_sd[ix * vs], vin, nin);", "#else", " memcpy((char *) &ohash_sd[ix * vs], (char *) ohash_hc, vs);", "#endif", "#if defined(USE_TDH) && defined(Q_PROVISO)", " ohash_inq[ix] = (uchar) BFS_INQ;", " Lstate = (H_el *) &ohash_inq[ix];", "#endif", " *t_entry = T_DONE;", "#ifdef VERBOSE", " #ifdef L_BOUND", " bfs_printf(\"New state %%p [%%p]\\n\",", " (void *) Lstate, (void *) o_sds);", " #else", " bfs_printf(\"New state %%p\\n\", (void *) Lstate);", " #endif", "#endif", "#ifdef L_BOUND", " if (o_bnd) { bfs_check_live(o_bnd, o_sds); }", "#endif", " return 0; /* New State */", " }", " while (*t_entry == T_BUSY)", " { usleep(2); /* wait */", " }", " if (*t_entry == T_DONE /* (first) hash matches, check data */", "#ifndef HC", " && memcmp((char *) &ohash_sd[ix * vs], vin, nin) == 0)", "#else", " && memcmp((char *) &ohash_sd[ix * vs], (char *) ohash_hc, vs) == 0)", "#endif", " {", "#if defined(USE_TDH) && defined(Q_PROVISO)", " Lstate = (H_el *) &ohash_inq[ix];", "#endif", "#ifdef VERBOSE", " #ifdef L_BOUND", " bfs_printf(\"Old state %%p [%%p]\\n\",", " (void *) Lstate, (void *) o_sds);", " #else", " bfs_printf(\"Old state %%p\\n\", (void *) Lstate);", " #endif", "#endif", "#ifdef L_BOUND", " if (o_bnd) { bfs_check_live(o_bnd, o_sds); }", "#endif", " return 1; /* Old State */", " }", " hcmp++; ix++;", " ix = (ix==ex) ? ex - T_ROW_SIZE : ix;", " }", " /* find a new slot: */", " do { o_hash((uchar *)vin, nin, (int) (hash_v + seed++));", " hash_v = K1;", " } while (hash_v == T_FREE || hash_v == T_STAT);", " T_BUSY = ((uint32_t) hash_v & ~((uint32_t) T_STAT));", " T_DONE = ((uint32_t) hash_v | ((uint32_t) T_STAT));", " }", "#ifdef STOP_ON_FULL", " Uerror(\"hash table full\");", " /* no return from Uerror */", "#else", " if (!h_table_full)", " { h_table_full++;", " if (who_am_i == 0)", " { bfs_printf(\"hash table is full\\n\");", " } }", "done:", " bfs_punt++; /* counts this as a lost state */", "#endif", "#ifdef L_BOUND", " now._l_bnd = 0; /* no more checking */", " now._l_sds = (uchar *) 0;", "#endif", " return 1; /* technically should be 0, but we want to throttle down */", "}", "#endif", /* USE_TDH && !WIN32 && !WIN64 */ "#endif", /* !BITSTATE || FULLSTACK */ "#include TRANSITIONS", 0, };