diff -rN -U3 ../murphi-3.1/include/mu_hash.C ./include/mu_hash.C --- ../murphi-3.1/include/mu_hash.C 1999-11-03 16:59:06.000000000 -0500 +++ ./include/mu_hash.C 2005-05-16 12:35:11.000000000 -0400 @@ -98,6 +98,82 @@ // rectly) // - otherwise, buffer oldvec is used { +#ifdef TRIPLE_MURPHI + /* + * based on Bob Jenkins LOOKUP2 hash function from 1996 + * see: http://www.burtleburtle.net/bob/ + */ + +#define mix(a,b,c) \ + { a -= b; a -= c; a ^= (c>>13); \ + b -= c; b -= a; b ^= (a<<8); \ + c -= a; c -= b; c ^= (b>>13); \ + a -= b; a -= c; a ^= (c>>12); \ + b -= c; b -= a; b ^= (a<<16); \ + c -= a; c -= b; c ^= (b>>5); \ + a -= b; a -= c; a ^= (c>>3); \ + b -= c; b -= a; b ^= (a<<10); \ + c -= a; c -= b; c ^= (b>>15); \ + } + +typedef unsigned long int ub4; + + if (args->use_jenkins.value) { + unsigned long a, b, c, len; + BIT_BLOCK *k = s->bits; + + if (sizeof(*k) != 1) Error.Notrace("Bad BIT_BLOCK size."); + + a = hashmatrix[0]; + b = hashmatrix[1]; + c = hashmatrix[2]; + + len = BLOCKS_IN_WORLD; + + while (len >= 12) { + a += (k[0] +((ub4)k[1]<<8) +((ub4)k[2]<<16) +((ub4)k[3]<<24)); + b += (k[4] +((ub4)k[5]<<8) +((ub4)k[6]<<16) +((ub4)k[7]<<24)); + c += (k[8] +((ub4)k[9]<<8) +((ub4)k[10]<<16)+((ub4)k[11]<<24)); + mix(a,b,c); + k += 12; len -= 12; + } + + switch(len) { + case 11: c+=((ub4)k[10]<<24); + case 10: c+=((ub4)k[9]<<16); + case 9 : c+=((ub4)k[8]<<8); + case 8 : b+=((ub4)k[7]<<24); + case 7 : b+=((ub4)k[6]<<16); + case 6 : b+=((ub4)k[5]<<8); + case 5 : b+=k[4]; + case 4 : a+=((ub4)k[3]<<24); + case 3 : a+=((ub4)k[2]<<16); + case 2 : a+=((ub4)k[1]<<8); + case 1 : a+=k[0]; + /* case 0: nothing left to add */ + } + mix(a,b,c); + +#ifdef ALIGN + s->hashkeys[0] = c; + s->hashkeys[1] = b; + s->hashkeys[2] = a; + if (!valid) +#endif + { + key[0] = c; + key[1] = b; + key[2] = a; + } + +#ifdef ALIGN + return s->hashkeys; +#else + return key; +#endif + + } +#endif //TRIPLE_MURPHI register unsigned long l0, l1, l2; register unsigned char qq; register unsigned char *q=s->bits, *qp; @@ -125,7 +201,12 @@ } do { +#ifdef ORIGINAL if (qq = *qp ^ *q) +#else // gets rid of a warning: + qq = *qp ^ *q; + if (qq) +#endif // ORIGINAL { mask = 1; for (i=ind; i 0) { // compute from est_states and mem + if (num_bits.value > 0) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tIgnoring -b%lu in favor of -e%lu ...\n", num_bits.value, est_states.value); + } + double bps = mem.value * 8.0 / est_states.value; + bps *= 0.998; + num_bits.reset((unsigned long)bps); + if (num_bits.value < 8) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing Bloom filter instead because of predicted memory constraints...\n"); + use_hashc.reset(FALSE); + num_bits.reset((unsigned long)0); + } else if (num_bits.value > 64) { + num_bits.reset(64); + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing 64 bits per compacted state (implementation maximum).....\n"); + } else { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing %lu bits per compacted state...\n", num_bits.value); + } + } else if (num_bits.value < 4) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing Bloom filter instead because of predicted memory constraints...\n"); + use_hashc.reset(FALSE); + /*num_bits.reset(4); + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing minimum compacted state size of 4 bits...\n");*/ + } else if (num_bits.value > 64) { + num_bits.reset(64); + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing maximum compacted state size of 64 bits...\n"); + } + } + if (!use_hashc.value) { // use a Bloom filter + if (est_states.value > 0) { // compute from est_states and mem + if (num_bits.value > 0) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tIgnoring -b%lu in favor of -e%lu ...\n", num_bits.value, est_states.value); + } + double bps = mem.value * 8.0 / est_states.value; + + // below is only used once; doesn't need to be efficient + unsigned long k; + if (bps < 1.13459) k = 1; + else if (bps < 2.34809) k = 2; + else if (bps < 3.64409) k = 3; + else if (bps < 4.98501) k = 4; + else if (bps < 6.35288) k = 5; + else if (bps < 7.73819) k = 6; + else if (bps < 9.13545) k = 7; + else if (bps < 10.5413) k = 8; + else if (bps < 11.9534) k = 9; + else if (bps < 13.3703) k = 10; + else if (bps < 14.7910) k = 11; + else if (bps < 16.2147) k = 12; + else if (bps < 17.6409) k = 13; + else if (bps < 19.0689) k = 14; + else if (bps < 20.4987) k = 15; + else if (bps < 21.9298) k = 16; + else if (bps < 23.3621) k = 17; + else if (bps < 24.7954) k = 18; + else if (bps < 26.2295) k = 19; + else if (bps < 27.6645) k = 20; + else if (bps < 29.1000) k = 21; + else if (bps < 30.5361) k = 22; + else if (bps < 31.9728) k = 23; + else if (bps < 33.4099) k = 24; + else if (bps < 34.8474) k = 25; + else if (bps < 36.2852) k = 26; + else if (bps < 37.7234) k = 27; + else if (bps < 39.1619) k = 28; + else if (bps < 40.6006) k = 29; + else if (bps < 42.0396) k = 30; + else if (bps < 43.4787) k = 31; + else if (bps < 44.9181) k = 32; + else if (bps < 46.3578) k = 33; + else if (bps < 47.7975) k = 34; + else if (bps < 49.2374) k = 35; + else if (bps < 50.6775) k = 36; + else if (bps < 52.1177) k = 37; + else if (bps < 53.5579) k = 38; + else if (bps < 54.9984) k = 39; + else { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing recommended maximum of 40 bits/state in Bloom filter...\n"); + k = 40; + } + if (k < 40) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tSetting %lu bits/state in Bloom filter...\n", k); + } + num_bits.reset(k); + } else if (num_bits.value == 0) { + num_bits.reset(DEFAULT_BITS); + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing default of setting of %lu bits/state in Bloom filter...\n", (unsigned long)DEFAULT_BITS); + } else if (num_bits.value > 40) { + num_bits.reset(40); + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing maximum setting of 40 bits/state in Bloom filter...\n"); + } + } + if (use_jenkins.value) { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing Jenkins hash function...\n"); + } else { + alglen += snprintf(alginfo + alglen, ALGINFO_MAX - alglen, + "\tUsing default (Universal+Diff) hash function...\n"); + } +#endif //TRIPLE_MURPHI + #ifdef HASHC // Uli: do not use trace info file in dfs case if (main_alg.mode == argmain_alg::Verify_dfs) { @@ -404,12 +534,19 @@ Error.Notrace ("Cannot print error trace if you do not specify trace info file."); +#ifdef TRIPLE_MURPHI + if (trace_file.value) { + TraceFile->setBytes(32); + print_trace.reset(TRUE); + } +#else // not TRIPLE_MURPHI // Uli: set number of bytes in trace info file // cannot be done earlier since number of bits may be unknown if (trace_file.value) { TraceFile->setBytes(int(num_bits.value)); print_trace.reset(TRUE); } +#endif //TRIPLE_MURPHI #endif // avoid mixing verbose and progress report @@ -447,6 +584,9 @@ cout << "Run this program with \"-h\" for the list of options.\n"; cout << "\nBugs, questions, and comments should be directed to\n" +#ifdef TRIPLE_MURPHI + << "\"peterd@cc.gatech.edu\", who will direct them, if appropriate, to\n" +#endif //TRIPLE_MURPHI << "\"murphi@verify.stanford.edu\".\n" << "\n" << "Murphi compiler last modified date: " << MURPHI_DATE << '\n' @@ -479,7 +619,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -490,7 +634,11 @@ { sscanf( options->value() + strlen(MEM_MEG_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized memory size. Do '%s -h' for list of valid arguments.", argv[0]); @@ -505,7 +653,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -516,7 +668,11 @@ { sscanf( options->value() + strlen(MEM_K_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized memory size. Do '%s -h' for list of valid arguments.", argv[0]); @@ -526,6 +682,51 @@ }; #ifdef HASHC +#ifdef TRIPLE_MURPHI + if( strcmp( option, ADVANCED_FLAG ) == 0 ) + { + advanced.set(TRUE); + continue; + } + if( strcmp( option, HASHC_FLAG ) == 0 ) + { + use_hashc.set(TRUE); + continue; + } + if ( strncmp(option, EST_STATES_PREFIX, strlen(EST_STATES_PREFIX) ) == 0 ) + { + if ( strlen(option) <= strlen(EST_STATES_PREFIX) ) + // there is a space before the number + { + sscanf( options->nextvalue(), "%s", temp_str ); + if (isdigit(temp_str[0])) + { + sscanf( temp_str, "%lu", &temp ); + options->next(); + } + else + Error.Notrace("Unrecognized state space size estimate.", + argv[0]); + } + else // no space + { + sscanf( options->value() + strlen(EST_STATES_PREFIX), "%s", temp_str ); + if (isdigit(temp_str[0])) + sscanf( temp_str, "%lu", &temp ); + else + Error.Notrace("Unrecognized state space size estimate.", + argv[0]); + } + est_states.set(temp); + continue; + }; + if( strcmp( option, JENKINS_FLAG ) == 0 ) + { + use_jenkins.set(TRUE); + continue; + } + +#endif //TRIPLE_MURPHI // added by Uli if ( strncmp(option, NUM_BITS_PREFIX, strlen(NUM_BITS_PREFIX) ) == 0 ) { @@ -535,7 +736,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { - sscanf( temp_str, "%u", (unsigned long) &temp ); +#ifdef ORIGINAL + sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -546,13 +751,22 @@ { sscanf( options->value() + strlen(NUM_BITS_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) - sscanf( temp_str, "%u", (unsigned long) &temp ); +#ifdef ORIGINAL + sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized number of bits.", argv[0]); } +#ifdef TRIPLE_MURPHI + if (temp<1) + Error.Notrace("Number of bits not allowed."); +#else // not TRIPLE_MURPHI if (temp>64 || temp<1) Error.Notrace("Number of bits not allowed."); +#endif //TRIPLE_MURPHI num_bits.set(temp); continue; }; @@ -584,7 +798,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -595,7 +813,11 @@ { sscanf( options->value() + strlen(LOOPMAX_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized iterator number. Do '%s -h' for list of valid arguments.", argv[0]); @@ -610,7 +832,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -621,7 +847,11 @@ { sscanf( options->value() + strlen(PERM_LIMIT), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized permutation limit number. Do '%s -h' for list of valid arguments.", argv[0]); @@ -638,7 +868,11 @@ { sscanf( options->value() + strlen(TEST1_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized test parameter 1. Do '%s -h' for list of valid arguments.", argv[0]); @@ -655,7 +889,11 @@ { sscanf( options->value() + strlen(TEST2_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized test parameter 2. Do '%s -h' for list of valid arguments.", argv[0]); @@ -700,7 +938,11 @@ sscanf( options->nextvalue(), "%s", temp_str ); if (isdigit(temp_str[0])) { +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL options->next(); } else @@ -711,7 +953,11 @@ { sscanf( options->value() + strlen(MAX_NUM_ERRORS_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized maximum number of errors. Do '%s -h' for list of valid arguments.", argv[0]); @@ -833,7 +1079,11 @@ { sscanf( options->value() + strlen(SYMMETRY_PREFIX), "%s", temp_str ); if (isdigit(temp_str[0])) +#ifdef ORIGINAL sscanf( temp_str, "%u", (unsigned long) &temp ); +#else // fixes a warning: + sscanf( temp_str, "%lu", &temp ); +#endif //ORIGINAL else Error.Notrace("Unrecognized symmetry algorithm. Do '%s -h' for list of valid arguments.", argv[0]); @@ -915,6 +1165,19 @@ << "\t 3 | heuristic small mem canonicaliztion/normalization\n" << "\t (depends on -permlimit)\n" << "\t 4 | heuristic fast normalization (alg 3 with -permlimit 1)\n" +#ifdef TRIPLE_MURPHI +<< "6) 3Murphi State Storage: (default: Bloom filter with " << DEFAULT_BITS + << " bits)\n" +<< "\t-c use hash compaction instead of a Bloom filter.\n" +<< "\t-b number of bits to store per state.\n" +<< "\t-e determine number of bits per state to set based on\n" +<< "\t estimated state space size, .\n" +<< "\t-j use Jenkins hash function instead of Universal+Diff.\n" +<< "\t-d dir write trace info into file dir/" +<< "\t-a output advanced analysis information.\n" + << PROTOCOL_NAME << TRACE_FILE << ".\n" + +#else // not TRIPLE_MURPHI #ifdef HASHC << "6) Hash Compaction: (default: hash compaction with " << DEFAULT_BITS << " bits)\n" @@ -922,6 +1185,7 @@ << "\t-d dir write trace info into file dir/" << PROTOCOL_NAME << TRACE_FILE << ".\n" #endif +#endif //TRIPLE_MURPHI << "\n"; // cout.flush(); /* @@ -1115,6 +1379,9 @@ cout << "??.\n"; break; } } +#ifdef TRIPLE_MURPHI + cout << args->alginfo; +#endif //TRIPLE_MURPHI } // added by Uli @@ -1153,11 +1420,18 @@ { cout << "\n=====================================" << "=====================================\n" +#ifdef TRIPLE_MURPHI + << TRIPLE_MURPHI_VERSION << ", based on " << MURPHI_VERSION << "\n" +#else // not TRIPLE_MURPHI << MURPHI_VERSION << "\n" +#endif //TRIPLE_MURPHI << "Finite-state Concurrent System Verifier.\n" << "\n" << "Copyright (C) 1992 - 1999 by the Board of Trustees of\n" << "Leland Stanford Junior University.\n" +#ifdef TRIPLE_MURPHI + << TRIPLE_MURPHI_COPYRIGHT << "\n" +#endif //TRIPLE_MURPHI << "\n=====================================" << "=====================================\n" << "\nProtocol: " << PROTOCOL_NAME << "\n"; @@ -1224,11 +1498,21 @@ cout << "\nProgress Report:\n\n"; initialized = TRUE; } +#ifdef TRIPLE_MURPHI + cout << " " + << StateSet->NumElts() << " states, " + << Rules->NumRulesFired() << " transitions, " + << SecondsSinceStart() << "s elapsed, " + << StateSet->QueueNumElts() << " in queue, " + << ((StateSet->BytesInQueue() + StateSet->BytesInSet()) / 1048576.0) + << "MB total.\n"; +#else // not TRIPLE_MURPHI cout << "\t" << StateSet->NumElts() << " states explored in " << SecondsSinceStart() << "s, with " << Rules->NumRulesFired() << " rules fired and " << StateSet->QueueNumElts() << " states in the queue.\n"; +#endif //TRIPLE_MURPHI cout.flush(); } } @@ -1245,7 +1529,9 @@ /************************************************************/ void ReportManager::print_summary(bool prob) { +#ifdef ORIGINAL bool exist = FALSE; +#endif //ORIGINAL (unused variable) cout << "\nState Space Explored:\n\n" << "\t" diff -rN -U3 ../murphi-3.1/include/mu_io.h ./include/mu_io.h --- ../murphi-3.1/include/mu_io.h 1999-01-29 02:49:10.000000000 -0500 +++ ./include/mu_io.h 2005-05-16 12:45:30.000000000 -0400 @@ -205,6 +205,10 @@ public: argnum(unsigned long val, char * n) : value(val), initialized(FALSE), name(n) {}; ~argnum() {}; +#ifdef TRIPLE_MURPHI + void reset(unsigned long val) + { initialized = TRUE; value = val; } +#endif //TRIPLE_MURPHI void set(unsigned long val) { if (!initialized) { initialized = TRUE; value = val; } @@ -266,6 +270,14 @@ // Uli: hash compaction options #ifdef HASHC +#ifdef TRIPLE_MURPHI +#define ALGINFO_MAX 500 + char alginfo[ALGINFO_MAX + 1]; + argbool advanced; + argbool use_hashc; + argnum est_states; + argbool use_jenkins; +#endif //TRIPLE_MURPHI argnum num_bits; argbool trace_file; #endif diff -rN -U3 ../murphi-3.1/include/mu_prolog.inc ./include/mu_prolog.inc --- ../murphi-3.1/include/mu_prolog.inc 1999-01-29 16:57:46.000000000 -0500 +++ ./include/mu_prolog.inc 2005-05-16 11:33:26.000000000 -0400 @@ -80,6 +80,15 @@ #define OLD_GPP(arg) #endif +#ifdef TRIPLE_MURPHI +#ifndef HASHC +#error You must use "mu -c " to use 3Murphi. +#endif +#ifdef VER_PSEUDO +#error VER_PSEUDO not supported in 3Murphi. +#endif +#endif // TRIPLE_MURPHI + /**************************************** Default Value or Constant that can be set by user ****************************************/ @@ -93,7 +102,11 @@ // Uli: default number of bits for hash compaction and // suffix of trace info file #ifdef HASHC +#ifdef TRIPLE_MURPHI +#define DEFAULT_BITS 3 +#else // not TRIPLE_MURPHI #define DEFAULT_BITS 40 +#endif //TRIPLE_MURPHI #define TRACE_FILE ".trace" #endif @@ -110,8 +123,14 @@ /**************************************** Release information ****************************************/ +#ifdef TRIPLE_MURPHI +#define INCLUDE_FILE_DATE "May 16 2005" +#define TRIPLE_MURPHI_VERSION "3Murphi version 3.2" +#define TRIPLE_MURPHI_COPYRIGHT "Portions Copyright (c) 2005 by Peter C. Dillinger and the\nGeorgia Tech Research Corporation" +#else // not TRIPLE_MURPHI /* last update */ #define INCLUDE_FILE_DATE "Jan 29 1999" +#endif //TRIPLE_MURPHI /* Murphi Version Number */ #define INCLUDE_FILE_VERSION "Murphi Release 3.1" diff -rN -U3 ../murphi-3.1/include/mu_state.C ./include/mu_state.C --- ../murphi-3.1/include/mu_state.C 1999-01-29 03:28:09.000000000 -0500 +++ ./include/mu_state.C 2005-04-26 16:17:14.000000000 -0400 @@ -146,6 +146,9 @@ #ifdef HASHC if (args->trace_file.value) { unsigned long *key = h3->hash(s, FALSE); +#ifdef TRIPLE_MURPHI + return key[0] == TraceFile->read(lv)->c1; +#else // not TRIPLE_MURPHI unsigned long c1 = key[1] & ((~0UL) << (args->num_bits.value>32 ? 0 : 32-args->num_bits.value)); unsigned long c2 = key[2] & @@ -153,6 +156,7 @@ return ( c1==TraceFile->read(lv)->c1 && c2==TraceFile->read(lv)->c2 ); +#endif //TRIPLE_MURPHI } else #endif @@ -202,12 +206,97 @@ /**************************************** class state_queue for searching the state space. ****************************************/ +#ifdef TRIPLE_MURPHI +state_queue::state_queue() +{ + front = NULL; + rear = &front; + num_elts = 0; +}; + + +state_queue::~state_queue() +{ + // assert front == NULL +} + +void +state_queue::Print( void ) +{ + // TODO? +} + +void +state_queue::enqueue( state* e ) +{ + *rear = new qnode(e); + rear = &((*rear)->next); + num_elts++; +} + +state* +state_queue::dequeue( void ) +{ + static state s; + if (front == NULL) { + cerr << "Queue should contain " << num_elts << " states...\n"; + Error.Notrace( "Internal: Attempt to dequeue() empty queue.", "", "" ); + } + s = front->data; + qnode * tmp = front; + front = front->next; + delete tmp; + if (front == NULL) rear = &front; + num_elts--; + return &s; +} + +state* +state_queue::top( void ) +{ + if ( num_elts>0 ) + { + return &(front->data); + } + else + { + cerr << "Queue should contain " << num_elts << " states...\n"; + Error.Notrace( "Internal: Attempt to top() empty state queue.", "", "" ); + return NULL; + } +} + +void +state_stack::enqueue( state* e ) +{ + front = new snode(e,front); + num_elts++; +} + +unsigned state_stack::NextRuleToTry() { + return ((snode *)front)->rulenum; +} + +void state_stack::NextRuleToTry(unsigned r) { + ((snode *)front)->rulenum = r; +} + +#else // not TRIPLE_MURPHI + state_queue::state_queue( unsigned long mas ) +#ifdef ORIGINAL :max_active_states(mas), num_elts(0), front(0), rear(0) +#else // fixes a warning: +:max_active_states(mas), front(0), rear(0), num_elts(0) +#endif //ORIGINAL { stateArray = new state*[ max_active_states ]; +#ifdef ORIGINAL for ( long i = 0; i < max_active_states; i++) // Uli: avoid bzero +#else // fixes a warning: + for ( unsigned long i = 0; i < max_active_states; i++) // Uli: avoid bzero +#endif //ORIGINAL stateArray[i] = NULL; }; @@ -265,12 +354,20 @@ retval = stateArray[ front ]; front = (front + 1) % max_active_states; num_elts--; +#ifndef ORIGINAL + return retval; +#endif //ORIGINAL } else { Error.Notrace( "Internal: Attempt to dequeue from empty state queue.", "", "" ); +#ifndef ORIGINAL + return NULL; /* dead code */ +#endif //ORIGINAL } +#ifdef ORIGINAL return retval; +#endif //ORIGINAL } state* @@ -302,6 +399,7 @@ Error.Notrace( "Internal: Too many active states." ); } } +#endif //TRIPLE_MURPHI /**************************************** // changes by Uli The Stateset implementation for recording all the states found. @@ -324,21 +422,62 @@ #else assert (sizeof(Unsigned32)==4); // the implementation is pretty depen- // dent on the 32 bits +#ifdef TRIPLE_MURPHI + double bps; + if (args->use_hashc.value) { + bps = (double)(args->num_bits.value); + } else { + bps = (2.0 + args->num_bits.value) / 2.0; + } + unsigned long size = + (unsigned long)((double)table_size * bps / 32.0) + 3; +#else // not TRIPLE_MURPHI unsigned long size = (unsigned long)((double)table_size*args->num_bits.value/32) + 3; +#endif //TRIPLE_MURPHI // higher precision necessary to avoid overflow // two extra elements needed in table table = new Unsigned32 [size]; for (unsigned long i=0; inum_bits.value; + if (args->use_hashc.value) { + bstore = &state_set::bstore_hc; + if (num_bits == 64) { + k1mask = k2mask = 0xffffffffU; + } else if (num_bits > 32) { + k2mask = 0xffffffffU; + k1mask = (1U << (num_bits - 32)) - 1U; + } else if (num_bits == 32) { + k2mask = 0xffffffffU; + k1mask = 0; + } else { + k2mask = (1U << num_bits) - 1U; + k1mask = 0; + } + hcslots = table_size; + bmask = 1; + while ((bmask << 1) + 1 < table_size) bmask = (bmask << 1) + 1; + // bmask allows us to avoid mod operations in computing successive indices. + } else { + bstore = &state_set::bstore_bf; + bmask = 1; + while ((bmask << 1) + 1 < table_words) bmask = (bmask << 1) + 1; + } +#else // not TRIPLE_MURPHI Full = new dynBitVec ( table_size ); +#endif //TRIPLE_MURPHI } state_set::~state_set() { delete[] table; // only works for newer g++ versions +#ifndef TRIPLE_MURPHI delete Full; +#endif //TRIPLE_MURPHI } // Uli: the two following routines were deleted because they were not called @@ -346,6 +485,113 @@ //void state_set::clear_state_set() //void copy_state_set( state_set * set1, state_set * set2) +#ifdef TRIPLE_MURPHI + +bool state_set::bstore_hc(unsigned long *key){ + unsigned long a,b,c=0; long t; + bool pres = TRUE; + unsigned long K1, K2, K3; + K1 = key[2]; + K2 = key[1]; + K3 = key[0]; + if (hcslots == 0) { + cerr << "The compacted hash table has filled up.\n"; + cerr << "We recommend trying again with a Bloom filter (no -c) storing no more than\n"; + cerr << num_bits/2 << " bits per state."; + Error.Notrace("Aborting...\n"); + } + a = K3 % table_size; + K2 &= k2mask; + b = K2 & bmask; + if (b == 0) { + K2 = (K3 + K1 + (key[1] >> 16)) & k2mask; + b = K2 & bmask; + if (b == 0) { + b = K2 = 1; + } + } + K1 &= k1mask; + for(;;) { + unsigned long *vect; unsigned long v1, v2; + unsigned long start, idx, invstart; + idx = num_bits * (a & 31); + start = idx & 31; + idx = (idx >> 5) + num_bits * (a >> 5); + invstart = 31 - start; + vect = table + idx; + v1 = ((vect[0] << start) | ((vect[1] >> invstart) >> 1)) & k1mask; + v2 = ((vect[1] << start) | ((vect[2] >> invstart) >> 1)) & k2mask; + if (v1 == 0 && v2 == 0) { + vect[0] |= K1 >> start; + vect[1] |= ((K1 << invstart) << 1) | (K2 >> start); + vect[2] |= (K2 << invstart) << 1; + hcslots--; + num_collisions += c; + return FALSE; + } + if (v1 == K1 && v2 == K2) { + return pres; + } + /* if we reach here, we know we're continuing... */ + c += pres ? 1 : 0; + if (K1 < v1 || (K1 == v1 && K2 < v2)) { + vect[0] ^= (K1^v1) >> start; + vect[1] ^= (((K1^v1) << invstart) << 1) | + ((K2^v2) >> start); + vect[2] ^= ((K2^v2) << invstart) << 1; + K1 = v1; K2 = v2; + b = K2 & bmask; + pres = FALSE; + } + t = a - b; a = t + ((t >> 31) & table_size); + } +} + +bool state_set::bstore_bf(unsigned long *key) { + unsigned long i, ay, ai, by, bi; + int t; + ay = key[0] % table_words; + ai = key[2] & 31; bi = ((key[2] >> 5) & 15) + 1; + by = key[1] & bmask; + + for (i = 1; ; i++) { + if (!(table[ay]&(1 << ai))) break; + if (i == num_bits) return TRUE; // search successful + t = ay - by; ay = t + ((t >> 31) & table_words); + // fast version of ay = (ay - by) % table_words + by = (by + i) & bmask; + ai = (ai + bi) & 31; + } + for (;; i++) { + table[ay] |= 1 << ai; + if (i == num_bits) break; + t = ay - by; ay = t + ((t >> 31) & table_words); + by = (by + i) & bmask; + ai = (ai + bi) & 31; + } + return FALSE; +} + +bool +state_set::simple_was_present( state *& in, bool valid, bool permanent ) +{ + unsigned long *key = h3->hash(in, valid); + + if ((this->*bstore)(key)) return TRUE; + + if (args->trace_file.value) + TraceFile->write(key[0], key[0], in->previous.lVal()); + + // Lifted out + //copy_state(in); + + num_elts++; + if (permanent) + num_elts_reduced++; + return FALSE; +}; + +#else // not TRIPLE_MURPHI bool state_set::simple_was_present( state *& in, bool valid, bool permanent ) /* changes in to point to the first state found with that pattern. */ @@ -373,7 +619,11 @@ register unsigned long addr, offset; register unsigned long c1 = key[1]&mask1; register unsigned long c2 = key[2]&mask2; +#ifdef ORIGINAL register unsigned long t1, t2; +#else // fixes a warning: (never actually used uninitialized, though) + unsigned long t1=0, t2=0; +#endif //ORIGINAL #endif #ifdef VER_PSEUDO @@ -502,6 +752,7 @@ #endif }; +#endif //TRIPLE_MURPHI bool state_set::was_present( state *& in, bool valid, bool permanent ) @@ -517,6 +768,38 @@ void state_set::print_capacity( void ) { +#ifdef TRIPLE_MURPHI + double states = table_words * 4.0; + double million = 1000000.0; + double mega = 1048576.0; + + if (args->use_hashc.value) { + cout << "\t* Memory allocated to compacted hash table:\n"; + cout << "\t " << states/mega << " MB" + << " (" << states/million << " million bytes)\n"; + cout << "\t* With states hash-compressed to " + << args->num_bits.value << " bits, the maximum size of\n" + << "\t the state space is about " + << table_size << " states.\n"; + } else { + cout << "\t* Memory allocated to Bloom filter:\n"; + cout << "\t " << states/mega << " MB" + << " (" << states/million << " million bytes)\n"; + if (args->num_bits.value < 3) { + cout << "\t* With the current Bloom filter setting (" + << args->num_bits.value << " bits), " + << "we could visit\n\tmore than " + << (table_words / (num_bits + 2)) * 64 << " states.\n"; + } else { + cout << "\t* The current Bloom filter setting (" + << args->num_bits.value << " bits) is the best for around\n" + << "\t " << (unsigned long)((table_words * 32.0) / (num_bits/.7 + 1.0/num_bits - 1.6)) + << " states, but could visit more than " + << (table_words / (num_bits + 2)) * 64 << " states.\n"; + } + } + +#else // not TRIPLE_MURPHI cout << "\t* The memory allocated for the hash table and state queue is\n\t "; if (args->mem.value > 1000000) cout << (args->mem.value/1000000) << " Mbytes.\n"; @@ -535,6 +818,7 @@ << table_size << " states.\n" << "\t * Use option \"-k\" or \"-m\" to increase this, if necessary.\n"; #endif +#endif //TRIPLE_MURPHI } /**************************************** diff -rN -U3 ../murphi-3.1/include/mu_statecl.h ./include/mu_statecl.h --- ../murphi-3.1/include/mu_statecl.h 1999-11-03 16:50:10.000000000 -0500 +++ ./include/mu_statecl.h 2005-04-21 18:21:50.000000000 -0400 @@ -136,7 +136,11 @@ friend int StateCmp(state * l, state * r); friend void copy_state(state *& s); #ifdef HASHC +#ifdef ORIGINAL friend hash_function; +#else // fixed version: +friend class hash_function; +#endif // ORIGINAL #endif //friend unsigned long* hash_function::hash(state*, bool); // friend bool StateEquivalent(state * l, state * r); // Uli: not necessary diff -rN -U3 ../murphi-3.1/include/mu_state.h ./include/mu_state.h --- ../murphi-3.1/include/mu_state.h 1999-01-29 03:28:09.000000000 -0500 +++ ./include/mu_state.h 2005-05-16 11:24:30.000000000 -0400 @@ -110,29 +110,72 @@ : s(s), next(next) {}; }; +#ifdef TRIPLE_MURPHI +struct qnode { + state data; + qnode * next; + + qnode(state *s) { + data = *s; + next = NULL; + } + + qnode(state *s, qnode *n) { + data = *s; + next = n; + } +}; + +struct snode: public qnode { + unsigned rulenum; + + snode(state *s) : qnode(s) { + rulenum = 0; + } + + snode(state *s, qnode *n) : qnode(s,n) { + rulenum = 0; + } +}; +#endif //TRIPLE_MURPHI + /**************************************** The state queue. ****************************************/ class state_queue { protected: +#ifdef TRIPLE_MURPHI + qnode * front; + qnode ** rear; +#else // not TRIPLE_MURPHI state** stateArray; /* The actual array. */ const unsigned long max_active_states; /* max size of queue */ unsigned long front; /* index of first active state. */ unsigned long rear; /* index of next free slot. */ +#endif //TRIPLE_MURPHI unsigned long num_elts; /* number of elements. */ public: // initializers +#ifdef TRIPLE_MURPHI + state_queue(); + virtual unsigned long bytesUsed() { return num_elts * sizeof(qnode); } +#else // not TRIPLE_MURPHI state_queue( unsigned long mas ); +#endif //TRIPLE_MURPHI // destructor virtual ~state_queue(); // information interface +#ifndef TRIPLE_MURPHI inline unsigned long MaxElts( void ) { return max_active_states; } +#endif //TRIPLE_MURPHI unsigned long NumElts( void ) { return num_elts; } +#ifndef TRIPLE_MURPHI inline static int BytesForOneState( void ); +#endif //TRIPLE_MURPHI inline bool isempty( void ) { return num_elts == 0; } // storing and removing elements @@ -154,19 +197,36 @@ void Print( void ); virtual void print_capacity( void ) { +#ifdef TRIPLE_MURPHI + cout << "\t* Using 3Murphi's breadth-first queue (limited only by v.m. size).\n"; +#else // not TRIPLE_MURPHI cout << "\t* Capacity in queue for breadth-first search: " << max_active_states << " states.\n" << "\t * Change the constant gPercentActiveStates in mu_prolog.inc\n" << "\t to increase this, if necessary.\n"; +#endif //TRIPLE_MURPHI } }; class state_stack: public state_queue { +#ifndef TRIPLE_MURPHI unsigned * nextrule_to_try; +#endif //TRIPLE_MURPHI public: // initializers +#ifdef TRIPLE_MURPHI + state_stack() + : state_queue() + { + } + + virtual ~state_stack() { + // assert front == NULL + } + virtual unsigned long bytesUsed() { return num_elts * sizeof(snode); } +#else // not TRIPLE_MURPHI state_stack( unsigned long mas ) : state_queue(mas) { @@ -181,24 +241,37 @@ { delete[ OLD_GPP(max_active_states) ] nextrule_to_try; // Should be delete[]. }; +#endif //TRIPLE_MURPHI virtual void print_capacity( void ) { +#ifdef TRIPLE_MURPHI + cout << "\t* Using 3Murphi's depth-first stack (limited only by v.m. size).\n"; +#else // not TRIPLE_MURPHI cout << "\t* Capacity in queue for depth-first search: " << max_active_states << " states.\n" << "\t * Change the constant gPercentActiveStates in mu_prolog.inc\n" << "\t to increase this, if necessary.\n"; +#endif //TRIPLE_MURPHI } virtual void enqueue( state* e ); virtual unsigned NextRuleToTry() +#ifdef TRIPLE_MURPHI + ; +#else // not TRIPLE_MURPHI { return nextrule_to_try[ front ]; } +#endif //TRIPLE_MURPHI virtual void NextRuleToTry(unsigned r) +#ifdef TRIPLE_MURPHI + ; +#else // not TRIPLE_MURPHI { nextrule_to_try[ front ] = r; } +#endif //TRIPLE_MURPHI #ifdef partial_order_opt // special interface with sleepset @@ -225,14 +298,30 @@ #else Unsigned32 *table; #endif +#ifdef TRIPLE_MURPHI + unsigned long table_words; + unsigned long num_bits; + unsigned long k1mask; + unsigned long k2mask; + unsigned long bmask; + unsigned long hcslots; + + bool (state_set::*bstore)(unsigned long *); + bool bstore_bf(unsigned long *); + bool bstore_hc(unsigned long *); + +#else // not TRIPLE_MURPHI dynBitVec *Full; /* whether element table[i] is used. */ +#endif //TRIPLE_MURPHI unsigned long num_elts; /* number of elements in table */ unsigned long num_elts_reduced; // Uli unsigned long num_collisions; /* number of collisions in hashing */ +#ifndef TRIPLE_MURPHI // internal routines bool is_empty( unsigned long i ) /* check if element table[i] is empty */ { return Full->get(i) == 0; }; +#endif //TRIPLE_MURPHI public: // constructors @@ -257,6 +346,11 @@ static int bits_per_state(void); #endif +#ifdef TRIPLE_MURPHI + inline unsigned long words_in_table() { return table_words; }; + inline unsigned long slots_left_in_table() { return hcslots; }; + inline unsigned long collisions_so_far() { return num_collisions; }; +#endif //TRIPLE_MURPHI // get the number of elts in the state set inline unsigned long NumElts() { return num_elts; }; @@ -268,6 +362,9 @@ // print hashtable void print() { +#ifdef TRIPLE_MURPHI + cout << "Entire table is compressed. Sorry.\n"; +#else // not TRIPLE_MURPHI for (unsigned long i=0; iCheckInvariants()) { +#ifdef TRIPLE_MURPHI + copy_state(s); +#endif //TRIPLE_MURPHI curstate = s; #ifdef HASHC if (args->trace_file.value) @@ -134,6 +145,13 @@ #ifdef HASHC #include +#ifdef TRIPLE_MURPHI +typedef long double calc_t; +#define powc powl +//calc_t powl(calc_t, calc_t); +#define logc logl +//calc_t logl(calc_t); +#endif //TRIPLE_MURPHI double StateManager::harmonic(double n) // return harmonic number H_n @@ -145,7 +163,10 @@ void StateManager::CheckLevel() // check if we are done with the level currently expanded { +#ifdef ORIGINAL // unused var: static double p = 1.0; // current bound on state omission probability +#endif //ORIGINAL +#ifndef TRIPLE_MURPHI static double l = pow(2, double(args->num_bits.value)); // l=2^b static double k = -1; // sum of the number of states - 1 static double m = NumStates; // size of the state table @@ -170,16 +191,256 @@ pno *= pk; } } +#endif //TRIPLE_MURPHI } void StateManager::PrintProb() { +#ifdef TRIPLE_MURPHI + cout << "3Murphi Omission Analysis (for b=" << args->num_bits.value + << ((args->use_hashc.value) ? " Hash Compaction" : " Bloom filter") + << "):\n\n"; + cout.flush(); + unsigned long nstates = the_states->NumElts(); + unsigned long words = the_states->words_in_table(); + unsigned long truncs = Rules->NumRulesFired() - nstates; + double hfv = (double) words * 32.0 / (double) nstates; + unsigned long nseen; + unsigned long ntot; + calc_t cov, f; + + if (args->use_hashc.value) { + unsigned long hcbits = args->num_bits.value; + unsigned long hcslots = the_states->slots_left_in_table(); + unsigned long hccolls = the_states->collisions_so_far(); + unsigned long hcmax = NumStates; + + /*================= taken almost straight from 3spin 3.0 ==============*/ + printf("\tslots remaining in table: %lu (%.4g%%)\n", + hcslots, 100.0 * (double) hcslots / (double) hcmax); + if (args->advanced.value) { + printf("\tinnocuous omissions: %lu\n", + (unsigned) nstates + hcslots - hcmax); + printf("\thash factor (visited): %.6g\n", hfv); + } + unsigned k; + f = (calc_t) words * 32.0L / (calc_t) nstates; + k = (unsigned) (powc(3.8L,1.0L/(f+4.2L))*f*.69315L + 0.99999999L); + printf("\n"); + calc_t m, n, ac, tc, l; + double hft = hfv; + if (args->advanced.value) printf("\tcollisions w/true omission potential: %lu\n", hccolls); + n = (calc_t) nstates; + m = (calc_t) hcmax; + l = powc(2.0L, (calc_t)hcbits) - 1.0L; + tc = (m + 1.5L - n) * logc((m + 1.5L - n)/m) + n; + ac = (calc_t) hccolls; + if (ac > 2*l) { + calc_t xr, mr, tf, te, tot; + while (n - ac/l < (calc_t)nstates) { + calc_t nc; + n += (calc_t)((unsigned)(ac/l)+1U); + nc = (m + 1.5L - n) * logc((m + 1.5L - n)/m) + n; + ac += nc - tc; tc = nc; + } + /* coverage heuristics */ + xr = (tc/l)/n; + mr = ((calc_t)nstates + (calc_t)truncs)/(calc_t)truncs; + tf = powl(mr, 3.0 + 10.0 * xr); + te = (tc/l) * tf; + tot = n + te; + cov = (n - (tc/l)) / tot; + /* end coverage heuristics */ + hft = (double) words * 32.0 / tot; + printf("\test. hash omissions: %6g\n", + (double)(tc/l)); + if (truncs > nstates) { + printf("\t(total omissions could be many times larger)\n"); + if (cov > 0.95L && !args->advanced.value) { + printf("\t*rough* coverage estimate: %6g%%\n", + 100.0* (double) cov); + } + } else { + printf("\t(total omissions could be orders of magnitude larger)\n"); + } + if (args->advanced.value) { + printf("\test. hash factor (seen): %6g\n", hft); + printf("\test. states seen: %u\n", + (unsigned) n); + printf("\t*rough* coverage estimate: %6g%%\n", + 100.0* (double) cov); + } + nseen = (unsigned long) (n + 0.99L); + ntot = (unsigned long) (tot + 0.99L); + } else if (ac < 0.01L * l) { + printf("\test. prob. of any omissions: 1 in %.7g\n", + (double)(l/ac)); + nseen = ntot = nstates; + cov = 1.0L; + } else { + printf("\test. prob. of any omissions: %.6g\n", + (double)(1.0L - powc(1.0L - 1.0L/l, ac))); + nseen = ntot = nstates; + cov = 1.0L; + } + +/* if (args->advanced.value) { + unsigned uhfv, uhft; + uhfv = (unsigned) (hfv * 0.998); + uhft = (unsigned) (hft * 0.998); + if (uhfv == hcbits) { + printf("\tYou used the max bits per compacted state (-b%lu) for allocated memory.\n", hcbits); + } else if (uhft < uhfv) { + printf("\tFor this model, -b%u is almost certainly a safe choice,\n", uhft); + printf("\tthough the table might not overflow with as much as -b%u\n", uhfv); + } else { + printf("\tThe max bits per compacted state for allocated memory is -b%u\n", uhfv); + } + if (uhfv > 64) { + printf("\t(Note that 3Murphi only supports up to -b64 (with -c), because\n\thigher values don't offer any tangible accuracy benefits.)\n"); + } + }*/ + } else { + unsigned long hfns = args->num_bits.value; + + /*================= taken almost straight from 3spin 3.0 ==============*/ + if (args->advanced.value) printf("\thash factor (visited): %.6g\n", hfv); + calc_t xr, mr, tf, te, tot; + calc_t i, n = 30000.0L; + calc_t p, q, m, c, est = 0.0L, k = (calc_t)hfns; + c = (calc_t) nstates / n; + m = (calc_t) words * 32.0L / c; + p = 1.0L - (k / m); q = 1.0L; + for (i = 0.0L; i - est < n && i < 300000.0L; i += 1.0L) { + q *= p; + est += powc(1.0L - q, k); + } + f = m/i; + est *= c; + i *= c; + m *= c; + est += i / m * (i - 1.0L) / 2.0L / m ; // for enh. double hashing + /* coverage heuristics */ + xr = est/i; + mr = ((calc_t)nstates + (calc_t)truncs)/(calc_t)truncs; + tf = powl(mr, 3.0 + 10.0 * xr); + te = est * tf; + tot = i + te; + cov = (i - est) / tot; + /* end coverage heuristics */ + if (est == 0.0L) { + printf("\test. prob. of any omissions: too small to measure\n"); + nseen = ntot = nstates; + } else if (est < 0.01L) { + printf("\test. prob. of any omissions: 1 in %.7g\n", + (double)(1.0L / est)); + nseen = ntot = nstates; + } else if (est > 1.5L) { + printf("\test. states seen: %u\n", + (unsigned) i); + printf("\test. hash omissions: %.6g\n", + (double) est); + if (truncs > nstates) { + printf("\t(total omissions could be many times larger)\n"); + if (cov > 0.9L && !args->advanced.value) { + printf("\t*rough* coverage estimate: %6g%%\n", + 100.0* (double) cov); + } + } else { + printf("\t(total omissions could be orders of magnitude larger)\n"); + } + nseen = (unsigned long) (i + 0.99L); + ntot = (unsigned long) (tot + 0.99L); + } else { + printf("\test. prob. of any omissions: %.6g\n", + (double)(1.0L - powc(2.718281828L, -est))); + nseen = ntot = nstates; + } + if (args->advanced.value) { + printf("\test. hash factor (seen): %.8g\n", (double)f); + printf("\t*rough* state space size estimate %.12g\n", (double) tot); + printf("\t*rough* coverage estimate: %.8g%%\n", 100.0 * (double) cov); + } +/* if (args->advanced.value) { + unsigned better_k; + if (f < 1.13459) better_k = 1; + else if (f < 2.34809) better_k = 2; + else if (f < 3.64409) better_k = 3; + else better_k = (unsigned) (powc(3.8L,1.0L/(f+4.2L))*f*.69315L + 0.99999999L); + if (better_k == hfns) { + printf("\tWithout -c, the -b value you chose (%lu) is likely the best.\n", hfns); + } else if (cov < 0.90L && ((int)better_k - (int)hfns) > 2) { + printf("\tWithout -c, -b%lu would probably be more accurate, but\n", (better_k + hfns) / 2); + printf("\tthe best choice might be as high as -b%u\n", better_k); + } else if (cov < 0.90L && ((int)better_k - (int)hfns) < -2) { + printf("\tWithout -c, -b%u would probably be more accurate.\n", better_k); + } else { + printf("\tWithout -c, -b%u is probably the most accurate choice.\n", better_k); + } + if (better_k > 40) { + printf("\t(Note that 3Murphi limits you to -b%u (without -c), because higher\n\tvalues don't offer any tangible accuracy benefits.)\n", 40); + } + printf("\n"); + if (cov < 0.9) { + printf("\tSwitching to hash compaction (-c) is not recommended given\n\tthe accuracy of this search.\n"); + } else if (f < 10.0) { + printf("\tYou have so little memory per state, hash compaction is\n\tunlikely to be better. You should continue without -c.\n"); + } else { + if (cov > 0.99) { + unsigned h = (unsigned)(f * (cov - 0.01L)); + printf("\tYou should use hash compaction for reverifying this model.\n"); + printf("\tEstimated best setting: -c -b%u\n", h); + if (h > 64) { + printf("\t(Note that 3Murphi only supports up to -b64 (with -c), because\n\thigher values don't offer any tangible accuracy benefits.)\n"); + } + } else { + unsigned h = (unsigned)(f * (cov - 0.05L)); + printf("\tHash compaction *might* yield more coverage on this model.\n"); + printf("\tEstimated safe h.c. setting: -c -b%u\n", h); + if (h > 64) { + printf("\t(Note that 3Murphi only supports up to -b64 (with -c), because\n\thigher values don't offer any tangible accuracy benefits.)\n"); + } + } + } + }*/ + } + + + /* recommendations */ + printf("\nRecommendations for follow-up verification of the SAME model:\n\n"); + + if (cov < 0.9L) { + printf("\tUsing hash compaction (-c) is NOT recommended given the accuracy\n\tof this search.\n"); + printf("\tUse a Bloom filter (no -c) with -e%lu\n", nseen); + } else if (f < 10.0) { + printf("\tYou have so little memory per state, a Bloom filter is likely to be\n\tbetter than hash compaction.\n"); + printf("\tUse a Bloom filter (no -c) with -e%lu\n", nseen); + } else { + if (cov > 0.99L) { + printf("\tYou should use hash compaction for reverifying this model.\n"); + printf("\tEstimated best setting: -c -e%lu\n", ntot); + } else { + printf("\tHash compaction *might* yield more coverage on this model.\n"); + printf("\tProbably safe, probably more accuracte: -c -e%lu\n", ntot); + printf("\tAlways safe, probably less accuracte: -e%lu (no -c)\n", nseen); + } + } + + printf("\nRecommendations for verification of a SIMILAR model:\n\n"); + printf("\tUse a Bloom filter (no -c) with -e%lu, though you can\n", nseen); + printf("\ttweak that estimate if you have some idea of what might happen\n\tto the state space size.\n"); + + printf("\n"); + fflush(stdout); +#else // not TRIPLE_MURPHI // calculate Pr(not even one omission) with equation (12) from CHARME // paper double l = pow(2,double(args->num_bits.value)); double m = NumStates; double n = the_states->NumElts(); +#ifdef ORIGINAL // unused var: double exp = (m+1) * (harmonic(m+1) - harmonic(m-n+1)) - n; +#endif //ORIGINAL double pNO = pow(1-1/l, (m+1) * (harmonic(m+1) - harmonic(m-n+1)) - n); // print omission probabilities @@ -193,6 +454,7 @@ // remark: startstates had incremented the currentLevel counter else cout << "\n"; +#endif //TRIPLE_MURPHI } #endif @@ -234,7 +496,9 @@ void StateManager::print_trace_aux(StatePtr p) // changes by Uli { +#ifdef ORIGINAL // unused var: state original; +#endif //ORIGINAL char *s; if (p.isStart()) @@ -322,7 +586,9 @@ state * StartStateManager::StartState() { +#ifdef ORIGINAL // unused var: state *next_state = NULL; +#endif //ORIGINAL category = STARTSTATE; @@ -690,7 +956,11 @@ void RuleManager::print_rules_information() { +#ifdef ORIGINAL // potentially used uninitialized: bool exist; +#else // fixed: + bool exist = FALSE; +#endif //ORIGINAL if (args->print_rule.value) { @@ -800,7 +1070,11 @@ Reporter->print_warning(); +#ifdef ORIGINAL signal(SIGFPE, &catch_div_by_zero); +#else // fixed version: + signal(SIGFPE, (void (*)(int))&catch_div_by_zero); +#endif //ORIGINAL }; @@ -858,8 +1132,10 @@ // omission probability calculation StateSet->CheckLevel(); +#ifndef TRIPLE_MURPHI delete curstate; #endif +#endif } // while Reporter->print_final_report(); } @@ -950,9 +1226,11 @@ // previous state does not deadlock, as it gives the state just removed deadlocked_so_far = FALSE; +#ifndef TRIPLE_MURPHI #ifdef HASHC delete curstate; #endif +#endif //TRIPLE_MURPHI } // if } // while diff -rN -U3 ../murphi-3.1/include/mu_system.h ./include/mu_system.h --- ../murphi-3.1/include/mu_system.h 1999-11-03 16:50:36.000000000 -0500 +++ ./include/mu_system.h 2005-05-16 11:25:03.000000000 -0400 @@ -95,7 +95,10 @@ unsigned long NumElts(); unsigned long NumEltsReduced(); // Uli unsigned long QueueNumElts(); - +#ifdef TRIPLE_MURPHI + unsigned long BytesInQueue() { return queue->bytesUsed(); } + unsigned long BytesInSet() { return the_states->words_in_table() * 4; } +#endif //TRIPLE_MURPHI }; // extern class StartStateGenerator; diff -rN -U3 ../murphi-3.1/include/mu_util.C ./include/mu_util.C --- ../murphi-3.1/include/mu_util.C 1999-01-29 02:49:11.000000000 -0500 +++ ./include/mu_util.C 2005-04-21 18:31:14.000000000 -0400 @@ -80,7 +80,11 @@ { if ( super[i+j] != sub[j] ) break; } +#ifdef ORIGINAL if ( j == strlen(sub) ) +#else // gets rid of a warning: + if ( (unsigned)j == strlen(sub) ) +#endif // ORIGINAL return &(super[i]); /* Match. */ } return NULL; /* No match. */ @@ -145,11 +149,22 @@ NumStatesGivenBytes( unsigned long bytes ) /* From Andreas\' code.*/ { +#ifdef TRIPLE_MURPHI + if (args->use_hashc.value) { // hash compaction + unsigned long n = (bytes / state_set::bits_per_state() + 1) * 8; + return NextPrime( n ); + } else { // Bloom filter: use a realistic maximum + return (unsigned long) + ( (double) bytes * 8.0 / + ( (state_set::bits_per_state() + 2.0) / 2.0)); + } +#else // not TRIPLE_MURPHI unsigned long exactNumStates = (unsigned long) ( (double) bytes * 8 / ( state_set::bits_per_state() + gPercentActiveStates * 8 * state_queue::BytesForOneState())); return NextPrime( exactNumStates ); +#endif //TRIPLE_MURPHI } char * diff -rN -U3 ../murphi-3.1/include/mu_util.h ./include/mu_util.h --- ../murphi-3.1/include/mu_util.h 1999-01-29 02:49:11.000000000 -0500 +++ ./include/mu_util.h 2005-04-20 13:51:46.000000000 -0400 @@ -164,7 +164,11 @@ // Uli: this constructor is called implicitly for function results // by the code generated by the Murphi compiler mu__int(const mu__int &src) +#ifdef ORIGINAL :lb(src.lb), ub(src.ub), size(src.size), in_world(FALSE) +#else // fixes a warning: + :in_world(FALSE), lb(src.lb), ub(src.ub), size(src.size) +#endif //ORIGINAL { set_self("Function result", 0); value(src.value()); // value() allows returning undefined values @@ -694,7 +698,7 @@ state *getstate(); /* return a state encoding the values of all variables. */ state_L *getstate_L(); /* return a state_L */ void setstate( state *thestate ); /*set the state of the world to - /*thestate.*/ + THESTATE.*/ }; /*************************** diff -rN -U3 ../murphi-3.1/README-3Murphi.html ./README-3Murphi.html --- ../murphi-3.1/README-3Murphi.html 1969-12-31 19:00:00.000000000 -0500 +++ ./README-3Murphi.html 2005-05-16 18:30:38.000000000 -0400 @@ -0,0 +1,182 @@ + + + +Home of 3Murphi by Peter C. Dillinger, Georgia Tech College of Computing + + +
+

