1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456145714581459146014611462146314641465146614671468146914701471147214731474147514761477147814791480148114821483148414851486148714881489149014911492149314941495149614971498149915001501150215031504150515061507150815091510151115121513151415151516151715181519152015211522152315241525152615271528152915301531153215331534153515361537153815391540154115421543154415451546154715481549155015511552155315541555155615571558155915601561156215631564156515661567156815691570157115721573157415751576157715781579158015811582158315841585158615871588158915901591159215931594159515961597159815991600160116021603160416051606160716081609161016111612161316141615161616171618161916201621162216231624162516261627162816291630163116321633163416351636163716381639164016411642164316441645164616471648164916501651165216531654165516561657165816591660166116621663166416651666166716681669167016711672167316741675167616771678167916801681168216831684168516861687168816891690169116921693169416951696169716981699170017011702170317041705170617071708170917101711171217131714171517161717171817191720172117221723172417251726172717281729173017311732173317341735173617371738173917401741174217431744174517461747174817491750175117521753175417551756175717581759176017611762176317641765176617671768176917701771177217731774177517761777177817791780178117821783178417851786178717881789179017911792179317941795179617971798179918001801180218031804180518061807180818091810181118121813181418151816181718181819182018211822182318241825182618271828182918301831183218331834183518361837183818391840184118421843184418451846184718481849185018511852185318541855185618571858185918601861186218631864186518661867186818691870187118721873187418751876187718781879188018811882188318841885188618871888188918901891189218931894189518961897189818991900190119021903190419051906190719081909191019111912191319141915191619171918191919201921192219231924192519261927192819291930193119321933193419351936193719381939194019411942194319441945194619471948194919501951195219531954195519561957195819591960196119621963196419651966196719681969197019711972197319741975197619771978197919801981198219831984198519861987198819891990199119921993199419951996199719981999200020012002200320042005200620072008200920102011201220132014201520162017201820192020202120222023202420252026202720282029203020312032203320342035203620372038203920402041204220432044204520462047204820492050205120522053205420552056205720582059206020612062206320642065206620672068206920702071207220732074207520762077207820792080208120822083208420852086208720882089209020912092209320942095209620972098209921002101210221032104210521062107210821092110211121122113211421152116211721182119212021212122212321242125212621272128212921302131213221332134213521362137213821392140214121422143214421452146214721482149215021512152215321542155215621572158215921602161216221632164216521662167216821692170217121722173217421752176217721782179218021812182218321842185218621872188218921902191219221932194219521962197219821992200220122022203220422052206220722082209221022112212221322142215221622172218221922202221222222232224222522262227222822292230223122322233223422352236223722382239224022412242224322442245224622472248224922502251225222532254225522562257225822592260226122622263226422652266226722682269227022712272227322742275227622772278227922802281228222832284228522862287228822892290229122922293229422952296229722982299230023012302230323042305230623072308230923102311231223132314231523162317231823192320232123222323232423252326232723282329233023312332233323342335233623372338233923402341234223432344234523462347234823492350235123522353235423552356235723582359236023612362236323642365236623672368236923702371237223732374237523762377237823792380238123822383238423852386238723882389239023912392239323942395239623972398239924002401240224032404240524062407240824092410241124122413241424152416241724182419242024212422242324242425242624272428242924302431243224332434243524362437243824392440244124422443244424452446244724482449245024512452245324542455245624572458245924602461246224632464246524662467246824692470247124722473247424752476247724782479248024812482248324842485248624872488248924902491249224932494249524962497249824992500250125022503250425052506250725082509251025112512251325142515251625172518251925202521252225232524252525262527252825292530253125322533253425352536253725382539254025412542254325442545254625472548254925502551255225532554255525562557255825592560256125622563256425652566256725682569257025712572257325742575257625772578257925802581258225832584258525862587258825892590259125922593259425952596259725982599260026012602260326042605260626072608260926102611261226132614261526162617261826192620262126222623262426252626262726282629263026312632263326342635263626372638263926402641264226432644264526462647264826492650265126522653265426552656265726582659266026612662266326642665266626672668266926702671267226732674267526762677267826792680268126822683268426852686268726882689269026912692269326942695269626972698269927002701270227032704270527062707270827092710271127122713271427152716271727182719272027212722272327242725272627272728272927302731273227332734273527362737273827392740274127422743274427452746274727482749275027512752275327542755275627572758275927602761276227632764276527662767276827692770277127722773277427752776277727782779278027812782278327842785278627872788278927902791279227932794279527962797279827992800280128022803280428052806280728082809281028112812281328142815281628172818281928202821282228232824282528262827282828292830283128322833283428352836283728382839284028412842284328442845284628472848284928502851285228532854285528562857285828592860286128622863286428652866286728682869287028712872287328742875287628772878287928802881288228832884288528862887288828892890289128922893289428952896289728982899290029012902290329042905290629072908290929102911291229132914291529162917291829192920292129222923292429252926292729282929293029312932293329342935293629372938293929402941294229432944294529462947294829492950295129522953295429552956295729582959296029612962296329642965296629672968296929702971297229732974297529762977297829792980298129822983298429852986298729882989299029912992299329942995299629972998299930003001300230033004300530063007300830093010301130123013301430153016301730183019302030213022302330243025302630273028302930303031303230333034303530363037303830393040304130423043304430453046304730483049305030513052305330543055305630573058305930603061306230633064306530663067306830693070307130723073307430753076307730783079308030813082308330843085308630873088308930903091309230933094309530963097309830993100310131023103310431053106310731083109311031113112311331143115311631173118311931203121312231233124312531263127312831293130313131323133313431353136313731383139314031413142314331443145314631473148314931503151315231533154315531563157315831593160316131623163316431653166316731683169317031713172317331743175317631773178317931803181318231833184318531863187318831893190319131923193319431953196319731983199320032013202320332043205320632073208320932103211321232133214321532163217321832193220322132223223322432253226322732283229323032313232323332343235323632373238323932403241324232433244324532463247324832493250325132523253325432553256325732583259326032613262326332643265326632673268326932703271327232733274327532763277327832793280328132823283328432853286328732883289329032913292329332943295329632973298329933003301330233033304330533063307330833093310331133123313331433153316331733183319332033213322332333243325332633273328332933303331333233333334333533363337333833393340334133423343334433453346334733483349335033513352335333543355335633573358335933603361336233633364336533663367336833693370337133723373337433753376337733783379338033813382338333843385338633873388338933903391339233933394339533963397339833993400340134023403340434053406340734083409341034113412341334143415341634173418341934203421342234233424342534263427342834293430343134323433343434353436343734383439344034413442344334443445344634473448344934503451345234533454345534563457345834593460346134623463346434653466346734683469347034713472347334743475347634773478347934803481348234833484348534863487348834893490349134923493349434953496349734983499350035013502350335043505350635073508350935103511351235133514351535163517351835193520352135223523352435253526352735283529353035313532353335343535353635373538353935403541354235433544354535463547354835493550355135523553355435553556355735583559356035613562356335643565356635673568356935703571357235733574357535763577357835793580358135823583358435853586358735883589359035913592359335943595359635973598359936003601360236033604360536063607 |
- /***** spin: pangen1.h *****/
- /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* Permission is given to distribute this code provided that this intro- */
- /* ductory message is not removed and no monies are exchanged. */
- /* No guarantee is expressed or implied by the distribution of this code. */
- /* Software written by Gerard J. Holzmann as part of the book: */
- /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */
- /* Prentice Hall, Englewood Cliffs, NJ, 07632. */
- /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */
- static char *Code2[] = { /* the tail of procedure run() */
- "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
- " if (!state_tables)",
- " { printf(\"warning: for p.o. reduction to be valid \");",
- " printf(\"the never claim must be stutter-closed\\n\");",
- " printf(\"(never claims generated from LTL \");",
- " printf(\"formulae are stutter-closed)\\n\");",
- " }",
- "#endif",
- " UnBlock; /* disable rendez-vous */",
- "#ifdef MEMCNT",
- " overhead = memcnt;",
- "#endif",
- "#ifdef BITSTATE",
- " SS = (uchar *) emalloc(1<<(ssize-3));",
- "#else",
- " hinit();",
- "#endif",
- "#if defined(FULLSTACK) && defined(BITSTATE)",
- " onstack_init();",
- "#endif",
- "#ifdef CNTRSTACK",
- " LL = (uchar *) emalloc(1<<(ssize-3));",
- "#endif",
- " stack = ( Stack *) emalloc(sizeof(Stack));",
- " svtack = (Svtack *) emalloc(sizeof(Svtack));",
- " /* a place to point for Pptr of non-running procs: */",
- " noptr = (uchar *) emalloc(Maxbody * sizeof(char));",
- "#ifdef SVDUMP",
- " if (vprefix > 0)",
- " write(svfd, (uchar *) &vprefix, sizeof(int));",
- "#endif",
- "#ifdef VERI",
- " Addproc(VERI); /* never - pid = 0 */",
- "#endif",
- " active_procs(); /* started after never */",
- "#ifdef EVENT_TRACE",
- " now._event = start_event;",
- " reached[EVENT_TRACE][start_event] = 1;",
- "#endif",
- "go_again:",
- " do_the_search();",
- "#if defined(BITSTATE)",
- " if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
- " { printf(\"Run %%d:\\n\", HASH_NR);",
- " wrap_stats();",
- " printf(\"\\n\");",
- " memset(SS, 0, 1<<(ssize-3));",
- "#if defined(CNTRSTACK)",
- " memset(LL, 0, 1<<(ssize-3));",
- "#endif",
- "#if defined(FULLSTACK)",
- " memset((uchar *) S_Tab, 0, ",
- " (1<<(ssize-3))*sizeof(struct H_el *));",
- "#endif",
- " nstates=nlinks=truncs=truncs2=ngrabs = 0;",
- " nlost=nShadow=hcmp = 0;",
- " Fa=Fh=Zh=Zn = 0;",
- " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
- " goto go_again;",
- " }",
- "#endif",
- "}",
- #ifndef PRINTF
- "#include <stdarg.h>",
- "void",
- "Printf(const char *fmt, ...)",
- "{ /* Make sure the args to Printf",
- " * are always evaluated (e.g., they",
- " * could contain a run stmnt)",
- " * but don't 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 PRINTF",
- " va_list args;",
- " va_start(args, fmt);",
- " vprintf(fmt, args);",
- " va_end(args);",
- "#endif",
- "}",
- #endif
- "#ifndef SC",
- "#define getframe(i) &trail[i];",
- "#else",
- "static long HHH, DDD, hiwater;",
- "static long CNT1, CNT2;",
- "static int stackwrite;",
- "static int stackread;",
- "static Trail frameptr;",
- "Trail *"
- "getframe(int d)",
- "{",
- " if (CNT1 == CNT2)",
- " return &trail[d];",
- "",
- " if (d >= (CNT1-CNT2)*DDD)",
- " return &trail[d - (CNT1-CNT2)*DDD];",
- "",
- " if (!stackread",
- " && (stackread = open(stackfile, 0)) < 0)",
- " { printf(\"getframe: cannot open %%s\\n\", stackfile);",
- " wrapup();",
- " }",
- " if (lseek(stackread, d*sizeof(Trail), SEEK_SET) == -1",
- " || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
- " { printf(\"getframe: frame read error\\n\");",
- " wrapup();",
- " }",
- " return &frameptr;",
- "}",
- "#endif",
- "#if !defined(SAFETY) && !defined(BITSTATE)",
- "#if !defined(FULLSTACK) || defined(MA)",
- "#define depth_of(x) A_depth /* an estimate */",
- "#else",
- "int",
- "depth_of(struct H_el *s)",
- "{ Trail *t; int d;",
- " for (d = 0; d <= A_depth; d++)",
- " { t = getframe(d);",
- " if (s == t->ostate)",
- " return d;",
- " }",
- " printf(\"pan: cannot happen, depth_of\\n\");",
- " return depthfound;",
- "}",
- "#endif",
- "#endif",
- "void",
- "do_the_search(void)",
- "{ int i;",
- " depth=mreached=0;",
- " trpt = &trail[depth];",
- "#ifdef VERI",
- " trpt->tau |= 4; /* the claim moves first */",
- "#endif",
- " for (i = 0; i < (int) now._nr_pr; i++)",
- " { P0 *ptr = (P0 *) pptr(i);",
- "#ifndef NP",
- " if (!(trpt->o_pm&2)",
- " && accpstate[ptr->_t][ptr->_p])",
- " { trpt->o_pm |= 2;",
- " }",
- "#else",
- " if (!(trpt->o_pm&4)",
- " && progstate[ptr->_t][ptr->_p])",
- " { trpt->o_pm |= 4;",
- " }",
- "#endif",
- " }",
- "#ifdef EVENT_TRACE",
- "#ifndef NP",
- " if (accpstate[EVENT_TRACE][now._event])",
- " { trpt->o_pm |= 2;",
- " }",
- "#else",
- " if (progstate[EVENT_TRACE][now._event])",
- " { trpt->o_pm |= 4;",
- " }",
- "#endif",
- "#endif",
- "#ifndef NOCOMP",
- " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */",
- " if (!a_cycles)",
- " { i = &(now._a_t) - (uchar *) &now;",
- " Mask[i] = 1; /* _a_t */",
- " }",
- "#ifndef NOFAIR",
- " if (!fairness)",
- " { int j = 0;",
- " i = &(now._cnt[0]) - (uchar *) &now;",
- " while (j++ < NFAIR)",
- " Mask[i++] = 1; /* _cnt[] */",
- " }",
- "#endif",
- "#endif",
- "#ifndef NOFAIR",
- " if (fairness",
- " && (a_cycles && (trpt->o_pm&2)))",
- " { now._a_t = 2; /* set the A-bit */",
- " now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */
- "#ifdef VERBOSE",
- " printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
- " depth, now._cnt[now._a_t&1], now._a_t);",
- "#endif",
- " }",
- "#endif",
- " new_state(); /* start 1st DFS */",
- "}",
- "#ifdef INLINE_REV",
- "char",
- "do_reverse(Trans *t, short II, char M)",
- "{ char m = M;",
- " short tt = (short) ((P0 *)this)->_p;",
- "#include REVERSE_MOVES",
- "R999: return m;",
- "}",
- "#endif",
- "#ifndef INLINE",
- "#ifdef EVENT_TRACE",
- "static char _tp = 'n'; static int _qid = 0;",
- "#endif",
- "char",
- "do_transit(Trans *t, short II, int n)",
- "{ char m;",
- " short tt = (short) ((P0 *)this)->_p;",
- " char ot = (char) ((P0 *)this)->_t;",
- "#ifdef EVENT_TRACE",
- " short oboq = boq;",
- " if (II == EVENT_TRACE) boq = -1;",
- "#define continue { boq = oboq; return 0; }",
- "#else",
- "#define continue return 0",
- "#endif",
- "#include FORWARD_MOVES",
- "P999:",
- "#ifdef EVENT_TRACE",
- " boq = oboq;",
- "#endif",
- " return m;",
- "#undef continue",
- "}",
- "#ifdef EVENT_TRACE",
- "void",
- "require(char tp, int qid)",
- "{ Trans *t;",
- " _tp = tp; _qid = qid;",
- "#ifdef NEGATED_TRACE",
- " if (now._event == endevent)",
- " { depth++; trpt++;",
- " uerror(\"event_trace error (all events matched)\");",
- "#ifndef NP",
- " if (accpstate[EVENT_TRACE][now._event])",
- " trpt->o_pm |= 2;",
- "#else",
- " if (progstate[EVENT_TRACE][now._event])",
- " trpt->o_pm |= 4;",
- "#endif",
- " trpt--; depth--;",
- " now._event = start_event;",
- " return;",
- " } else",
- "#else",
- " if (now._event != endevent)",
- "#endif",
- " for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
- " { if (do_transit(t, EVENT_TRACE, 0))",
- " { now._event = t->st;",
- " reached[EVENT_TRACE][t->st] = 1;",
- "#ifdef VERBOSE",
- " printf(\" event_trace move to -> %%d\\n\", t->st);",
- "#endif",
- "#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",
- " for (t = t->nxt; t; t = t->nxt)",
- " { if (do_transit(t, EVENT_TRACE, 0))",
- " 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 = start_event; /* only 1st try will count */",
- "#else",
- " depth++; trpt++;",
- " uerror(\"event_trace error (no matching event)\");",
- " trpt--; depth--;",
- "#endif",
- "}",
- "#endif",
- "int",
- "enabled(int iam, int pid)",
- "{ Trans *t; uchar *othis = this;",
- " int res = 0; short tt; char ot;",
- "#ifdef VERI",
- " /* if (pid > 0) */ pid++;",
- "#endif",
- " if (pid == iam)",
- " Uerror(\"used: enabled(pid=thisproc)\");",
- " if (pid < 0 || pid >= (int) now._nr_pr)",
- " return 0;",
- " this = pptr(pid);",
- " TstOnly = 1;",
- " tt = (short) ((P0 *)this)->_p;",
- " ot = (uchar) ((P0 *)this)->_t;",
- " for (t = trans[ot][tt]; t; t = t->nxt)",
- " if (do_transit(t, pid, 0))",
- " { res = 1;",
- " break;",
- " }",
- " TstOnly = 0;",
- " this = othis;",
- " return res;",
- "}",
- "#endif",
- "void",
- "snapshot(void)",
- "{ static long sdone = (long) 0;",
- " long ndone = (unsigned long) nstates/1000000;",
- " if (ndone == sdone) return;",
- " sdone = ndone;",
- " printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
- " printf(\"Transitions= %%7g \", nstates+truncs);",
- "#ifdef MA",
- " printf(\"Nodes= %%7d \", nr_states);",
- "#endif",
- " printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
- " fflush(stdout);",
- "}",
- "#ifdef SC",
- "void",
- "stack2disk(void)",
- "{",
- " if (!stackwrite",
- " && (stackwrite = creat(stackfile, 0666)) <= 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*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*sizeof(Trail), SEEK_SET) == -1)",
- " Uerror(\"disk2stack lseek error2\");",
- "",
- " have = read(stackread, trail, DDD*sizeof(Trail));",
- " if (have != DDD*sizeof(Trail))",
- " Uerror(\"stackfile read error\");",
- "}",
- "#endif",
- "uchar *",
- "Pptr(int x)", /* as a fct, to avoid a problem with the p9 compiler */
- "{ if (proc_offset[x])",
- " return (uchar *) pptr(x);",
- " else",
- " return noptr;",
- "}",
- "extern void check_claim(int);",
- "/* new_state() is the main search routine in the verifier",
- " * it has a lot of code ifdef-ed together to support",
- " * different search modes -- this makes it quite unreadable",
- " * of course. if you are studying the code, first",
- " * let the C preprocessor generate a specific version",
- " * from the pan.c source, e.g. by saying:",
- " * /lib/cpp -DNOREDUCE -DBITSTATE pan.c > Pan.c",
- " * and study the resulting file, rather than this one",
- " */",
- "void",
- "new_state(void)",
- "{ Trans *t;",
- " char n, m, ot;",
- " short II, JJ=0, tt, kk;\n",
- " short From = now._nr_pr-1, To = BASE;",
- "Down:",
- "#ifdef CHECK",
- " printf(\"%%d: Down - %%s\",",
- " depth, (trpt->tau&4)?\"claim\":\"program\");",
- " printf(\" %%saccepting [pids %%d-%%d]\\n\",",
- " (trpt->o_pm&2)?\"\":\"non-\", From, To);",
- "#endif",
- "#ifdef SC",
- " if (depth > hiwater)",
- " { stack2disk();",
- " maxdepth += DDD;",
- " hiwater += DDD;",
- " trpt -= DDD;",
- "if(verbose)",
- "printf(\"zap %%d: %%d (maxdepth now %%d)\\n\", CNT1, hiwater, maxdepth);",
- " }",
- "#endif",
- " trpt->tau &= ~(16|32|64); /* make sure these are off */",
- "#if defined(FULLSTACK) && defined(MA)",
- " trpt->proviso = 0;",
- "#endif",
- " if (depth >= maxdepth)",
- " { truncs++;",
- "#if SYNC",
- " (trpt+1)->o_n = 1; /* not a deadlock */",
- "#endif",
- " if (!warned)",
- " { warned = 1;",
- " printf(\"error: max search depth too small\\n\");",
- " }",
- " (trpt-1)->tau |= 16; /* worstcase guess */",
- " goto Up;",
- " }",
- "AllOver:",
- "#if defined(FULLSTACK) && !defined(MA)",
- " trpt->ostate = (struct H_el *) 0;",
- "#endif",
- "#ifdef VERI",
- " if ((trpt->tau&4) || ((trpt-1)->tau&128))",
- "#endif",
- " if (boq == -1) { /* if not mid-rv */",
- "#ifndef SAFETY",
- " /* this check should now be redundant",
- " * because the seed state also appears",
- " * on the 1st dfs stack and would be",
- " * matched in hstore below",
- " */",
- " if ((now._a_t&1) && depth > A_depth)",
- " { if (!memcmp((char *)&A_Root, ",
- " (char *)&now, vsize))",
- " {",
- " depthfound = A_depth;",
- "#ifdef CHECK",
- " printf(\"matches seed\\n\");",
- "#endif",
- "#ifdef NP",
- " uerror(\"non-progress cycle\");",
- "#else",
- " uerror(\"acceptance cycle\");",
- "#endif",
- " goto Up;",
- " }",
- "#ifdef CHECK",
- " printf(\"not seed\\n\");",
- "#endif",
- " }",
- "#endif",
- " if (!(trpt->tau&8)) /* if no atomic move */",
- " {",
- "#ifdef CNTRSTACK", /* -> bitstate, reduced, safety */
- " d_hash((uchar *)&now, vsize);",
- " trpt->j6 = j1; trpt->j7 = j2;",
- " JJ = LL[j1] && LL[j2];",
- "#endif",
- "#ifdef FULLSTACK",
- "#ifdef BITSTATE",
- " JJ = onstack_now();",
- "#else",
- "#ifdef MA",
- " II = gstore((char *)&now, vsize, 0);",
- "#else",
- " II = hstore((char *)&now, vsize, 1);",
- "#endif",
- " JJ = (II == 2)?1:0;",
- "#endif",
- "#endif",
- "#ifdef BITSTATE",
- "#ifndef CNTRSTACK", /* !reduced */
- " d_hash((uchar *) &now, vsize);",
- "#endif",
- " kk = II = ((SS[j2]&j3) && (SS[j1]&j4));",
- "#ifdef DEBUG",
- " if (II) printf(\"Old bitstate\\n\");",
- " else printf(\"New bitstate\\n\");",
- "#endif",
- "#else",
- "#ifndef FULLSTACK",
- "#ifdef MA",
- " JJ = II = gstore((char *) &now, vsize, 0);",
- "#else",
- " II = hstore((char *)&now, vsize, 2);",
- "#endif",
- "#endif",
- " kk = (II == 1 || II == 2);",
- "#endif",
- "#ifndef SAFETY",
- "#if defined(FULLSTACK) && defined(BITSTATE)",
- " if (!JJ && (now._a_t&1) && depth > A_depth)",
- " { int oj1 = j1;",
- " uchar o_a_t = now._a_t;",
- " now._a_t &= ~(1|16|32);",
- " if (onstack_now())",
- " { II = 3;",
- "#ifdef VERBOSE",
- " printf(\"state match on 1st dfs stack\\n\");",
- "#endif",
- " }",
- " now._a_t = o_a_t;",
- " j1 = oj1;",
- " }",
- "#endif",
- " if (II == 3 && a_cycles && (now._a_t&1))",
- " {",
- "#ifndef NOFAIR",
- " if (fairness && now._cnt[1] > 1) /* was != 0 */",
- " {",
- "#ifdef VERBOSE",
- " printf(\" fairness count non-zero\\n\");",
- "#endif",
- " II = 0;",
- " } else",
- "#endif",
- " {",
- "#ifdef BITSTATE",
- " depthfound = Lstate->tagged - 1;",
- "#ifdef NP",
- " uerror(\"non-progress cycle\");",
- "#else",
- " uerror(\"acceptance cycle\");",
- "#endif",
- "#else",
- " depthfound = depth_of(Lstate);",
- "#ifdef NP",
- " uerror(\"non-progress cycle\");",
- "#else",
- " uerror(\"acceptance cycle\");",
- "#endif",
- " nShadow--;",
- "#endif",
- " goto Up;",
- " }",
- " }",
- "#endif",
- "#if !defined(FULLSTACK) && !defined(CNTRSTACK) && defined(BITSTATE)",
- "#ifndef NOREDUCE",
- " JJ = II; /* worstcase guess for p.o. */",
- "#endif",
- "#endif",
- "#ifndef NOREDUCE",
- "#ifndef SAFETY",
- " if ((II && JJ) || (II == 3))",
- " { /* marker for liveness proviso */",
- " truncs2++;",
- " (trpt-1)->tau |= 16;",
- " }",
- "#else",
- " if (!II || !JJ)",
- " { /* has successor outside stack */",
- " (trpt-1)->tau |= 64;",
- " }",
- "#endif",
- "#endif",
- " if (II)",
- " { truncs++;",
- " goto Up;",
- " }",
- " if (!kk)",
- " { nstates++;",
- "#ifdef SVDUMP",
- " if (vprefix > 0)",
- " if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
- " { fprintf(efd, \"writing %%s.svd failed\\n\", Source);",
- " wrapup();",
- " }",
- "#endif",
- " if ((unsigned long) nstates%%1000000 == 0)",
- " snapshot();",
- "#ifdef MA",
- "#ifdef W_XPT",
- " if ((unsigned long) nstates%%W_XPT == 0)",
- " { void w_xpoint(void);",
- " w_xpoint();",
- " }",
- "#endif",
- "#endif",
- " }",
- "#ifdef BITSTATE",
- "#ifdef RANDSTOR",
- " if (rand()%%100 <= RANDSTOR)",
- "#endif",
- " { SS[j2] |= j3; SS[j1] |= j4; }",
- "#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",
- "#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(\"endstate in claim reached\");",
- " check_claim(((P0 *)pptr(0))->_p);",
- "Stutter:",
- " if (trpt->tau&4) /* must make a claimmove */",
- " { II = 0; /* never */",
- " goto Veri0;",
- " }",
- "#endif",
- "#ifndef NOREDUCE",
- " /* Look for a process with only safe transitions */",
- " /* (special rules apply in the 2nd dfs) */",
- "#ifdef SAFETY",
- " if (boq == -1 && From != To)",
- "#else",
- "/* implied: #ifdef FULLSTACK */",
- " if (boq == -1 && From != To",
- " && (!(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))",
- "#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 */",
- "#endif",
- " for (II = From; II >= To; II -= 1)",
- " {",
- "Resume: /* pick up here if preselect fails */",
- " this = pptr(II);",
- " tt = (short) ((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;",
- "#ifdef NIBIS",
- " t->om = 0;",
- "#endif",
- " trpt->tau |= 32; /* preselect marker */",
- "#ifdef DEBUG",
- "#ifdef NIBIS",
- " printf(\"%%3d: proc %%d Pre\", depth, II);",
- " printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
- " t->om, trpt->tau);",
- "#else",
- " printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
- " depth, II, trpt->tau);",
- "#endif",
- "#endif",
- " goto Again;",
- " }",
- " }",
- " trpt->tau &= ~32;",
- "#endif",
- "Again:",
- " /* The Main Expansion Loop over Processes */",
- " trpt->o_pm &= ~(8|16|32|64); /* 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;", /* NEW +1 */
- " trpt->o_pm |= 8;",
- "#ifdef DEBUG",
- " printf(\"%%3d: 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)", /* NEW: 1 iso 0 */
- " { now._a_t &= ~2;", /* reset a-bit */
- " now._cnt[now._a_t&1] = 0;", /* NEW: reset cnt */
- " trpt->o_pm |= 16;",
- "#ifdef DEBUG",
- " printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
- " depth, now._a_t);",
- "#endif",
- " } } }",
- "#endif",
- " for (II = From; II >= To; II -= 1)",
- " {",
- "#if SYNC",
- " /* no rendezvous with same proc */",
- " if (boq != -1 && trpt->pr == II) continue;",
- "#endif",
- "Veri0: this = pptr(II);",
- " tt = (short) ((P0 *)this)->_p;",
- " ot = (uchar) ((P0 *)this)->_t;",
- "#ifdef NIBIS",
- " /* don't repeat a previous preselected expansion */",
- " /* could hit this if reduction proviso was false */",
- " t = trans[ot][tt];",
- " if (!(trpt->tau&4)", /* not claim */
- " && !(trpt->tau&1)", /* not timeout */
- " && !(trpt->tau&32)", /* not preselected */
- " && (t->atom & 8)", /* local */
- " && boq == -1", /* not inside rendezvous */
- " && From != To)", /* not inside atomic seq */
- " { if (t->qu[0] == 0", /* unconditional */
- " || q_cond(II, t))", /* true condition */
- " { m = t->om;",
- " if (m>n||(n>3&&m!=0)) n=m;",
- " continue; /* did it before */",
- " } }",
- "#endif",
- " trpt->o_pm &= ~1; /* no move in this pid yet */",
- "#ifdef EVENT_TRACE",
- " (trpt+1)->o_event = now._event;",
- "#endif",
- " /* Fairness: Cnt++ when Cnt == II */",
- "#ifndef NOFAIR",
- " trpt->o_pm &= ~64; /* didn't apply rule 2 */",
- " if (fairness",
- " && boq == -1", /* not mid rv - except rcv - NEW 3.0.8 */
- " && !(trpt->o_pm&32)", /* Rule 2 not in effect */
- " && (now._a_t&2)", /* A-bit is set */
- " && now._cnt[now._a_t&1] == II+2)",
- " { now._cnt[now._a_t&1] -= 1;",
- "#ifdef VERI",
- " /* claim need not participate */",
- " if (II == 1)",
- " now._cnt[now._a_t&1] = 1;",
- "#endif",
- "#ifdef DEBUG",
- " printf(\"%%3d: proc %%d fairness \", depth, II);",
- " printf(\"Rule 2: --cnt to %%d (%%d)\\n\",",
- " now._cnt[now._a_t&1], now._a_t);",
- "#endif",
- " trpt->o_pm |= (32|64);",
- " }",
- "#endif",
- "#ifdef HAS_PROVIDED",
- " if (!provided(II, ot, tt, t)) continue;",
- "#endif",
- " /* check all trans of proc II - escapes first */",
- "#ifdef HAS_UNLESS",
- " trpt->e_state = 0;",
- "#endif",
- "#ifdef EVENT_TRACE",
- " (trpt+1)->pr = II;",
- "#endif",
- " for (t = trans[ot][tt]; t; t = t->nxt)",
- " {",
- "#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",
- "#ifdef EVENT_TRACE",
- " (trpt+1)->o_t = t;",
- "#endif",
- "#ifdef INLINE",
- "#include FORWARD_MOVES",
- "#else",
- " if (!(m = do_transit(t, II, n))) continue;",
- "#endif",
- "P999: /* jumps here when move succeeds */",
- " 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;",
- " trpt->o_pm |= 1; /* we moved */",
- " }",
- "#else",
- " trpt->o_pm |= 1; /* we moved */",
- "#endif",
- "#ifdef PEG",
- " peg[t->forw]++;",
- "#endif",
- "#if defined(VERBOSE) || defined(CHECK)",
- "#if defined(SVDUMP)",
- " printf(\"%%3d: proc %%d exec %%d \\n\", ",
- " depth, II, t->t_id);",
- "#else",
- " printf(\"%%3d: 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",
- "#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 = 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)",
- " { int ii;",
- "#define PQ ((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[PQ->_t][PQ->_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[PQ->_t][PQ->_p])",
- " { trpt->o_pm |= 4;",
- " break;",
- " } }",
- "#endif",
- "#undef PQ",
- " }",
- "#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;",
- " 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 = now._nr_pr-1; To = BASE;",
- " }",
- " goto Down; /* pseudo-recursion */",
- "Up:",
- "#ifdef CHECK",
- " printf(\"%%d: Up - %%s\\n\", depth,",
- " (trpt->tau&4)?\"claim\":\"program\");",
- "#endif",
- "#ifdef MA",
- " 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)",
- " {",
- " trpt += DDD;",
- " disk2stack();",
- " maxdepth -= DDD;",
- " hiwater -= DDD;",
- "if(verbose)",
- "printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
- " }",
- "#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(\"%%3d: reversed fairness default move\\n\", depth);",
- "#endif",
- " goto Q999;",
- " }",
- "#endif",
- "#ifdef HAS_LAST",
- "#ifdef VERI",
- " { int d; Trail *trl;",
- " now._last = 0;",
- " for (d = 1; d < depth; d++)",
- " { trl = getframe(depth-d); /* was (trpt-d) */",
- " if (trl->pr != 0)",
- " { now._last = trl->pr - BASE;",
- " break;",
- " } } }",
- "#else",
- " now._last = (depth<1)?0:(trpt-1)->pr;",
- "#endif",
- "#endif",
- "#ifdef EVENT_TRACE",
- " now._event = trpt->o_event;",
- "#endif",
- "#ifndef SAFETY",
- " if ((now._a_t&1) && depth <= A_depth)",
- " return; /* to checkcycles() */",
- "#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 INLINE_REV",
- " m = do_reverse(t, II, m);",
- "#else",
- "#include REVERSE_MOVES",
- "R999: /* jumps here when done */",
- "#endif",
- "#ifdef VERBOSE",
- " printf(\"%%3d: proc %%d \", depth, II);",
- " printf(\"reverses %%d, %%d to %%d,\",",
- " t->forw, tt, t->st);",
- " printf(\" %%s [abit=%%d,adepth=%%d,\", ",
- " t->tp, now._a_t, A_depth);",
- " printf(\"tau=%%d,%%d]\\n\", ",
- " trpt->tau, (trpt-1)->tau);",
- "#endif",
- "#ifndef NOREDUCE",
- " /* pass the proviso tags */",
- " if ((trpt->tau&8) /* rv or atomic */",
- " && (trpt->tau&16))",
- " (trpt-1)->tau |= 16;",
- "#ifdef SAFETY",
- " if ((trpt->tau&8) /* rv or atomic */",
- " && (trpt->tau&64))",
- " (trpt-1)->tau |= 64;",
- "#endif",
- "#endif",
- " depth--; trpt--;",
- "#ifdef NIBIS",
- " (trans[ot][tt])->om = m; /* head of list */",
- "#endif",
- " /* i.e., not set if rv fails */",
- " if (m)",
- " {",
- "#if defined(VERI) && !defined(NP)",
- " if (II == 0 && verbose && !reached[ot][t->st])",
- " {",
- " printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
- " depth, t->st, src_claim [t->st]);",
- " fflush(stdout);",
- " }",
- "#endif",
- " reached[ot][t->st] = 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 */",
- "#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)", /* NEW: 1 iso 0 */
- " now._cnt[now._a_t&1] = 2;", /* NEW: 2 iso 1*/
- "#endif",
- " now._cnt[now._a_t&1] += 1;",
- "#ifdef VERBOSE",
- " printf(\"%%3d: 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 = From+1;",
- " } } }",
- "#endif",
- "#ifdef VERI",
- " if (II == 0) break; /* never claim */",
- "#endif",
- " } /* all processes */",
- "#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)", /* NEW: 1 iso 0 */
- " now._cnt[now._a_t&1] = 2;", /* NEW: 2 iso 1 */
- "#endif",
- " now._cnt[now._a_t&1] += 1;",
- "#ifdef VERBOSE",
- " printf(\"%%3d: proc -- fairness \", depth);",
- " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
- " now._cnt[now._a_t&1], now._a_t);",
- "#endif",
- " trpt->o_pm &= ~32;",
- " }",
- "#ifndef NP",
- /* 12/97 non-progress cycles cannot be created
- * by stuttering extension, here or elsewhere
- */
- " if (fairness",
- " && n == 0 /* nobody moved */",
- "#ifdef VERI",
- " && !(trpt->tau&4) /* in program move */",
- "#endif",
- " && !(trpt->tau&8) /* not an atomic one */",
- "#ifdef OTIM",
- " && ((trpt->tau&1) || endstate())",
- "#else",
- "#ifdef ETIM",
- " && (trpt->tau&1) /* already tried timeout */",
- "#endif",
- "#endif",
- "#ifndef NOREDUCE",
- " /* see below */",
- " && !((trpt->tau&32) && (n == 0 || (trpt->tau&16)))",
- "#endif",
- " && now._cnt[now._a_t&1] > 0) /* needed more procs */",
- " { depth++; trpt++;",
- " trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
- " trpt->bup.oval = now._cnt[now._a_t&1];",
- " now._cnt[now._a_t&1] = 1; /* gh,1/99 was 0 */",
- "#ifdef VERI",
- " trpt->tau = 4;",
- "#else",
- " trpt->tau = 0;",
- "#endif",
- " From = now._nr_pr-1; To = BASE;",
- "#if defined(VERBOSE) || defined(CHECK)",
- " printf(\"%%3d: 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(\"%%3d: 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(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
- " depth, now._a_t);",
- "#endif",
- " }",
- "#endif",
- "#ifndef NOREDUCE",
- "#ifdef SAFETY",
- " /* preselected move - no successors outside stack */",
- " if ((trpt->tau&32) && !(trpt->tau&64))",
- " { From = now._nr_pr-1; To = BASE;",
- "#ifdef DEBUG",
- " printf(\"%%3d: proc %%d UnSelected (n=%%d, tau=%%d)\\n\", ",
- " depth, II+1, n, trpt->tau);",
- "#endif",
- " n = 0; trpt->tau &= ~(16|32|64);",
- " if (II >= BASE) /* II already decremented */",
- " goto Resume;",
- " else",
- " goto Again;",
- " }",
- "#else",
- " /* at least one move that was preselected at this */",
- " /* level, blocked or truncated at the next level */",
- "/* implied: #ifdef FULLSTACK */",
- " if ((trpt->tau&32) && (n == 0 || (trpt->tau&16)))",
- " {",
- "#ifdef DEBUG",
- " printf(\"%%3d: proc %%d UnSelected (n=%%d, tau=%%d)\\n\", ",
- " depth, II+1, n, trpt->tau);",
- "#endif",
- " if (a_cycles && (trpt->tau&16))",
- " { if (!(now._a_t&1))",
- " {",
- "#ifdef DEBUG",
- " printf(\"%%3d: 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 = now._nr_pr-1; To = BASE;",
- " n = 0; trpt->tau &= ~(16|32|64);",
- " goto Again; /* do full search */",
- " } /* else accept reduction */",
- " } else",
- " { From = now._nr_pr-1; To = BASE;",
- " n = 0; trpt->tau &= ~(16|32|64);",
- " if (II >= BASE) /* already decremented */",
- " goto Resume;",
- " else",
- " goto Again;",
- " } }",
- "/* #endif */",
- "#endif",
- "#endif",
- " if (n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
- " {",
- "#ifdef DEBUG",
- " printf(\"%%3d: 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",
- "#ifdef OTIM",
- " || endstate()",
- "#endif",
- " || depth >= maxdepth-1) goto Done;",
- /* new location of atomic block code -- BEFORE timeout */
- " if ((trpt->tau&8) && !(trpt->tau&4))",
- " { trpt->tau &= ~(1|8);",
- " /* 1=timeout, 8=atomic */",
- " From = now._nr_pr-1; To = BASE;",
- "#ifdef DEBUG",
- " printf(\"%%3d: atomic step proc %%d \", depth, II);",
- " printf(\"unexecutable\\n\");",
- "#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",
- " 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",
- " printf(\"%%d: req timeout\\n\",",
- " depth);",
- "#endif",
- " (trpt-1)->tau |= 2; /* request */",
- " goto Up;",
- " }",
- "#else",
- "#ifdef DEBUG",
- " printf(\"%%d: timeout\\n\", depth);",
- "#endif",
- " trpt->tau |= 1;",
- " goto Again;",
- "#endif",
- " }",
- "#endif",
- /* old location of atomic block code */
- "BreakOut:",
- "#ifdef VERI",
- "#ifndef NOSTUTTER",
- #if 1
- " if (!(trpt->tau&4))",
- #else
- /* visser's example shows this is insufficient: */
- " if ((now._a_t&1) && !(trpt->tau&4))",
- #endif
- " { trpt->tau |= 4; /* claim stuttering */",
- " trpt->tau |= 128; /* stutter mark */",
- "#ifdef DEBUG",
- " printf(\"%%d: claim stutter\\n\", depth);",
- "#endif",
- " goto Stutter;",
- " }",
- "#endif",
- "#else",
- " if (!noends && !a_cycles && !endstate())",
- " uerror(\"invalid endstate\");",
- "#endif",
- " }",
- "Done:",
- " if (!(trpt->tau&8)) /* not in atomic seqs */",
- " {",
- "#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)",
- " {",
- "#ifdef VERBOSE",
- " printf(\"Consider check %%d %%d...\\n\",",
- " now._a_t, now._cnt[0]);",
- "#endif",
- " if ((now._a_t&2) /* A-bit */",
- " && (now._cnt[0] == 1))",
- " checkcycles();",
- " } else",
- "#endif",
- " if (a_cycles && (trpt->o_pm&2))",
- " checkcycles();",
- " }",
- "#endif",
- "#ifndef MA",
- "#if defined(FULLSTACK) || defined(CNTRSTACK)",
- "#ifdef VERI",
- " if (boq == -1",
- " && (((trpt->tau&4) && !(trpt->tau&128))",
- " || ( (trpt-1)->tau&128)))",
- "#else",
- " if (boq == -1)",
- "#endif",
- " {",
- "#ifdef DEBUG2",
- "#if defined(FULLSTACK)",
- " printf(\"%%d: zapping %%u (%%d)\\n\",",
- " depth, trpt->ostate,",
- " (trpt->ostate)?trpt->ostate->tagged:0);",
- "#endif",
- "#endif",
- " onstack_zap();",
- " }",
- "#endif",
- "#else",
- "#ifdef VERI",
- " if (boq == -1",
- " && (((trpt->tau&4) && !(trpt->tau&128))",
- " || ( (trpt-1)->tau&128)))",
- "#else",
- " if (boq == -1)",
- "#endif",
- " {",
- "#ifdef DEBUG",
- " printf(\"%%d: zapping\\n\", depth);",
- "#endif",
- " onstack_zap();",
- "#ifndef NOREDUCE",
- " if (trpt->proviso)",
- " gstore((char *) &now, vsize, 1);",
- "#endif",
- " }",
- "#endif",
- " }",
- " if (depth > 0) goto Up;",
- "}\n",
- "void",
- "assert(int a, char *s, int ii, int tt, Trans *t)",
- "{",
- " if (!a && !noasserts)",
- " { char bad[1024];",
- " if (strlen(s) > 999) s[999] = '\\0';",
- " sprintf(bad, \"assertion violated %%s\", s);",
- " depth++; trpt++;",
- " if (t) {",
- " trpt->pr = ii;",
- " trpt->st = tt;",
- " trpt->o_t = t;",
- " } else {",
- " trpt->pr = (trpt-1)->pr;",
- " trpt->st = (trpt-1)->st;",
- " trpt->o_t = (trpt-1)->o_t;",
- " }",
- " uerror(bad);",
- " depth--; trpt--;",
- " }",
- "}",
- "#ifndef NOBOUNDCHECK",
- "int",
- "Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
- "{",
- " assert((x >= 0 && x < y), \"- invalid array index\",",
- " a1, a2, a3);",
- " return x;",
- "}",
- "#endif",
- "void",
- "wrap_stats(void)",
- "{ double a, b;",
- "#ifdef COVEST",
- " extern double log(double);\n",
- "#endif",
- " if (nShadow>0)",
- " printf(\"%%8g states, stored (%%g visited)\\n\",",
- " nstates - nShadow, nstates);",
- " else",
- " printf(\"%%8g states, stored\\n\", nstates);",
- " printf(\"%%8g states, matched\\n\", truncs);",
- "#ifdef CHECK",
- " printf(\"%%8g matches within stack\\n\",truncs2);",
- "#endif",
- " if (nShadow>0)",
- " printf(\"%%8g transitions (= visited+matched)\\n\",",
- " nstates+truncs);",
- " else",
- " printf(\"%%8g transitions (= stored+matched)\\n\",",
- " nstates+truncs);",
- " printf(\"%%8g atomic steps\\n\", nlinks);",
- " if (nlost) printf(\"%%g lost messages\\n\", (double)nlost);",
- "#ifdef BITSTATE",
- "#ifdef CHECK",
- " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
- "#endif",
- " a = (double) (1<<(ssize-3)); a = 8.*a; /* avoid overflow on << */",
- " b = nstates+1.;",
- "#ifdef COVEST",
- " printf(\"coverage estimate: %%0.1f%%%%\\n\",",
- " (100.*b)/(log(1. - b / a)/log(1. - 1. / a)));",
- "#endif",
- " printf(\"hash factor: %%g \", a/b);",
- " if (!single)",
- " { if (a/b > 100.)",
- "#ifdef COVEST",
- " printf(\"(good confidence estimate)\\n\");",
- " else if (a/b > 10.)",
- " printf(\"(medium confidence estimate)\\n\");",
- " else",
- " printf(\"(low confidence estimate, best if >100)\\n\");",
- " } else",
- " { if (a/b > 1000.)",
- " printf(\"(good confidence estimate)\\n\");",
- " else if (a/b > 100.)",
- " printf(\"(medium confidence estimate)\\n\");",
- " else",
- " printf(\"(low confidence estimate (1-bit hash), best if >1000)\\n\");",
- "#else",
- " printf(\"(expected coverage: >= 99.9%%%% on avg.)\\n\");",
- " else if (a/b > 10.)",
- " printf(\"(expected coverage: >= 98%%%% on avg.)\\n\");",
- " else",
- " printf(\"(best coverage if >100)\\n\");",
- " } else",
- " { if (a/b > 1000.)",
- " printf(\"(expected coverage: >= 99.9%%%% on avg.)\\n\");",
- " else if (a/b > 100.)",
- " printf(\"(expected coverage: >= 98%%%% on avg.)\\n\");",
- " else",
- " printf(\"(best coverage (1-bit hash) if >1000)\\n\");",
- "#endif",
- " }",
- "#else",
- " printf(\"hash conflicts: %%g (resolved)\\n\", hcmp);",
- "#endif",
- "}",
- "void",
- "wrapup(void)",
- "{ double nr1, nr2, nr3 = 0.0, nr4;",
- "#ifndef BITSTATE",
- " double tmp_nr;",
- "#endif",
- " signal(SIGINT, SIG_DFL);",
- " printf(\"(%%s)\\n\", Version);",
- " if (!done) printf(\"Warning: Search not completed\\n\");",
- "#ifdef SC",
- " (void) unlink((const char *)stackfile);",
- "#endif",
- "#ifndef NOREDUCE",
- " printf(\" + Partial Order Reduction\\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\", Source);",
- "#endif",
- "#endif",
- "#ifdef CHECK",
- "#ifdef FULLSTACK",
- " printf(\" + FullStack Matching\\n\");",
- "#endif",
- "#ifdef CNTRSTACK",
- " printf(\" + CntrStack Matching\\n\");",
- "#endif",
- "#endif",
- "#ifdef BITSTATE",
- " printf(\"\\nBit statespace search for:\\n\");",
- "#else",
- "#ifdef HC",
- " printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
- "#else",
- " printf(\"\\nFull statespace search for:\\n\");",
- "#endif",
- "#endif",
- "#ifdef EVENT_TRACE",
- "#ifdef NEGATED_TRACE",
- " printf(\"\tnotrace assertion \t+\\n\");",
- "#else",
- " printf(\"\ttrace assertion \t+\\n\");",
- "#endif",
- "#endif",
- "#ifdef VERI",
- " printf(\"\tnever-claim \t+\\n\");",
- " printf(\"\tassertion violations\t\");",
- " if (noasserts)",
- " printf(\"- (disabled by -A flag)\\n\");",
- " else",
- " printf(\"+ (if within scope of claim)\\n\");",
- "#else",
- "#ifdef NOCLAIM",
- " printf(\"\tnever-claim \t- (not selected)\\n\");",
- "#else",
- " printf(\"\tnever-claim \t- (none specified)\\n\");",
- "#endif",
- " printf(\"\tassertion violations\t\");",
- " if (noasserts)",
- " printf(\"- (disabled by -A flag)\\n\");",
- " else",
- " printf(\"+\\n\");",
- "#endif",
- "#ifndef SAFETY",
- "#ifdef NP",
- " printf(\"\tnon-progress cycles \t\");",
- "#else",
- " printf(\"\tacceptance cycles \t\");",
- "#endif",
- " if (a_cycles)",
- " printf(\"+ (fairness %%sabled)\\n\",",
- " fairness?\"en\":\"dis\");",
- " else printf(\"- (not selected)\\n\");",
- "#else",
- " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");",
- "#endif",
- "#ifdef VERI",
- " printf(\"\tinvalid endstates\t- \");",
- " printf(\"(disabled by \");",
- " if (noends)",
- " printf(\"-E flag)\\n\\n\");",
- " else",
- " printf(\"never-claim)\\n\\n\");",
- "#else",
- " printf(\"\tinvalid endstates\t\");",
- " if (noends)",
- " printf(\"- (disabled by -E flag)\\n\\n\");",
- " else",
- " printf(\"+\\n\\n\");",
- "#endif",
- " printf(\"State-vector %%d byte, depth reached %%d\", ",
- " hmax, mreached);",
- " printf(\", errors: %%d\\n\", errors);",
- "#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();",
- " printf(\"(max size 2^%%d states\", ssize);",
- "#ifdef CHECK",
- " printf(\", stackframes: %%d/%%d)\\n\\n\", smax, svmax);",
- " printf(\"stats: fa %%d, fh %%d, zh %%d, zn %%d - \",",
- " Fa, Fh, Zh, Zn);",
- " printf(\"check %%d holds %%d\\n\", Ccheck, Cholds);",
- " printf(\"stack stats: puts %%d, probes %%d, zaps %%d\\n\",",
- " PUT, PROBE, ZAPS);",
- "#else",
- " printf(\")\\n\\n\");",
- "#endif",
- "#ifdef MEMCNT",
- "#if defined(BITSTATE) || !defined(NOCOMP)",
- " nr1 = (nstates-nShadow)*",
- " (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
- " nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
- "#ifndef BITSTATE",
- "#if !defined(MA) || defined(COLLAPSE)",
- " nr3 = (double) (1<<ssize)*sizeof(struct H_el *);",
- "#endif",
- "#else",
- " nr3 = (double) (1<<(ssize-3));",
- "#ifdef CNTRSTACK",
- " nr3 += (double) (1<<(ssize-3));",
- "#endif",
- "#ifdef FULLSTACK",
- " overhead += (double) (1<<(ssize-3))*sizeof(struct H_el *);",
- "#endif",
- "#endif",
- " nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
- " + (double) (smax * (sizeof(Stack) + Maxbody));",
- " overhead = overhead - nr2 + fragment;",
- "#ifndef MA",
- " if (memcnt < nr1+nr2+nr3+nr4)",
- "#else",
- " if (1)",
- "#endif",
- " { printf(\"Stats on memory usage (in Megabytes):\\n\");",
- " printf(\"%%-6.3f\tequivalent memory usage for states\",",
- " nr1/1000000.);",
- " printf(\" (stored*(State-vector + overhead))\\n\");",
- "#ifdef BITSTATE",
- " printf(\"%%-6.3f\tmemory used for hash-array (-w%%d)\\n\",",
- " nr3/1000000., ssize);",
- "#else",
- " tmp_nr = memcnt-nr3-nr4-(overhead+nr2-fragment);",
- " if (tmp_nr < 0.0) tmp_nr = 0.;",
- " printf(\"%%-6.3f\tactual memory usage for states\",",
- " tmp_nr/1000000.);",
- " printf(\" (\");",
- " if (tmp_nr > 0.)",
- " { if (tmp_nr > nr1)",
- " printf(\"unsuccessful \");",
- " printf(\"compression: %%.2f%%%%)\\n\",",
- " (100.0*tmp_nr)/nr1);",
- " } else",
- " printf(\"less than 1k)\\n\");",
- "#ifndef MA",
- " if (tmp_nr > 0.)",
- " { printf(\"\tState-vector as stored = %%.0f byte\",",
- " (tmp_nr)/(nstates-nShadow) -",
- " (double) (sizeof(struct H_el) - sizeof(unsigned)));",
- " printf(\" + %%d byte overhead\\n\",",
- " sizeof(struct H_el)-sizeof(unsigned));",
- " }",
- "#endif",
- "#if !defined(MA) || defined(COLLAPSE)",
- " printf(\"%%-6.3f\tmemory used for hash-table (-w%%d)\\n\",",
- " nr3/1000000., ssize);",
- "#endif",
- "#endif",
- " printf(\"%%-6.3f\tmemory used for DFS stack (-m%%d)\\n\",",
- " nr2/1000000., maxdepth);",
- " /* remainder is mem used for proc and chan stacks */",
- " /* and memory lost in allocator (=fragment) */",
- " printf(\"%%-6.3f\ttotal actual memory usage\\n\\n\",",
- " memcnt/1000000.);",
- " } else",
- "#endif",
- " printf(\"%%-6.3f\tmemory usage (Mbyte)\\n\\n\",",
- " memcnt/1000000.);",
- "#endif",
- "#ifdef COLLAPSE",
- " printf(\"nr of templates: [ globals procs chans ]\\n\");",
- " printf(\"collapse counts: [ \");",
- " { int i; for (i = 0; i < 256+2; i++)",
- " if (ncomps[i] != 0)",
- " printf(\"%%d \", ncomps[i]);",
- " printf(\"]\\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",
- " exit(0);",
- "}\n",
- "void",
- "stopped(int arg)",
- "{ printf(\"Interrupted\\n\");",
- " wrapup();",
- "}",
- "void",
- "d_hash(uchar *Cp, int Om)",
- "{ long z = (long) HASH_CONST[HASH_NR];",
- " long *q, *r, h;",
- " long m, n;",
- "#ifndef BCOMP",
- " uchar *cp = Cp;",
- " long om = (long) Om;",
- "#else",
- " uchar *cp = (uchar *) &comp_now;",
- " char *vv = (char *) Cp;",
- " char *v = (char *) &comp_now;",
- " long i, om;",
- " for (i = 0; i < Om; i++, vv++)",
- " if (!Mask[i]) *v++ = *vv;",
- " for (i = 0; i < WS-1; i++)",
- " *v++ = 0;",
- " v -= i;",
- " om = v - (char *)&comp_now;",
- "#endif",
- " h = (om+sizeof(long)-1)/sizeof(long);",
- " m = n = -1;",
- " q = r = (long *) cp;",
- " r += (long) h;",
- " do {",
- " if (m < 0)",
- " { m += m;",
- " m ^= z;",
- " } else",
- " m += m;",
- " m ^= *q++;",
- " if (n < 0)",
- " { n += n;",
- " n ^= z;",
- " } else",
- " n += n;",
- " n ^= *--r;",
- " } while (--h > 0);",
- " J1 = (m ^ (m>>(8*sizeof(long)-ssize)))&mask;",
- " J2 = (n ^ (n>>(8*sizeof(long)-ssize)))&mask;",
- "#if 0",
- " j3 = (1<<(J1&7)); j1 = J1>>3;",
- " j4 = (1<<(J2&7)); j2 = J2>>3;",
- "#endif",
- " if (!single)",
- " { j3 = (1<<(J1&7)); j2 = J2>>3;",
- " j4 = (1<<(J2&7)); j1 = J1>>3;",
- " } else /* single-bit address */",
- " { J1 = J1^J2; /* use all bits */",
- " j3 = (1<<(J1&7)); j2 = J1>>3;",
- " j1 = 0; j4 = 1;",
- " }",
- "}\n",
- "#ifdef HYBRID_HASH",
- "long",
- "#else",
- "void",
- "#endif",
- "s_hash(uchar *cp, int om) /* single forward hash */",
- "{ long z = (long) HASH_CONST[HASH_NR];",
- " long *q;",
- " long h;",
- " long m = -1;",
- " h = (om+sizeof(long)-1)/sizeof(long);",
- " q = (long *) cp;",
- " do {",
- " if (m < 0)",
- " { m += m;",
- " m ^= z;",
- " } else",
- " m += m;",
- " m ^= *q++;",
- " } while (--h > 0);",
- "#ifdef BITSTATE",
- " if (S_Tab == H_tab)",
- " j1 = (m^(m>>(8*sizeof(long)-(ssize-3))))&((1<<(ssize-3))-1);",
- " else",
- "#endif",
- " j1 = (m^(m>>(8*sizeof(long)-ssize)))&mask;",
- "#ifdef HYBRID_HASH",
- "#ifndef BITSTATE",
- " if ((om&(sizeof(void *)-1)) == 1) /* very badly aligned */",
- " { /* use last data byte as first byte of hash */",
- " j1 = (j1 & (~255)) | cp[om-1];",
- " return om-1; /* perfect alignment */",
- " }",
- "#endif",
- " return om;",
- "#endif",
- "}",
- "#if defined(HC) || (defined(BITSTATE) && defined(LC))",
- "void",
- "r_hash(uchar *cp, int om) /* reverse direction from s_hash */",
- "{ long z = (long) HASH_CONST[HASH_NR];",
- " long *r, h, n = -1;",
- " h = (om+sizeof(long)-1)/sizeof(long);",
- " r = (long *) cp + h;",
- " do {",
- " if (n < 0)",
- " { n += n;",
- " n ^= z;",
- " } else",
- " n += n;",
- " n ^= *--r;",
- " } while (--h > 0);",
- " J3 = n; /* the compressed state vector */",
- " n = -1; /* forward hash for hash_table index */",
- " h = (om+sizeof(long)-1)/sizeof(long);",
- " r = (long *) cp;",
- " do {",
- " if (n < 0)",
- " { n += n;",
- " n ^= z;",
- " } else",
- " n += n;",
- " n ^= *r++;",
- " } while (--h > 0);",
- " J4 = n; /* more bits, when needed */",
- " j1 = (n^(n>>(8*sizeof(long)-ssize)))&((1<<(ssize-3))-1);",
- "}",
- "#endif",
- "unsigned long TMODE = 0666; /* default permission bits for trail files */",
- "int",
- "main(int argc, char *argv[])",
- "{ void to_compile(void);\n",
- " efd = stderr; /* default */",
- " while (argc > 1 && argv[1][0] == '-')",
- " { switch (argv[1][1]) {",
- "#ifndef SAFETY",
- "#ifdef NP",
- " case 'a': fprintf(efd, \"error: -a disabled\");",
- " usage(efd); break;",
- "#else",
- " case 'a': a_cycles = 1; break;",
- "#endif",
- "#endif",
- " case 'A': noasserts = 1; break;",
- " case 'c': upto = atoi(&argv[1][2]); break;",
- " case 'd': state_tables++; break;",
- " case 'e': every_error = 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",
- " case 'h': if (!argv[1][2]) usage(efd); else",
- " HASH_NR = atoi(&argv[1][2])%%33; break;",
- " case 'I': iterative = 2; every_error = 1; break;",
- " case 'i': iterative = 1; every_error = 1; break;",
- " case 'J': like_java = 1; break; /* Klaus Havelund */",
- "#ifndef SAFETY",
- "#ifdef NP",
- " case 'l': a_cycles = 1; break;",
- "#else",
- " case 'l': fprintf(efd, \"error: -l disabled\");",
- " usage(efd); break;",
- "#endif",
- "#endif",
- " case 'm': maxdepth = atoi(&argv[1][2]); break;",
- " case 'n': no_rck = 1; break;",
- "#ifdef SVDUMP",
- " case 'p': vprefix = atoi(&argv[1][2]); break;",
- "#endif",
- " case 'q': strict = 1; break;",
- " case 'R': Nrun = atoi(&argv[1][2]); break;",
- " case 's': single = 1; break;",
- " case 'T': TMODE = 0444; break;",
- " case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;",
- " case 'V': printf(\"Generated by %%s\\n\", Version);",
- " to_compile(); exit(0); break;",
- " case 'v': verbose = 1; break;",
- " case 'w': ssize = atoi(&argv[1][2]); break;",
- " case 'X': efd = stdout; break;",
- " default : usage(efd); break;",
- " }",
- " argc--; argv++;",
- " }",
- " if (iterative && TMODE != 0666)",
- " { TMODE = 0666;",
- " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
- " }",
- "#ifdef SC",
- " omaxdepth = maxdepth;",
- " hiwater = HHH = maxdepth-10;",
- " DDD = HHH/2;",
- " if (!stackfile)",
- " { stackfile = (char *) emalloc(strlen(Source)+4+1);",
- " sprintf(stackfile, \"%%s._s_\", Source);",
- " }",
- " if (iterative)",
- " { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
- " exit(1);",
- " }",
- "#endif",
- "#if defined(MERGED) && defined(PEG)",
- " fprintf(efd, \"error: to allow -DPEG use: spin -o3 -a %%s\\n\", Source);",
- " fprintf(efd, \" to turn off transition merge optimization\\n\");",
- " exit(1);",
- "#endif",
- "#ifdef HC",
- "#ifdef NOCOMP",
- " fprintf(efd, \"error: cannot combine -DHC and -DNOCOMP\\n\");",
- " exit(1);",
- "#endif",
- "#ifdef BITSTATE",
- " fprintf(efd, \"error: cannot combine -DHC and -DBITSTATE\\n\");",
- " exit(1);",
- "#endif",
- "#endif",
- "#if defined(SAFETY) && defined(NP)",
- " fprintf(efd, \"error: cannot combine -DNP and -DSAFETY\\n\");",
- " exit(1);",
- "#endif",
- "#ifdef MA",
- "#ifdef BITSTATE",
- " fprintf(efd, \"error: cannot combine -DMA and -DBITSTATE\\n\");",
- " exit(1);",
- "#endif",
- " if (MA <= 0)",
- " { fprintf(efd, \"usage: -DMA=N with N > 0 and < VECTORSZ\\n\");",
- " exit(1);",
- " }",
- "#endif",
- "#ifdef COLLAPSE",
- "#if defined(BITSTATE)",
- " fprintf(efd, \"error: cannot combine -DBITSTATE and -DCOLLAPSE\\n\");",
- " exit(1);",
- "#endif",
- "#if defined(NOCOMP)",
- " fprintf(efd, \"error: cannot combine -DNOCOMP and -DCOLLAPSE\\n\");",
- " exit(1);",
- "#endif",
- "#endif",
- " if (maxdepth <= 0 || ssize <= 0) 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\");",
- " exit(1);",
- " }",
- "#endif",
- "#if defined(NOCOMP) && !defined(BITSTATE)",
- " if (a_cycles)",
- " { fprintf(efd, \"error: -DNOCOMP voids -l and -a\\n\");",
- " exit(1);",
- " }",
- "#endif",
- "#ifdef MEMLIM", /* MEMLIM setting takes precedence */
- " memlim = (double) MEMLIM * (double) (1<<20); /* size in Mbyte */",
- "#else",
- "#ifdef MEMCNT",
- "#if MEMCNT<31",
- " memlim = (double) (1<<MEMCNT);",
- "#else",
- " memlim = (double) (1<<30);",
- " memlim *= (double) (1<<(MEMCNT-30));",
- "#endif",
- "#endif",
- "#endif",
- "#ifndef BITSTATE",
- " if (Nrun > 1) HASH_NR = Nrun - 1;",
- "#endif",
- " if (Nrun < 1 || Nrun > 32)",
- " { fprintf(efd, \"error: invalid arg for -R\\n\");",
- " usage(efd);",
- " }",
- "#ifndef SAFETY",
- " if (fairness && !a_cycles)",
- " { fprintf(efd, \"error: -f requires -a or -l\\n\");",
- " usage(efd);",
- " }",
- "#if ACCEPT_LAB==0",
- " if (a_cycles)",
- "#ifndef VERI",
- " { fprintf(efd, \"error: no accept labels defined \");",
- " fprintf(efd, \"in model (for option -a)\\n\");",
- " usage(efd);",
- " }",
- "#else",
- " { fprintf(efd, \"warning: no explicit accept labels \");",
- " fprintf(efd, \"defined in model (for -a)\\n\");",
- " }",
- "#endif",
- "#endif",
- "#endif",
- "#if !defined(NOREDUCE)",
- "#if defined(HAS_ENABLED)",
- " fprintf(efd, \"error: reduced search precludes \");",
- " fprintf(efd, \"use of 'enabled()'\\n\");",
- " exit(1);",
- "#endif",
- "#if defined(HAS_PCVALUE)",
- " fprintf(efd, \"error: reduced search precludes \");",
- " fprintf(efd, \"use of 'pcvalue()'\\n\");",
- " exit(1);",
- "#endif",
- "#if defined(HAS_BADELSE)",
- " fprintf(efd, \"error: reduced search precludes \");",
- " fprintf(efd, \"using 'else' combined with i/o stmnts\\n\");",
- " exit(1);",
- "#endif",
- "#if defined(HAS_LAST)",
- " fprintf(efd, \"error: reduced search precludes \");",
- " fprintf(efd, \"use of _last\\n\");",
- " exit(1);",
- "#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, could make p.o. reduction\\n\");",
- " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
- "#endif",
- "#endif",
- "#if !defined(REACH) && !defined(BITSTATE)",
- " if (iterative != 0)",
- " fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
- "#endif",
- "#if defined(BITSTATE) && defined(REACH)",
- " fprintf(efd, \"warning: -DREACH voided by -DBITSTATE\\n\");",
- "#endif",
- "#if defined(FULLSTACK) && defined(CNTRSTACK)",
- " fprintf(efd, \"error: cannot combine\");",
- " fprintf(efd, \" -DFULLSTACK and -DCNTRSTACK\\n\");",
- " exit(1);",
- "#endif",
- "#ifdef VERI",
- "#if ACCEPT_LAB>0",
- " if (!a_cycles && !state_tables)",
- " { fprintf(efd, \"warning: never-claim + accept-labels \");",
- " fprintf(efd, \"requires -a flag to fully verify\\n\");",
- " }",
- "#endif",
- "#endif",
- "#ifndef SAFETY",
- " if (!a_cycles && !state_tables)",
- " { fprintf(efd, \"hint: this search is more efficient \");",
- " fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
- " }",
- "#ifndef NOCOMP",
- " if (!a_cycles)",
- " S_A = 0;",
- " else",
- " { if (!fairness)",
- " S_A = 1; /* _a_t */",
- "#ifndef NOFAIR",
- " else /* _a_t and _cnt[NFAIR] */",
- " S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;",
- " /* -2 because first two uchars in now are masked */",
- "#endif",
- " }",
- "#endif",
- "#endif",
- " signal(SIGINT, stopped);",
- " mask = ((1<<ssize)-1); /* hash init */",
- " trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
- " trail++; /* protect trpt-1 refs at depth 0 */",
- "#ifdef SVDUMP",
- " if (vprefix > 0)",
- " { char nm[64];",
- " sprintf(nm, \"%%s.svd\", Source);",
- " if ((svfd = creat(nm, 0666)) <= 0)",
- " { fprintf(efd, \"couldn't create %%s\\n\", nm);",
- " vprefix = 0;",
- " } }",
- "#endif",
- "#ifdef RANDSTOR",
- " srand(123);",
- "#endif",
- "#if SYNC>0 && ASYNC==0",
- " set_recvs();",
- "#endif",
- " run();",
- " done = 1;",
- " wrapup();",
- " return 0;",
- "}\n",
- "void",
- "usage(FILE *fd)",
- "{",
- " 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-cN stop at Nth error \");",
- " fprintf(fd, \"(defaults to -c1)\\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 endstates\\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 choose other hash-function 1..32\\n\");",
- " fprintf(fd, \"\t-i search for shortest path to error\\n\");",
- " fprintf(fd, \"\t-I like -i, but approximate and faster\\n\");",
- " fprintf(fd, \"\t-J reverse eval order of nested unlesses\\n\");",
- "#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",
- " fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
- " fprintf(fd, \"\t-n no listing of unreached states\\n\");",
- "#ifdef SVDUMP",
- " fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
- "#endif",
- " fprintf(fd, \"\t-q require empty chans in valid endstates\\n\");",
- "#ifdef BITSTATE",
- " fprintf(fd, \"\t-RN repeat run Nx with N \");",
- " fprintf(fd, \"[1..32] independent hash functions\\n\");",
- "#endif",
- " fprintf(fd, \"\t-s 1-bit hashing (default is 2-bit)\\n\");",
- " fprintf(fd, \"\t-T create trail files in read-only mode\\n\");",
- " fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
- " fprintf(fd, \"\t-V print SPIN version number\\n\");",
- " fprintf(fd, \"\t-v verbose -- filenames in unreached state listing\\n\");",
- " fprintf(fd, \"\t-wN hashtable of 2^N entries\");",
- " fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
- " exit(1);",
- "}",
- "",
- "char *",
- "Malloc(unsigned long n)",
- "{ char *tmp;",
- "#ifdef MEMCNT",
- " if (memcnt+ (double) n > memlim) goto err;",
- "#endif",
- "#ifdef PC",
- " tmp = (char *) malloc(n);",
- "#else",
- " tmp = (char *) sbrk(n);",
- "#endif",
- " if (tmp == (char *) -1L)", /* was: if ((int)tmp == -1) */
- " {",
- "err:",
- " printf(\"pan: out of memory\\n\");",
- "#ifdef MEMCNT",
- " printf(\"\t%%g bytes used\\n\", memcnt);",
- " printf(\"\t%%g bytes more needed\\n\", (double) n);",
- " printf(\"\t%%g bytes limit (2^MEMCNT)\\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",
- " wrapup();",
- " }",
- "#ifdef MEMCNT",
- " memcnt += n;",
- "#endif",
- " return tmp;",
- "}",
- "",
- "#define CHUNK (100*VECTORSZ)",
- "",
- "char *",
- "emalloc(unsigned long n) /* never released or reallocated */",
- "{ char *tmp;",
- " if (n == 0)",
- " return (char *) NULL;",
- " if (n&(sizeof(void *)-1)) /* for proper alignment */",
- " n += sizeof(void *)-(n&(sizeof(void *)-1));",
- " if (left < (long) n)",
- " { grow = (n < CHUNK) ? CHUNK : n;",
- "#ifdef PC",
- " have = Malloc(grow);",
- "#else",
- " /* gcc's sbrk can give non-aligned result */",
- " grow += sizeof(void *); /* allow realignment */",
- " have = Malloc(grow);",
- " if (((unsigned) have)&(sizeof(void *)-1))",
- " { have += (long) (sizeof(void *) ",
- " - (((unsigned) have)&(sizeof(void *)-1)));",
- " grow -= sizeof(void *);",
- " }",
- "#endif",
- " fragment += (double) left;",
- " left = grow;",
- " }",
- " tmp = have;",
- " have += (long) n;",
- " left -= (long) n;",
- " memset(tmp, 0, n);",
- " return tmp;",
- "}",
- "void",
- "Uerror(char *str)",
- "{ /* always fatal */",
- " uerror(str);",
- " wrapup();",
- "}\n",
- "#if defined(MA) && !defined(SAFETY)",
- "int",
- "Unwind(void)",
- "{ Trans *t; char ot, m; short tt; short II, i;\n",
- " uchar oat = now._a_t;",
- " now._a_t &= ~(1|16|32);",
- " memcpy((char *) &comp_now, (char *) &now, vsize);",
- " now._a_t = oat;",
- "Up:",
- "#ifdef SC",
- " trpt = getframe(depth);",
- "#endif",
- "#ifdef VERBOSE",
- " printf(\"%%d State: \", depth);",
- " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
- " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
- " printf(\"\\n\");",
- "#endif",
- "#ifndef NOFAIR",
- " if (trpt->o_pm&128) /* fairness alg */",
- " { now._cnt[now._a_t&1] = trpt->bup.oval;",
- " depth--;",
- "#ifdef SC",
- " trpt = getframe(depth);",
- "#else",
- " trpt--;",
- "#endif",
- " goto Q999;",
- " }",
- "#endif",
- "#ifdef HAS_LAST",
- "#ifdef VERI",
- " { int d; Trail *trl;",
- " now._last = 0;",
- " for (d = 1; d < depth; d++)",
- " { trl = getframe(depth-d); /* was trl = (trpt-d); */",
- " if (trl->pr != 0)",
- " { now._last = trl->pr - BASE;",
- " break;",
- " } } }",
- "#else",
- " now._last = (depth<1)?0:(trpt-1)->pr;",
- "#endif",
- "#endif",
- "#ifdef EVENT_TRACE",
- " now._event = trpt->o_event;",
- "#endif",
- " if ((now._a_t&1) && depth <= A_depth)",
- " { now._a_t &= ~(1|16|32);",
- " if (fairness) now._a_t |= 2; /* ? */",
- " A_depth = 0;",
- " goto CameFromHere; /* checkcycles() */",
- " }",
- " t = trpt->o_t;",
- " ot = trpt->o_ot; II = trpt->pr;",
- " tt = trpt->o_tt; this = pptr(II);",
- " m = do_reverse(t, II, trpt->o_m);",
- "#ifdef VERBOSE",
- " printf(\"%%3d: proc %%d \", depth, II);",
- " printf(\"reverses %%d, %%d to %%d,\",",
- " t->forw, tt, t->st);",
- " printf(\" %%s [abit=%%d,adepth=%%d,\", ",
- " t->tp, now._a_t, A_depth);",
- " printf(\"tau=%%d,%%d] <unwind>\\n\", ",
- " trpt->tau, (trpt-1)->tau);",
- "#endif",
- " depth--;",
- "#ifdef SC",
- " trpt = getframe(depth);",
- "#else",
- " trpt--;",
- "#endif",
- " reached[ot][t->st] = 1;",
- " ((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",
- "void",
- "uerror(char *str)",
- "{ static char laststr[256];\n",
- " if (strcmp(str, laststr))",
- " printf(\"pan: %%s (at depth %%d)\\n\", str,",
- " (depthfound==-1)?depth:depthfound);",
- " strcpy(laststr, str);",
- " errors++;",
- " if (every_error != 0",
- " || errors == upto)",
- " {",
- "#if defined(MA) && !defined(SAFETY)",
- " if (strstr(str, \" cycle\"))",
- " { int od = depth;",
- " depthfound = Unwind();",
- " depth = od;",
- " }",
- "#endif",
- " putrail();",
- "#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 (iterative != 0 && maxdepth > 0)",
- " { maxdepth = (iterative == 1)?(depth-1):(depth/2);",
- " warned = 1;",
- " printf(\"pan: reducing search depth to %%d\\n\",",
- " maxdepth);",
- " } else if (errors >= upto && upto != 0)",
- " wrapup();",
- " depthfound = -1; /* tripakis */",
- "}\n",
- "void",
- "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
- "{ int i, m=0;\n",
- "#ifdef VERI",
- " if (M == VERI && !verbose) return;",
- "#endif",
- " printf(\"unreached in proctype %%s\\n\", procname[M]);",
- " for (i = 1; i < N; i++)",
- " if (which[i] == 0 && trans[M][i])",
- " xrefsrc((int) src[i], mp, M, i);",
- " else",
- " m++;",
- " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
- "}\n",
- "void",
- "xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
- "{ Trans *T; int j;",
- " for (T = trans[M][i]; T; T = T->nxt)",
- " if (T && T->tp)",
- " { printf(\"\\tline %%d\", lno);",
- " if (verbose)",
- " for (j = 0; j < sizeof(mp); j++)",
- " if (i >= mp[j].from && i <= mp[j].upto)",
- " { printf(\", \\\"%%s\\\"\", mp[j].fnm);",
- " break;",
- " }",
- " printf(\", state %%d\", i);",
- " if (strcmp(T->tp, \"\") != 0)",
- " printf(\", \\\"%%s\\\"\", T->tp);",
- " else if (stopstate[M][i])",
- " printf(\", -endstate-\");",
- " printf(\"\\n\");",
- " }",
- "}\n",
- "void",
- "putrail(void)",
- "{ int fd; long i, j;",
- " Trail *trl;",
- " char snap[64], fnm[256];",
- " if (iterative == 0 && Nr_Trails++ > 0)",
- " sprintf(fnm, \"%%s%%d.%%s\",",
- " TrailFile, Nr_Trails, tprefix);",
- " else",
- " sprintf(fnm, \"%%s.%%s\",",
- " TrailFile, tprefix);",
- " if ((fd = creat(fnm, TMODE)) <= 0)",
- " { printf(\"cannot create %%s\\n\", fnm);",
- " perror(\"cause\");",
- " return;",
- " }",
- "#ifdef VERI",
- " sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
- " write(fd, snap, strlen(snap));",
- "#endif",
- "#ifdef MERGED",
- " sprintf(snap, \"-4:-4:-4\\n\");",
- " write(fd, snap, strlen(snap));",
- "#endif",
- " for (i = 1; i <= depth; i++)",
- " { if (i == depthfound+1)",
- " write(fd, \"-1:-1:-1\\n\", 9);",
- " trl = getframe(i);",
- " if (trl->o_pm&128) continue;",
- " sprintf(snap, \"%%d:%%d:%%d\\n\", ",
- " i, trl->pr, trl->o_t->t_id);",
- " j = strlen(snap);",
- " if (write(fd, snap, j) != j)",
- " { printf(\"pan: error writing %%s\\n\", fnm);",
- " close(fd);",
- " wrapup();",
- " }",
- " }",
- " printf(\"pan: wrote %%s\\n\", fnm);",
- " close(fd);",
- "}\n",
- "void",
- "sv_save(char *won) /* 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",
- " svtack->o_delta = vsize; /* don't compress */",
- " memcpy((char *)(svtack->body), won, vsize);",
- "#ifdef DEBUG",
- " 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",
- " if (vsize != svtack->o_delta)",
- " Uerror(\"sv_restor\");",
- " if (!svtack->lst)",
- " Uerror(\"error: v_restor\");",
- " svtack = svtack->lst;",
- "#ifdef DEBUG",
- " printf(\" sv_restor\\n\");",
- "#endif",
- "}\n",
- "void",
- "p_restor(int h)",
- "{ int i; char *z = (char *) &now;\n",
- " proc_offset[h] = stack->o_offset;",
- " proc_skip[h] = stack->o_skip;",
- "#ifndef XUSAFE",
- " p_name[h] = stack->o_name;",
- "#endif",
- "#ifndef NOCOMP",
- " for (i = vsize + stack->o_skip; i > vsize; i--)",
- " Mask[i-1] = 1; /* align */",
- "#endif",
- " vsize += stack->o_skip;",
- " memcpy(z+vsize, stack->body, stack->o_delta);",
- " vsize += stack->o_delta;",
- "#ifndef NOVSZ",
- " now._vsz = vsize;",
- "#endif",
- "#ifndef NOCOMP",
- " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
- " Mask[vsize - i] = 1; /* pad */",
- " Mask[proc_offset[h]] = 1; /* _pid */",
- "#endif",
- " if (BASE > 0 && h > 0)",
- " ((P0 *)pptr(h))->_pid = h-BASE;",
- " else",
- " ((P0 *)pptr(h))->_pid = h;",
- " i = stack->o_delqs;",
- " now._nr_pr += 1;",
- " if (!stack->lst) /* debugging */",
- " Uerror(\"error: p_restor\");",
- " stack = stack->lst;",
- " this = pptr(h);",
- " while (i-- > 0)",
- " q_restor();",
- "}\n",
- "void",
- "q_restor(void)",
- "{ int k; char *z = (char *) &now;\n",
- " q_offset[now._nr_qs] = stack->o_offset;",
- " q_skip[now._nr_qs] = stack->o_skip;",
- "#ifndef XUSAFE",
- " q_name[now._nr_qs] = stack->o_name;",
- "#endif",
- " vsize += stack->o_skip;",
- " memcpy(z+vsize, stack->body, stack->o_delta);",
- " vsize += stack->o_delta;",
- "#ifndef NOVSZ",
- " now._vsz = vsize;",
- "#endif",
- " now._nr_qs += 1;",
- "#ifndef NOCOMP",
- " k = stack->o_offset - stack->o_skip;",
- "#if SYNC",
- " if (q_zero(now._nr_qs)) k += stack->o_delta;",
- "#endif",
- " for ( ; k < stack->o_offset; k++)",
- " Mask[k] = 1; /* align */",
- "#endif",
- " if (!stack->lst) /* debugging */",
- " Uerror(\"error: q_restor\");",
- " stack = stack->lst;",
- "}",
- "typedef struct IntChunks {",
- " int *ptr;",
- " struct IntChunks *nxt;",
- "} IntChunks;",
- "IntChunks *filled_chunks[128];",
- "IntChunks *empty_chunks[128];",
- "int *",
- "grab_ints(int nr)",
- "{ IntChunks *z;",
- " if (nr >= 128) 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;",
- "}",
- #if 0
- "void",
- "p_q_restor(int h, int K)",
- "{ int k = K-1;",
- " if (!stack || !stack->lst || !stack->lst->lst)",
- " Uerror(\"error: p_q_restor\");",
- " /* restore globals */",
- " memcpy((char *)&now, stack->body, sizeof(State)-VECTORSZ);",
- " stack = stack->lst;",
- " memcpy((char *) qptr(k), stack->body, Maxbody);",
- " stack = stack->lst;",
- "#if SYNC",
- " boq = stack->o_boq;",
- "#endif",
- " memcpy((char *) pptr(h), stack->body, Maxbody);",
- " stack = stack->lst;",
- "}",
- "Stack *",
- "p_q_frame(void)",
- "{ if (!stack->nxt)",
- " { stack->nxt = (Stack *)",
- " emalloc(sizeof(Stack));",
- " stack->nxt->body = ",
- " emalloc(Maxbody*sizeof(char));",
- " stack->nxt->lst = stack;",
- " smax++;",
- " }",
- " return stack->nxt;",
- "}",
- "void",
- "p_q_save(int h, int K)",
- "{ int k = K-1;",
- " stack = p_q_frame();",
- " memcpy(stack->body, (char *)pptr(h), Maxbody);",
- "#if SYNC",
- " stack->o_boq = boq;",
- "#endif",
- " stack = p_q_frame();",
- " memcpy(stack->body, (char *)qptr(k), Maxbody);",
- " /* save globals */",
- " stack = p_q_frame();",
- " memcpy(stack->body, (char *)&now, sizeof(State)-VECTORSZ);",
- "}",
- "void",
- "bup_q(int h, int K)",
- "{",
- "#if VECTORSZ<=1024",
- " sv_save((char *)&now);",
- "#else",
- " p_q_save(h, K);",
- "#endif",
- "}",
- "void",
- "unbup_q(int h, int K)",
- "{",
- "#if VECTORSZ<=1024",
- " sv_restor();",
- "#else",
- " p_q_restor(h, K);",
- "#endif",
- "}",
- #endif
- "int",
- "delproc(int sav, int h)",
- "{ int d, i=0, o_vsize = vsize;\n",
- " if (h+1 != (int) now._nr_pr) return 0;\n",
- " 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];",
- " stack->o_skip = proc_skip[h];",
- "#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 = now._nr_pr - 1;",
- " memset((char *)pptr(h), 0, d);",
- " vsize -= proc_skip[h];",
- "#ifndef NOVSZ",
- " now._vsz = vsize;",
- "#endif",
- "#ifndef NOCOMP",
- " for (i = vsize; i < o_vsize; i++)",
- " Mask[i] = 0; /* reset */",
- "#endif",
- " return 1;",
- "}\n",
- "void",
- "delq(int sav)",
- "{ int h = now._nr_qs - 1;",
- " int d = vsize - q_offset[now._nr_qs - 1];",
- "#ifndef NOCOMP",
- " int k, o_vsize = vsize;",
- "#endif",
- " 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 = q_offset[h];",
- " stack->o_skip = q_skip[h];",
- "#ifndef XUSAFE",
- " stack->o_name = q_name[h];",
- "#endif",
- " stack->o_delta = d;",
- " memcpy(stack->body, (char *)qptr(h), d);",
- " }",
- " vsize = q_offset[h];",
- " now._nr_qs = now._nr_qs - 1;",
- " memset((char *)qptr(h), 0, d);",
- " vsize -= q_skip[h];",
- "#ifndef NOVSZ",
- " now._vsz = vsize;",
- "#endif",
- "#ifndef NOCOMP",
- " for (k = vsize; k < o_vsize; k++)",
- " Mask[k] = 0; /* reset */",
- "#endif",
- "}\n",
- "int",
- "qs_empty(void)",
- "{ int i;",
- " for (i = 0; i < (int) now._nr_qs; i++)",
- " { if (q_sz(i) > 0)",
- " return 0;",
- " }",
- " return 1;",
- "}\n",
- "int",
- "endstate(void)",
- "{ int i; P0 *ptr;",
- " for (i = BASE; i < (int) now._nr_pr; i++)",
- " { ptr = (P0 *) pptr(i);",
- " if (!stopstate[ptr->_t][ptr->_p])",
- " return 0;",
- " }",
- " if (strict) return qs_empty();",
- "#if defined(EVENT_TRACE) && !defined(OTIM)",
- " if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
- " { printf(\"pan: event_trace not completed\\n\");",
- " return 0;",
- " }",
- "#endif",
- " return 1;",
- "}\n",
- "#ifndef SAFETY",
- "void",
- "checkcycles(void)",
- "{ uchar o_a_t = now._a_t;",
- "#ifndef NOFAIR",
- " uchar o_cnt = now._cnt[1];",
- "#endif",
- "#ifdef FULLSTACK",
- "#ifndef MA",
- " struct H_el *sv = trpt->ostate; /* save */",
- "#else",
- " uchar prov = trpt->proviso; /* save */",
- "#endif",
- "#endif",
- "#ifdef DEBUG",
- " { int i; uchar *v = (uchar *) &now;",
- " printf(\" set Seed state \");",
- "#ifndef NOFAIR",
- " if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
- " now._cnt[0], now._cnt[1], now._nr_pr);",
- "#endif",
- " /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */",
- " printf(\"\\n\");",
- " }",
- " printf(\"%%d: cycle check starts\\n\", depth);",
- "#endif",
- " now._a_t |= (1|16|32);",
- " /* 1 = 2nd DFS; (16|32) to help hasher */",
- "#ifndef NOFAIR",
- #if 0
- " if (fairness)",
- " { now._a_t &= ~2; /* pre-apply Rule 3 */",
- " now._cnt[1] = 0;", /* reset both a-bit and cnt=0 */
- " /* avoid matching seed on claim stutter on this state */",
- " }",
- #else
- " now._cnt[1] = now._cnt[0];",
- #endif
- "#endif",
- " memcpy((char *)&A_Root, (char *)&now, vsize);",
- " A_depth = depthfound = depth;",
- " new_state(); /* start 2nd DFS */",
- " now._a_t = o_a_t;",
- "#ifndef NOFAIR",
- " now._cnt[1] = o_cnt;",
- "#endif",
- " A_depth = 0; depthfound = -1;",
- "#ifdef DEBUG",
- " printf(\"%%d: cycle check returns\\n\", depth);",
- "#endif",
- "#ifdef FULLSTACK",
- "#ifndef MA",
- " trpt->ostate = sv; /* restore */",
- "#else",
- " trpt->proviso = prov;",
- "#endif",
- "#endif",
- "}",
- "#endif\n",
- "#if defined(FULLSTACK) && defined(BITSTATE)",
- "struct H_el *Free_list = (struct H_el *) 0;",
- "void",
- "onstack_init(void)",
- "{ S_Tab = (struct H_el **)",
- " emalloc((1<<(ssize-3))*sizeof(struct H_el *));",
- "}",
- "struct H_el *",
- "grab_state(int n)",
- "{ struct H_el *v, *last = 0;",
- " if (H_tab == S_Tab)",
- " { for (v = Free_list; v && v->tagged >= n; v=v->nxt)",
- " { if (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 && v->tagged >= n)",
- " goto gotcha;",
- " ngrabs++;",
- " }",
- " return (struct H_el *)",
- " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
- "}\n",
- "#else",
- "#define grab_state(n) (struct H_el *) \\",
- " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
- "#endif",
- "#ifdef COLLAPSE",
- "unsigned long",
- "#ifdef HYBRID_HASH",
- "ordinal(char *v, long N, short tp) /* store components */",
- "{ struct H_el *tmp, *ntmp; long n, m;",
- " struct H_el *olst = (struct H_el *) 0;",
- " n = s_hash((uchar *)v, N);",
- "#else",
- "ordinal(char *v, long n, short tp)",
- "{ struct H_el *tmp, *ntmp; long m;",
- " struct H_el *olst = (struct H_el *) 0;",
- " s_hash((uchar *)v, n);",
- "#endif",
- " tmp = H_tab[j1];",
- " if (!tmp)",
- " { tmp = grab_state(n);",
- " H_tab[j1] = tmp;",
- " } else",
- " for ( ;; olst = tmp, tmp = tmp->nxt)",
- " { m = memcmp(((char *)&(tmp->state)), v, n);",
- " if (n == tmp->ln)",
- " {",
- " if (m == 0)",
- " goto done;",
- " if (m < 0)",
- " {",
- "Insert: ntmp = grab_state(n);",
- " ntmp->nxt = tmp;",
- " if (!olst)",
- " H_tab[j1] = 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;",
- " }",
- " m = ++ncomps[tp];",
- "#ifdef FULLSTACK",
- " tmp->tagged = m;",
- "#else",
- " tmp->st_id = m;",
- "#endif",
- " memcpy(((char *)&(tmp->state)), v, n);",
- " tmp->ln = n;",
- "done:",
- "#ifdef FULLSTACK",
- " return tmp->tagged;",
- "#else",
- " return tmp->st_id;",
- "#endif",
- "}",
- "",
- "int",
- "compress(char *vin, int nin) /* collapse compression */",
- "{ char *w, *v = (char *) &comp_now;",
- " int i, j;",
- " unsigned long n;",
- " static char *x;",
- " static uchar nbytes[513]; /* 1 + 256 + 256 */",
- " static unsigned short nbytelen;",
- " long col_q(int, char *);",
- " long col_p(int, char *);",
- "#ifndef SAFETY",
- " if (a_cycles)",
- " *v++ = now._a_t;",
- "#ifndef NOFAIR",
- " if (fairness)",
- " for (i = 0; i < NFAIR; i++)",
- " *v++ = now._cnt[i];",
- "#endif",
- "#endif",
- " nbytelen = 0;",
- "#ifndef JOINPROCS",
- " for (i = 0; i < (int) now._nr_pr; i++)",
- " { n = col_p(i, (char *) 0);",
- " 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++;",
- " }",
- "#else",
- " x = scratch;",
- " for (i = 0; i < (int) now._nr_pr; i++)",
- " x += col_p(i, x);",
- " n = ordinal(scratch, x-scratch, 2); /* procs */",
- " *v++ = n&255;",
- " nbytes[nbytelen] = 0;",
- " if (n >= (1<<8))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>8)&255;",
- " }",
- " if (n >= (1<<16))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>16)&255;",
- " }",
- " if (n >= (1<<24))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>24)&255;",
- " }",
- " nbytelen++;",
- "#endif",
- "#ifdef SEPQS",
- " for (i = 0; i < (int) now._nr_qs; i++)",
- " { n = col_q(i, (char *) 0);",
- " nbytes[nbytelen] = 0;",
- " *v++ = n&255;",
- " if (n >= (1<<8))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>8)&255;",
- " }",
- " if (n >= (1<<16))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>16)&255;",
- " }",
- " if (n >= (1<<24))",
- " { nbytes[nbytelen]++;",
- " *v++ = (n>>24)&255;",
- " }",
- " nbytelen++;",
- " }",
- "#endif",
- "#ifdef NOVSZ",
- " /* 3 = _a_t, _nr_pr, _nr_qs */",
- " w = (char *) &now + 3 * sizeof(uchar);",
- "#ifndef NOFAIR",
- " w += NFAIR;",
- "#endif",
- "#else",
- "#if VECTORSZ<65536",
- " w = (char *) &(now._vsz) + sizeof(unsigned short);",
- "#else",
- " w = (char *) &(now._vsz) + sizeof(unsigned long);",
- "#endif",
- "#endif",
- " x = scratch;",
- " *x++ = now._nr_pr;",
- " *x++ = now._nr_qs;",
- " if (now._nr_qs > 0 && qptr(0) < pptr(0))",
- " n = qptr(0) - (uchar *) w;",
- " else",
- " n = pptr(0) - (uchar *) w;",
- " j = w - (char *) &now;",
- " for (i = 0; i < n; i++, w++)",
- " if (!Mask[j++]) *x++ = *w;",
- "#ifndef SEPQS",
- " for (i = 0; i < (int) now._nr_qs; i++)",
- " x += col_q(i, x);",
- "#endif",
- " x--;",
- " for (i = 0, j = 6; i < nbytelen; i++)",
- " { if (j == 6)",
- " { j = 0;",
- " *(++x) = 0;",
- " } else",
- " j += 2;",
- " *x |= (nbytes[i] << j);",
- " }",
- " x++;",
- " for (j = 0; j < WS-1; j++)",
- " *x++ = 0;",
- " x -= j; j = 0;",
- " n = ordinal(scratch, x-scratch, 0); /* globals */",
- " *v++ = n&255;",
- " if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
- " if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
- " if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
- " *v++ = j; /* add last count as a byte */",
- " for (i = 0; i < WS-1; i++)",
- " *v++ = 0;",
- " v -= i;",
- "#if 0",
- " printf(\"collapse %%d -> %%d\\n\",",
- " vsize, v - (char *)&comp_now);",
- "#endif",
- " return v - (char *)&comp_now;",
- "}",
- "#else",
- "#if !defined(NOCOMP)",
- "int",
- "compress(char *vin, int n) /* default compression */",
- "{",
- "#ifdef HC",
- " int delta = 0;",
- " r_hash((uchar *)vin, n); /* sets J3 and J4 */",
- "#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 *) &J3, sizeof(long));",
- " delta += sizeof(long);",
- "#if HC>0",
- " memcpy((char *) &comp_now + delta, (char *) &J4, HC);",
- " delta += HC;",
- "#endif",
- " return delta;",
- "#else",
- " char *vv = vin;",
- " char *v = (char *) &comp_now;",
- " int i;",
- " for (i = 0; i < n; i++, vv++)",
- " if (!Mask[i]) *v++ = *vv;",
- " for (i = 0; i < WS-1; i++)",
- " *v++ = 0;",
- " v -= i;",
- "#if 0",
- " printf(\"compress %%d -> %%d\\n\",",
- " n, v - (char *)&comp_now);",
- "#endif",
- " return v - (char *)&comp_now;",
- "#endif",
- "}",
- "#endif",
- "#endif",
- "#if defined(FULLSTACK) && defined(BITSTATE)",
- "void",
- "onstack_zap(void)",
- "{ struct H_el *v, *w, *last = 0;",
- " struct H_el **tmp = H_tab;",
- " char *nv; int n, m;\n",
- " 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))",
- "#ifdef HYBRID_HASH",
- " n = ",
- "#endif",
- " s_hash((uchar *)nv, n);",
- "#endif",
- " H_tab = tmp;",
- " for (v = S_Tab[j1]; v; Zh++, last=v, v=v->nxt)",
- " { m = memcmp(&(v->state), nv, n);",
- " if (m == 0)",
- " goto Found;",
- " if (m < 0)",
- " break;",
- " }",
- "NotFound:",
- " Uerror(\"stack out of wack - zap\");",
- " return;",
- "Found:",
- " ZAPS++;",
- " if (last)",
- " last->nxt = v->nxt;",
- " else",
- " S_Tab[j1] = v->nxt;",
- " v->tagged = n;",
- "#if !defined(NOREDUCE) && !defined(SAFETY)",
- " v->proviso = 0;",
- "#endif",
- " v->nxt = last = (struct H_el *) 0;",
- " for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
- " { if (w->tagged <= n)",
- " { if (last)",
- " { v->nxt = w->nxt;",
- " last->nxt = v;",
- " } else",
- " { v->nxt = Free_list;",
- " Free_list = v;",
- " }",
- " return;",
- " }",
- " if (!w->nxt)",
- " { w->nxt = v;",
- " return;",
- " } }",
- " Free_list = v;",
- "}",
- "void",
- "onstack_put(void)",
- "{ struct H_el **tmp = H_tab;",
- " H_tab = S_Tab;",
- " if (hstore((char *)&now, vsize, 3) != 0)",
- "#if defined(BITSTATE) && defined(LC)",
- " printf(\"pan: warning, double stack entry\\n\");",
- "#else",
- " Uerror(\"cannot happen - unstack_put\");",
- "#endif",
- " H_tab = tmp;",
- " trpt->ostate = Lstate;",
- " PUT++;",
- "}",
- "int",
- "onstack_now(void)",
- "{ struct H_el *tmp;",
- " struct H_el **tmp2 = H_tab;",
- " char *v; int n, m = 1;\n",
- " 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))",
- "#ifdef HYBRID_HASH",
- " n = ",
- "#endif",
- " s_hash((uchar *)v, n);",
- "#endif",
- " H_tab = tmp2;",
- " for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
- " { m = memcmp(((char *)&(tmp->state)),v,n);",
- " if (m <= 0)",
- " { Lstate = tmp;",
- " break;",
- " } }",
- " PROBE++;",
- " return (m == 0);",
- "}",
- "#endif",
- "#ifndef BITSTATE",
- "void",
- "hinit(void)",
- "{",
- "#ifdef MA",
- "#ifdef R_XPT",
- " { void r_xpoint(void);",
- " r_xpoint();",
- " }",
- "#else",
- " dfa_init(MA+a_cycles);",
- "#endif",
- "#endif",
- "#if !defined(MA) || defined(COLLAPSE)",
- " H_tab = (struct H_el **)",
- " emalloc((1<<ssize)*sizeof(struct H_el *));",
- "#endif",
- "}",
- "#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",
- "#ifndef NOCOMP",
- " printf(\"\t State: \");",
- " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
- " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
- "#endif",
- " printf(\"\\n\tVector: \");",
- " for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
- " printf(\"\\n\");",
- "#endif",
- "}",
- "#endif",
- "#ifdef MA",
- "int",
- "gstore(char *vin, int nin, uchar pbit)",
- "{ int n = compress(vin, nin);",
- " int i, j=0;",
- " static uchar Info[MA+1];",
- " 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 > maxgs) maxgs = n;",
- " for (i = 0; i < n; i++)",
- " Info[i] = ((uchar *)&comp_now)[i];",
- " for ( ; i < MA-1; i++)",
- " Info[i] = 0;",
- " Info[MA-1] = pbit;",
- " if (a_cycles) /* place _a_t at the end */",
- " { Info[MA] = Info[0]; Info[0] = 0; }",
- " if (!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))",
- " {",
- "#ifdef VERBOSE",
- " printf(\"intersected 1st dfs stack\\n\");",
- "#endif",
- " return 3;",
- " } } }",
- "#ifdef VERBOSE",
- " printf(\"new state\\n\");",
- "#endif",
- " return 0; /* new state */",
- " }",
- "#ifdef FULLSTACK",
- " if (pbit == 0)",
- " { Info[MA-1] = 1; /* proviso bit */",
- " trpt->proviso = dfa_member(MA-1);",
- " Info[MA-1] = 4; /* off-stack bit */",
- " if (dfa_member(MA-1)) {",
- "#ifdef VERBOSE",
- " printf(\"old state\\n\");",
- "#endif",
- " return 1; /* off-stack */",
- " } else {",
- "#ifdef VERBOSE",
- " printf(\"on-stack\\n\");",
- "#endif",
- " return 2; /* on-stack */",
- " }",
- " }",
- "#endif",
- "#ifdef VERBOSE",
- " printf(\"old state\\n\");",
- "#endif",
- " return 1; /* old state */",
- "}",
- "#endif",
- "#if defined(BITSTATE) && defined(LC)",
- "int",
- "compact_stack(char *vin, int n)", /* special case of HC4 */
- "{ int delta = 0;",
- " r_hash((uchar *)vin, n); /* sets J3 and J4 */",
- "#ifndef SAFETY",
- " delta++; /* room for state[0] |= 128 */",
- "#endif",
- " memcpy((char *) &comp_now + delta, (char *) &J3, sizeof(long));",
- " delta += sizeof(long);",
- " memcpy((char *) &comp_now + delta, (char *) &J4, sizeof(long));",
- " delta += sizeof(long); /* use all available bits */",
- " return delta;",
- "}",
- "#endif",
- "int",
- "hstore(char *vin, int nin, short xx)",
- "{ struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;",
- " char *v; int n, m=0;",
- "#ifdef NOCOMP",
- "#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;",
- " n = compress(vin, nin);",
- "#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))",
- "#ifdef HYBRID_HASH",
- " n = ",
- "#endif",
- " s_hash((uchar *)v, n);",
- "#endif",
- " tmp = H_tab[j1];",
- " if (!tmp)",
- " { tmp = grab_state(n);",
- " H_tab[j1] = tmp;",
- " } else",
- " { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
- " { /* skip the _a_t and the _cnt bytes */",
- "#ifdef COLLAPSE",
- " if (tmp->ln != 0)",
- " { if (!tmp->nxt) goto Append;",
- " continue;",
- " }",
- "#endif",
- " m = memcmp(((char *)&(tmp->state)) + S_A, ",
- " v + S_A, n - S_A);",
- " if (m == 0) {",
- "#ifdef SAFETY",
- "#define wasnew 0",
- "#else",
- " int wasnew = 0;",
- "#endif",
- "#ifndef SAFETY",
- "#ifndef NOCOMP",
- " if (S_A)",
- " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
- " { wasnew = 1; nShadow++;",
- " ((char *)&(tmp->state))[0] |= V_A;",
- " }",
- "#ifndef NOFAIR",
- " if (S_A > NFAIR)",
- " { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */",
- " unsigned ci, bp; /* index, bit pos */",
- " ci = (now._cnt[now._a_t&1] / 8);",
- " bp = (now._cnt[now._a_t&1] - 8*ci);",
- " if (now._a_t&1) /* use tail-bits in _cnt */",
- " { ci = (NFAIR - 1) - ci;",
- " bp = 7 - bp; /* bp = 0..7 */",
- " }",
- " ci++; /* skip over _a_t */",
- " bp = 1 << bp; /* the bit mask */",
- " if ((((char *)&(tmp->state))[ci] & bp)==0)",
- " { if (!wasnew)",
- " { wasnew = 1;",
- " nShadow++;",
- " }",
- " ((char *)&(tmp->state))[ci] |= bp;",
- " }",
- " }",
- " /* else: wasnew == 0, i.e., old state */",
- "#endif",
- " }",
- "#endif",
- "#endif",
- "#ifdef FULLSTACK",
- "#ifndef SAFETY", /* or else wasnew == 0 */
- " if (wasnew)",
- " { Lstate = tmp;",
- " tmp->tagged |= V_A;",
- " if ((now._a_t&1)",
- " && (tmp->tagged&A_V)",
- " && depth > A_depth)",
- " {",
- "intersect:",
- "#ifdef CHECK",
- " printf(\"1st dfs-stack intersected on state %%d+\\n\",",
- " (int) tmp->st_id);",
- "#endif",
- " return 3;",
- " }",
- "#ifdef CHECK",
- " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
- "#endif",
- "#ifdef DEBUG",
- " dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
- "#endif",
- " return 0;",
- " } else",
- "#endif",
- " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
- " { Lstate = tmp;",
- "#ifndef SAFETY",
- " /* already on current dfs stack */",
- " /* but may also be on 1st dfs stack */",
- " if ((now._a_t&1)",
- " && (tmp->tagged&A_V)",
- " && depth > A_depth",
- /* new (Zhang's example) */
- "#ifndef NOFAIR",
- " && (!fairness || now._cnt[1] <= 1)",
- "#endif",
- " )",
- " goto intersect;",
- "#endif",
- "#ifdef CHECK",
- " printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
- "#endif",
- "#ifdef DEBUG",
- " dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
- "#endif",
- " return 2; /* match on stack */",
- " }",
- "#else",
- " if (wasnew)",
- " {",
- "#ifdef CHECK",
- " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
- "#endif",
- "#ifdef DEBUG",
- " dumpstate(1, (char *)&(tmp->state), n, 0);",
- "#endif",
- " return 0;",
- " }",
- "#endif",
- "#ifdef CHECK",
- " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
- "#endif",
- "#ifdef DEBUG",
- " dumpstate(0, (char *)&(tmp->state), n, 0);",
- "#endif",
- "#ifdef REACH",
- " if (tmp->D > depth)",
- " { tmp->D = depth;",
- "#ifdef CHECK",
- " printf(\"\t\tReVisiting (from smaller depth)\\n\");",
- "#endif",
- " nstates--;",
- " return 0;",
- " }",
- "#endif",
- " return 1; /* match outside stack */",
- " } else if (m < 0)",
- " { /* insert state before tmp */",
- " ntmp = grab_state(n);",
- " ntmp->nxt = tmp;",
- " if (!olst)",
- " H_tab[j1] = ntmp;",
- " else",
- " olst->nxt = ntmp;",
- " tmp = ntmp;",
- " break;",
- " } else if (!tmp->nxt)",
- " { /* append after tmp */",
- "Append: tmp->nxt = grab_state(n);",
- " tmp = tmp->nxt;",
- " break;",
- " } }",
- " }",
- "#ifdef CHECK",
- " tmp->st_id = (unsigned) nstates;",
- "#ifdef BITSTATE",
- " printf(\" Push state %%d\\n\", ((int) nstates) - 1);",
- "#else",
- " printf(\" New state %%d\\n\", (int) nstates);",
- "#endif",
- "#endif",
- "#ifdef REACH",
- " tmp->D = depth;",
- "#endif",
- "#ifndef SAFETY",
- "#ifndef NOCOMP",
- " if (S_A)",
- " { v[0] = V_A;",
- "#ifndef NOFAIR",
- " if (S_A > NFAIR)",
- " { unsigned ci, bp; /* as above */",
- " ci = (now._cnt[now._a_t&1] / 8);",
- " bp = (now._cnt[now._a_t&1] - 8*ci);",
- " if (now._a_t&1)",
- " { ci = (NFAIR - 1) - ci;",
- " bp = 7 - bp; /* bp = 0..7 */",
- " }",
- " v[1+ci] = 1 << bp;",
- " }",
- "#endif",
- " }",
- "#endif",
- "#endif",
- " 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 = tmp;",
- "#else",
- "#ifdef DEBUG",
- " dumpstate(-1, v, n, 0);",
- "#endif",
- "#endif",
- " return 0;",
- "}",
- "#endif",
- "#include TRANSITIONS",
- "void",
- "do_reach(void)",
- "{",
- 0,
- };
|