3Murphi Home/Documentation

+
+

Intro

+3Murphi (pronounced "Triple Murphy") is a modified version of the +Murphi verifier +with advances in the efficiency, configurability, and usability of +probabilistic explicit-state verification. I will try to match up +releases of 3Murphi with versions of its cousin, +3SPIN, with which it +shares much code and many features. The most notable features 3Murphi offers +to users of Murphi are Bloom filters, an improved hash compaction +implementation, and more useful feedback from verification runs. +

+
+ +

The Papers

+

+Although these papers use Spin for experimental validation, the ideas are +relevant to the design and use of 3Murphi, which incorporates virutally all +of the techniques discussed therein: +

+Fast and Accurate Bitstate Verification for SPIN,
+by Peter C. Dillinger and Panagiotis Manolios,
+In Proc. of 11th Int'l SPIN Workshop,
+Volume 2989 of Springer LNCS +

+Bloom Filters in Probabilistic Verification,
+by Peter C. Dillinger and Panagiotis Manolios,
+In Proc. of FMCAD 2004, Formal Methods in Computer-Aided Design, 2004,
+Volume 3312 of Springer LNCS +

+
+

Using 3Murphi v3.2

+

+The process of generating a C++ verifier with 3Murphi is exactly as +with generating a hash compaction based verifier with Murphi, +mu -c mymodel.m. Using -b with 3Murphi presents a similar +trade-off as it does with a hash compaction based Murphi verifier. +

+Users should refer to Murphi documentation for details on the process of +building a model and generating a verifier. +

+

+

Compile time

+After adding 3Murphi capabilities to a Murphi 3.2 installation, the user +won't notice any difference (aside from some bug fixes and compiler warning +fixes) unless the C++ verifier (mymodel.C) is compiled with +-DTRIPLE_MURPHI. Specifying -DTRIPLE_MURPHI means the +compiled verifier includes 3Murphi's implementations of both bitstate hashing +(Bloom filter) and hash compaction. Total (non-probabilistic) verification +is only available as usual, without -DTRIPLE_MURPHI, but when given +the amount of memory required for total verification, probabilistic approaches +will typically be a less likely source of error than the verification software +or hardware itself. +

+-DTRIPLE_MURPHI may or may not be compatible with other various +preprocessing flags used in compiling the verifier, but none should be +required. However, we recommend compiling with optimizations +(e.g. -O3) because we have seen greater than two-fold speed-ups +from enabling optimization in Murphi and 3Murphi. +

+

Run time

+3Murphi is highly-configurable from the verifier command line. +These options are either exclusive to 3Murphi or behave differently in 3Murphi: +

+

+ + + + + + + + + + + + + + +
-cUse hash compaction instead of the default of using a Bloom filter. +Note that this is a change of default behavior from regular Murphi, +but it works well with the probabilistic verification methodology described +in our research papers.
-bxx +In Bloom filter mode (no -c): Set xx bits +per state instead of the default of 3 (inherited from Spin and "supertrace"). +Must be at least 1 and values larger than 40 will be truncated to 40. +

+In Hash Compaction mode (with -c): Store xx bits +per state instead of the 3Murphi default of 32. Values outside the valid +range of 4 to 64 will be truncated to the nearest valid value. +

-jUse the Jenkins LOOKUP2 hash function instead of Murphi's default. +This hash function can be faster but might not be quite as accurate. +
-mxxxUse xxx megabytes for the Bloom filter or compacted hash table. +No subtractions are made for stack/queue space. (see below) +
-kxxxUse xxx kilobytes for the Bloom filter or compacted hash table. +No subtractions are made for stack/queue space. (see below) +
+

+

Memory usage

+Regardless of the verification mode and regardless of what the output seems +to indicate, Murphi stores states on the "todo" list (stack for DFS or +queue for BFS) explicitly, and only a small portion of this space is +included in the memory amount specified with -m or -k. +3Murphi also stores todo states explicitly, but does not take any of this +space from that specified by -m or -k. This is related to +another feature of 3Murphi: the number of states in the todo list is only +limited by the vitrtual memory of the machine. +

+The storage of todo states presents some +interesting trade-offs. Using bit-compaction (-b to mu) +means these states will be much smaller, but Murphi is much slower at +processing bit-compacted states. This is the first trade-off. +

+The second trade-off deals with how much memory to dedicate to the visited +list. Dedicating nearly all of main memory to the visited list (e.g. +-m480 on a 512MB machine) maximizes accuracy without killing the +execution time by having the visited list spill into swap space. However, +in our experience, the todo list gets much bigger than an +appropriately-sized visited list, meaning the bulk of the todo list will +be swapped out if the visited list is taking up 90+% of main memory. This +will slow down the verification process, but not intractably. The todo list +is accessed linearly, whereas the visited list is accessed randomly. But +the entire process is fastest if both lists fit in main memory. +

+A good strategy would be to dedicate about 20% of main memory to the visited +list when first verifying a model. Using the default setting of a 3-bit +Bloom filter will almost certainly find errors if there are any, and the +todo list is likely to fit in the rest of main memory. In following +up to double-check error-freedom, one could dedicate more memory to the +visited list, enabling more accuracy at a possible speed cost. Notice that +the recommendations output by 3Murphi are based on -e, which does +not need to change if you increase the memory dedicated to the visited list. +Drastically reducing the visited list memory could, however, hurt coverage +enough to make the visitable size estimate too large. +

+

Supported platforms

+3Murphi is optimized for 32-bit machines and may or may not work on machines +with different word sizes. 3Murphi is also optimized for Intel x86 +architectures such as the Pentium 4. We developed 3SPIN +with various versions of GNU/Linux, but should work for other 32-bit +platforms supported by Murphi. +

+Taking advantage of 64-bit architectures would require significant +changes/updates to 3Murphi and might happen in the future. +

+
+

+

Getting 3Murphi v3.2

+

Downloads

+3Murphi version 3.2 is a patch against Murphi 3.1, available +here, +according to +this +license. You should install and be familiar with Murphi 3.1 before +using 3Murphi. +

+ +Download +3Murphi 3.2 here + +

+

Install Instructions

+To install 3Murphi, save the gzipped patch file into the Murphi 3.1 +directory, along side of include, ex, etc., and apply +the patch: +
patch -p0 < 3murphi-3_2.patch
+This patches files in include, so no rebuilding is necessary other +than compiling verifiers with -DTRIPLE_MURPHI (see instructions above). +
+

The Author(s)

+Peter C. Dillinger, advised by +Panagiotis (Pete) Manolios + +