/****************************** Program "80216e.m" compiled by "Murphi Release 3.1" Murphi Last Modefied Date: "Jan 29 1999" Murphi Last Compiled date: "Jan 8 2004" ******************************/ /******************** Parameter ********************/ #define MURPHI_VERSION "Murphi Release 3.1" #define MURPHI_DATE "Jan 29 1999" #define PROTOCOL_NAME "80216e" #define BITS_IN_WORLD 1712 /******************** Include ********************/ #include "mu_prolog.inc" /******************** Decl declaration ********************/ class mu_1_MSId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_MSId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_MSId& val) { if (val.defined()) return ( s << mu_1_MSId::values[ int(val) - 1 ] ); else return ( s << "Undefined" ); }; mu_1_MSId (char *name, int os): mu__byte(1, 1, 1, name, os) {}; mu_1_MSId (void): mu__byte(1, 1, 1) {}; mu_1_MSId (int val): mu__byte(1, 1, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -1]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 1] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_MSId& a, mu_1_MSId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_MSId::values[] = { "MSId_1",NULL }; /*** end scalarset declaration ***/ mu_1_MSId mu_1_MSId_undefined_var; class mu_1_BSId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_BSId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_BSId& val) { if (val.defined()) return ( s << mu_1_BSId::values[ int(val) - 2 ] ); else return ( s << "Undefined" ); }; mu_1_BSId (char *name, int os): mu__byte(2, 2, 1, name, os) {}; mu_1_BSId (void): mu__byte(2, 2, 1) {}; mu_1_BSId (int val): mu__byte(2, 2, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -2]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 2] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_BSId& a, mu_1_BSId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_BSId::values[] = { "BSId_1",NULL }; /*** end scalarset declaration ***/ mu_1_BSId mu_1_BSId_undefined_var; class mu_1_IntruderId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_IntruderId& val){ return value(val.value());}; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_IntruderId& val) { if (val.defined()) return ( s << mu_1_IntruderId::values[ int(val) - 3 ] ); else return ( s << "Undefined" ); }; mu_1_IntruderId (char *name, int os): mu__byte(3, 3, 1, name, os) {}; mu_1_IntruderId (void): mu__byte(3, 3, 1) {}; mu_1_IntruderId (int val): mu__byte(3, 3, 1, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -3]; }; virtual void print() { if (defined()) cout << name << ':' << values[ value() - 3] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; friend int CompareWeight(mu_1_IntruderId& a, mu_1_IntruderId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); }; char *mu_1_IntruderId::values[] = { "IntruderId_1",NULL }; /*** end scalarset declaration ***/ mu_1_IntruderId mu_1_IntruderId_undefined_var; class mu_1_AgentId: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_AgentId& val) { return value(val.value()); }; inline operator int() const { return value(); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_AgentId& val) { if (val.defined()) return ( s << mu_1_AgentId::values[ val.indexvalue() ] ); else return ( s << "Undefined" ); }; // note thate lb and ub are not used if we have byte compacted state. mu_1_AgentId (char *name, int os): mu__byte(0, 2, 2, name, os) {}; mu_1_AgentId (void): mu__byte(0, 2, 2) {}; mu_1_AgentId (int val): mu__byte(0, 2, 2, "Parameter or function result.", 0) { operator=(val); }; int value() const { int val = mu__byte::value(); // val == -1 if value undefined // we can return it since no enum/scalarsetid will have value -1 if (val == -1) return -1; if (val <= 0) return val+1; if (val <= 1) return val+1; if (val <= 2) return val+1; } inline int value(int val) { if (val == -1) { undefine(); return -1; } if ((val >= 1) && (val <= 1)) return (mu__byte::value(val-1)+1); if ((val >= 2) && (val <= 2)) return (mu__byte::value(val-1)+1); if ((val >= 3) && (val <= 3)) return (mu__byte::value(val-1)+1); } inline int indexvalue() const { return mu__byte::value(); }; inline int unionassign(int val) { return mu__byte::value(val); }; char * Name() { return values[ indexvalue() ]; }; friend int CompareWeight(mu_1_AgentId& a, mu_1_AgentId& b) { if (!a.defined() && b.defined()) return -1; else if (a.defined() && !b.defined()) return 1; else return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void print() { if (defined()) cout << name << ':' << values[ indexvalue() ] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; }; char *mu_1_AgentId::values[] = {"MSId_1","BSId_1","IntruderId_1",NULL }; /*** end union declaration ***/ mu_1_AgentId mu_1_AgentId_undefined_var; class mu_1_Nonce: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1_Nonce& val) { return mu__byte::operator=((int) val); }; mu_1_Nonce (char *name, int os): mu__byte(0, 30, 5, name, os) {}; mu_1_Nonce (void): mu__byte(0, 30, 5) {}; mu_1_Nonce (int val): mu__byte(0, 30, 5, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_Nonce mu_1_Nonce_undefined_var; class mu_1_PN: public mu__long { public: inline int operator=(int val) { return mu__long::operator=(val); }; inline int operator=(const mu_1_PN& val) { return mu__long::operator=((int) val); }; mu_1_PN (char *name, int os): mu__long(-1, 100, 7, name, os) {}; mu_1_PN (void): mu__long(-1, 100, 7) {}; mu_1_PN (int val): mu__long(-1, 100, 7, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_PN mu_1_PN_undefined_var; class mu_1_SessionId: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1_SessionId& val) { return mu__byte::operator=((int) val); }; mu_1_SessionId (char *name, int os): mu__byte(0, 1, 2, name, os) {}; mu_1_SessionId (void): mu__byte(0, 1, 2) {}; mu_1_SessionId (int val): mu__byte(0, 1, 2, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1_SessionId mu_1_SessionId_undefined_var; class mu_1_AK { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_AgentId mu_peer1; mu_1_AgentId mu_peer2; mu_1_AK ( char *n, int os ) { set_self(n,os); }; mu_1_AK ( void ) {}; virtual ~mu_1_AK(); friend int CompareWeight(mu_1_AK& a, mu_1_AK& b) { int w; w = CompareWeight(a.mu_peer1, b.mu_peer1); if (w!=0) return w; w = CompareWeight(a.mu_peer2, b.mu_peer2); if (w!=0) return w; return 0; } friend int Compare(mu_1_AK& a, mu_1_AK& b) { int w; w = Compare(a.mu_peer1, b.mu_peer1); if (w!=0) return w; w = Compare(a.mu_peer2, b.mu_peer2); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_peer1.MultisetSort(); mu_peer2.MultisetSort(); } void print_statistic() { mu_peer1.print_statistic(); mu_peer2.print_statistic(); } void clear() { mu_peer1.clear(); mu_peer2.clear(); }; void undefine() { mu_peer1.undefine(); mu_peer2.undefine(); }; void reset() { mu_peer1.reset(); mu_peer2.reset(); }; void print() { mu_peer1.print(); mu_peer2.print(); }; void print_diff(state *prevstate) { mu_peer1.print_diff(prevstate); mu_peer2.print_diff(prevstate); }; void to_state(state *thestate) { mu_peer1.to_state(thestate); mu_peer2.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_AK& operator= (const mu_1_AK& from) { mu_peer1.value(from.mu_peer1.value()); mu_peer2.value(from.mu_peer2.value()); return *this; }; }; void mu_1_AK::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_AK::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_AK::set_self(char *n, int os) { name = n; mu_peer1.set_self_2(name, ".peer1", os + 0 ); mu_peer2.set_self_2(name, ".peer2", os + 2 ); } mu_1_AK::~mu_1_AK() { } /*** end record declaration ***/ mu_1_AK mu_1_AK_undefined_var; class mu_1_MessageType: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_MessageType& val) { return value(val.value()); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_MessageType& val) { if (val.defined()) return ( s << mu_1_MessageType::values[ int(val) - 4] ); else return ( s << "Undefined" ); }; mu_1_MessageType (char *name, int os): mu__byte(4, 6, 2, name, os) {}; mu_1_MessageType (void): mu__byte(4, 6, 2) {}; mu_1_MessageType (int val): mu__byte(4, 6, 2, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -4]; }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; virtual void print() { if (defined()) cout << name << ":" << values[ value() -4] << '\n'; else cout << name << ":Undefined\n"; }; }; char *mu_1_MessageType::values[] = {"M_1","M_2","M_3",NULL }; /*** end of enum declaration ***/ mu_1_MessageType mu_1_MessageType_undefined_var; class mu_1_MAC { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_AK mu_ak; mu_1_Nonce mu_MSnonce; mu_1_Nonce mu_BSnonce; mu_1_Nonce mu_TEKnonce; mu_1_MessageType mu_mtype; mu_1_MAC ( char *n, int os ) { set_self(n,os); }; mu_1_MAC ( void ) {}; virtual ~mu_1_MAC(); friend int CompareWeight(mu_1_MAC& a, mu_1_MAC& b) { int w; w = CompareWeight(a.mu_ak, b.mu_ak); if (w!=0) return w; w = CompareWeight(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = CompareWeight(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = CompareWeight(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = CompareWeight(a.mu_mtype, b.mu_mtype); if (w!=0) return w; return 0; } friend int Compare(mu_1_MAC& a, mu_1_MAC& b) { int w; w = Compare(a.mu_ak, b.mu_ak); if (w!=0) return w; w = Compare(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = Compare(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = Compare(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = Compare(a.mu_mtype, b.mu_mtype); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_ak.MultisetSort(); mu_MSnonce.MultisetSort(); mu_BSnonce.MultisetSort(); mu_TEKnonce.MultisetSort(); mu_mtype.MultisetSort(); } void print_statistic() { mu_ak.print_statistic(); mu_MSnonce.print_statistic(); mu_BSnonce.print_statistic(); mu_TEKnonce.print_statistic(); mu_mtype.print_statistic(); } void clear() { mu_ak.clear(); mu_MSnonce.clear(); mu_BSnonce.clear(); mu_TEKnonce.clear(); mu_mtype.clear(); }; void undefine() { mu_ak.undefine(); mu_MSnonce.undefine(); mu_BSnonce.undefine(); mu_TEKnonce.undefine(); mu_mtype.undefine(); }; void reset() { mu_ak.reset(); mu_MSnonce.reset(); mu_BSnonce.reset(); mu_TEKnonce.reset(); mu_mtype.reset(); }; void print() { mu_ak.print(); mu_MSnonce.print(); mu_BSnonce.print(); mu_TEKnonce.print(); mu_mtype.print(); }; void print_diff(state *prevstate) { mu_ak.print_diff(prevstate); mu_MSnonce.print_diff(prevstate); mu_BSnonce.print_diff(prevstate); mu_TEKnonce.print_diff(prevstate); mu_mtype.print_diff(prevstate); }; void to_state(state *thestate) { mu_ak.to_state(thestate); mu_MSnonce.to_state(thestate); mu_BSnonce.to_state(thestate); mu_TEKnonce.to_state(thestate); mu_mtype.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_MAC& operator= (const mu_1_MAC& from) { mu_ak = from.mu_ak; mu_MSnonce.value(from.mu_MSnonce.value()); mu_BSnonce.value(from.mu_BSnonce.value()); mu_TEKnonce.value(from.mu_TEKnonce.value()); mu_mtype.value(from.mu_mtype.value()); return *this; }; }; void mu_1_MAC::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_MAC::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_MAC::set_self(char *n, int os) { name = n; mu_ak.set_self_2(name, ".ak", os + 0 ); mu_MSnonce.set_self_2(name, ".MSnonce", os + 4 ); mu_BSnonce.set_self_2(name, ".BSnonce", os + 9 ); mu_TEKnonce.set_self_2(name, ".TEKnonce", os + 14 ); mu_mtype.set_self_2(name, ".mtype", os + 19 ); } mu_1_MAC::~mu_1_MAC() { } /*** end record declaration ***/ mu_1_MAC mu_1_MAC_undefined_var; class mu_1_Message { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_AgentId mu_source; mu_1_AgentId mu_dest; mu_1_MessageType mu_mtype; mu_1_Nonce mu_BSnonce; mu_1_Nonce mu_MSnonce; mu_1_Nonce mu_TEKnonce; mu_1_AgentId mu_address; mu_1_PN mu_pn; mu_1_MAC mu_mac; mu_1_Message ( char *n, int os ) { set_self(n,os); }; mu_1_Message ( void ) {}; virtual ~mu_1_Message(); friend int CompareWeight(mu_1_Message& a, mu_1_Message& b) { int w; w = CompareWeight(a.mu_source, b.mu_source); if (w!=0) return w; w = CompareWeight(a.mu_dest, b.mu_dest); if (w!=0) return w; w = CompareWeight(a.mu_mtype, b.mu_mtype); if (w!=0) return w; w = CompareWeight(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = CompareWeight(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = CompareWeight(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = CompareWeight(a.mu_address, b.mu_address); if (w!=0) return w; w = CompareWeight(a.mu_pn, b.mu_pn); if (w!=0) return w; w = CompareWeight(a.mu_mac, b.mu_mac); if (w!=0) return w; return 0; } friend int Compare(mu_1_Message& a, mu_1_Message& b) { int w; w = Compare(a.mu_source, b.mu_source); if (w!=0) return w; w = Compare(a.mu_dest, b.mu_dest); if (w!=0) return w; w = Compare(a.mu_mtype, b.mu_mtype); if (w!=0) return w; w = Compare(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = Compare(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = Compare(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = Compare(a.mu_address, b.mu_address); if (w!=0) return w; w = Compare(a.mu_pn, b.mu_pn); if (w!=0) return w; w = Compare(a.mu_mac, b.mu_mac); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_source.MultisetSort(); mu_dest.MultisetSort(); mu_mtype.MultisetSort(); mu_BSnonce.MultisetSort(); mu_MSnonce.MultisetSort(); mu_TEKnonce.MultisetSort(); mu_address.MultisetSort(); mu_pn.MultisetSort(); mu_mac.MultisetSort(); } void print_statistic() { mu_source.print_statistic(); mu_dest.print_statistic(); mu_mtype.print_statistic(); mu_BSnonce.print_statistic(); mu_MSnonce.print_statistic(); mu_TEKnonce.print_statistic(); mu_address.print_statistic(); mu_pn.print_statistic(); mu_mac.print_statistic(); } void clear() { mu_source.clear(); mu_dest.clear(); mu_mtype.clear(); mu_BSnonce.clear(); mu_MSnonce.clear(); mu_TEKnonce.clear(); mu_address.clear(); mu_pn.clear(); mu_mac.clear(); }; void undefine() { mu_source.undefine(); mu_dest.undefine(); mu_mtype.undefine(); mu_BSnonce.undefine(); mu_MSnonce.undefine(); mu_TEKnonce.undefine(); mu_address.undefine(); mu_pn.undefine(); mu_mac.undefine(); }; void reset() { mu_source.reset(); mu_dest.reset(); mu_mtype.reset(); mu_BSnonce.reset(); mu_MSnonce.reset(); mu_TEKnonce.reset(); mu_address.reset(); mu_pn.reset(); mu_mac.reset(); }; void print() { mu_source.print(); mu_dest.print(); mu_mtype.print(); mu_BSnonce.print(); mu_MSnonce.print(); mu_TEKnonce.print(); mu_address.print(); mu_pn.print(); mu_mac.print(); }; void print_diff(state *prevstate) { mu_source.print_diff(prevstate); mu_dest.print_diff(prevstate); mu_mtype.print_diff(prevstate); mu_BSnonce.print_diff(prevstate); mu_MSnonce.print_diff(prevstate); mu_TEKnonce.print_diff(prevstate); mu_address.print_diff(prevstate); mu_pn.print_diff(prevstate); mu_mac.print_diff(prevstate); }; void to_state(state *thestate) { mu_source.to_state(thestate); mu_dest.to_state(thestate); mu_mtype.to_state(thestate); mu_BSnonce.to_state(thestate); mu_MSnonce.to_state(thestate); mu_TEKnonce.to_state(thestate); mu_address.to_state(thestate); mu_pn.to_state(thestate); mu_mac.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Message& operator= (const mu_1_Message& from) { mu_source.value(from.mu_source.value()); mu_dest.value(from.mu_dest.value()); mu_mtype.value(from.mu_mtype.value()); mu_BSnonce.value(from.mu_BSnonce.value()); mu_MSnonce.value(from.mu_MSnonce.value()); mu_TEKnonce.value(from.mu_TEKnonce.value()); mu_address.value(from.mu_address.value()); mu_pn.value(from.mu_pn.value()); mu_mac = from.mu_mac; return *this; }; }; void mu_1_Message::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Message::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Message::set_self(char *n, int os) { name = n; mu_source.set_self_2(name, ".source", os + 0 ); mu_dest.set_self_2(name, ".dest", os + 2 ); mu_mtype.set_self_2(name, ".mtype", os + 4 ); mu_BSnonce.set_self_2(name, ".BSnonce", os + 6 ); mu_MSnonce.set_self_2(name, ".MSnonce", os + 11 ); mu_TEKnonce.set_self_2(name, ".TEKnonce", os + 16 ); mu_address.set_self_2(name, ".address", os + 21 ); mu_pn.set_self_2(name, ".pn", os + 23 ); mu_mac.set_self_2(name, ".mac", os + 30 ); } mu_1_Message::~mu_1_Message() { } /*** end record declaration ***/ mu_1_Message mu_1_Message_undefined_var; class mu_1_MSStates: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_MSStates& val) { return value(val.value()); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_MSStates& val) { if (val.defined()) return ( s << mu_1_MSStates::values[ int(val) - 7] ); else return ( s << "Undefined" ); }; mu_1_MSStates (char *name, int os): mu__byte(7, 9, 2, name, os) {}; mu_1_MSStates (void): mu__byte(7, 9, 2) {}; mu_1_MSStates (int val): mu__byte(7, 9, 2, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -7]; }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; virtual void print() { if (defined()) cout << name << ":" << values[ value() -7] << '\n'; else cout << name << ":Undefined\n"; }; }; char *mu_1_MSStates::values[] = {"MS_WAIT_CLG","MS_WAIT_RES","MS_DONE",NULL }; /*** end of enum declaration ***/ mu_1_MSStates mu_1_MSStates_undefined_var; class mu_1__type_0: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1__type_0& val) { return mu__byte::operator=((int) val); }; mu_1__type_0 (char *name, int os): mu__byte(0, 200, 8, name, os) {}; mu_1__type_0 (void): mu__byte(0, 200, 8) {}; mu_1__type_0 (int val): mu__byte(0, 200, 8, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1__type_0 mu_1__type_0_undefined_var; class mu_1__type_1: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1__type_1& val) { return mu__byte::operator=((int) val); }; mu_1__type_1 (char *name, int os): mu__byte(0, 200, 8, name, os) {}; mu_1__type_1 (void): mu__byte(0, 200, 8) {}; mu_1__type_1 (int val): mu__byte(0, 200, 8, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1__type_1 mu_1__type_1_undefined_var; class mu_1_MSSessions { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_MSStates mu_state; mu_1_AK mu_ak; mu_1__type_0 mu_costs; mu_1__type_1 mu_intCosts; mu_1_MSSessions ( char *n, int os ) { set_self(n,os); }; mu_1_MSSessions ( void ) {}; virtual ~mu_1_MSSessions(); friend int CompareWeight(mu_1_MSSessions& a, mu_1_MSSessions& b) { int w; w = CompareWeight(a.mu_state, b.mu_state); if (w!=0) return w; w = CompareWeight(a.mu_ak, b.mu_ak); if (w!=0) return w; w = CompareWeight(a.mu_costs, b.mu_costs); if (w!=0) return w; w = CompareWeight(a.mu_intCosts, b.mu_intCosts); if (w!=0) return w; return 0; } friend int Compare(mu_1_MSSessions& a, mu_1_MSSessions& b) { int w; w = Compare(a.mu_state, b.mu_state); if (w!=0) return w; w = Compare(a.mu_ak, b.mu_ak); if (w!=0) return w; w = Compare(a.mu_costs, b.mu_costs); if (w!=0) return w; w = Compare(a.mu_intCosts, b.mu_intCosts); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_state.MultisetSort(); mu_ak.MultisetSort(); mu_costs.MultisetSort(); mu_intCosts.MultisetSort(); } void print_statistic() { mu_state.print_statistic(); mu_ak.print_statistic(); mu_costs.print_statistic(); mu_intCosts.print_statistic(); } void clear() { mu_state.clear(); mu_ak.clear(); mu_costs.clear(); mu_intCosts.clear(); }; void undefine() { mu_state.undefine(); mu_ak.undefine(); mu_costs.undefine(); mu_intCosts.undefine(); }; void reset() { mu_state.reset(); mu_ak.reset(); mu_costs.reset(); mu_intCosts.reset(); }; void print() { mu_state.print(); mu_ak.print(); mu_costs.print(); mu_intCosts.print(); }; void print_diff(state *prevstate) { mu_state.print_diff(prevstate); mu_ak.print_diff(prevstate); mu_costs.print_diff(prevstate); mu_intCosts.print_diff(prevstate); }; void to_state(state *thestate) { mu_state.to_state(thestate); mu_ak.to_state(thestate); mu_costs.to_state(thestate); mu_intCosts.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_MSSessions& operator= (const mu_1_MSSessions& from) { mu_state.value(from.mu_state.value()); mu_ak = from.mu_ak; mu_costs.value(from.mu_costs.value()); mu_intCosts.value(from.mu_intCosts.value()); return *this; }; }; void mu_1_MSSessions::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_MSSessions::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_MSSessions::set_self(char *n, int os) { name = n; mu_state.set_self_2(name, ".state", os + 0 ); mu_ak.set_self_2(name, ".ak", os + 2 ); mu_costs.set_self_2(name, ".costs", os + 6 ); mu_intCosts.set_self_2(name, ".intCosts", os + 14 ); } mu_1_MSSessions::~mu_1_MSSessions() { } /*** end record declaration ***/ mu_1_MSSessions mu_1_MSSessions_undefined_var; class mu_1_MSAssociations { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_MSSessions mu_session; mu_1_SessionId mu_sid; mu_1_AgentId mu_peer; mu_1_Nonce mu_MSnonce; mu_1_Nonce mu_BSnonce; mu_1_Nonce mu_TEKnonce; mu_1_PN mu_lastKnownPN; mu_1_MSAssociations ( char *n, int os ) { set_self(n,os); }; mu_1_MSAssociations ( void ) {}; virtual ~mu_1_MSAssociations(); friend int CompareWeight(mu_1_MSAssociations& a, mu_1_MSAssociations& b) { int w; w = CompareWeight(a.mu_session, b.mu_session); if (w!=0) return w; w = CompareWeight(a.mu_sid, b.mu_sid); if (w!=0) return w; w = CompareWeight(a.mu_peer, b.mu_peer); if (w!=0) return w; w = CompareWeight(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = CompareWeight(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = CompareWeight(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = CompareWeight(a.mu_lastKnownPN, b.mu_lastKnownPN); if (w!=0) return w; return 0; } friend int Compare(mu_1_MSAssociations& a, mu_1_MSAssociations& b) { int w; w = Compare(a.mu_session, b.mu_session); if (w!=0) return w; w = Compare(a.mu_sid, b.mu_sid); if (w!=0) return w; w = Compare(a.mu_peer, b.mu_peer); if (w!=0) return w; w = Compare(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = Compare(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = Compare(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; w = Compare(a.mu_lastKnownPN, b.mu_lastKnownPN); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_session.MultisetSort(); mu_sid.MultisetSort(); mu_peer.MultisetSort(); mu_MSnonce.MultisetSort(); mu_BSnonce.MultisetSort(); mu_TEKnonce.MultisetSort(); mu_lastKnownPN.MultisetSort(); } void print_statistic() { mu_session.print_statistic(); mu_sid.print_statistic(); mu_peer.print_statistic(); mu_MSnonce.print_statistic(); mu_BSnonce.print_statistic(); mu_TEKnonce.print_statistic(); mu_lastKnownPN.print_statistic(); } void clear() { mu_session.clear(); mu_sid.clear(); mu_peer.clear(); mu_MSnonce.clear(); mu_BSnonce.clear(); mu_TEKnonce.clear(); mu_lastKnownPN.clear(); }; void undefine() { mu_session.undefine(); mu_sid.undefine(); mu_peer.undefine(); mu_MSnonce.undefine(); mu_BSnonce.undefine(); mu_TEKnonce.undefine(); mu_lastKnownPN.undefine(); }; void reset() { mu_session.reset(); mu_sid.reset(); mu_peer.reset(); mu_MSnonce.reset(); mu_BSnonce.reset(); mu_TEKnonce.reset(); mu_lastKnownPN.reset(); }; void print() { mu_session.print(); mu_sid.print(); mu_peer.print(); mu_MSnonce.print(); mu_BSnonce.print(); mu_TEKnonce.print(); mu_lastKnownPN.print(); }; void print_diff(state *prevstate) { mu_session.print_diff(prevstate); mu_sid.print_diff(prevstate); mu_peer.print_diff(prevstate); mu_MSnonce.print_diff(prevstate); mu_BSnonce.print_diff(prevstate); mu_TEKnonce.print_diff(prevstate); mu_lastKnownPN.print_diff(prevstate); }; void to_state(state *thestate) { mu_session.to_state(thestate); mu_sid.to_state(thestate); mu_peer.to_state(thestate); mu_MSnonce.to_state(thestate); mu_BSnonce.to_state(thestate); mu_TEKnonce.to_state(thestate); mu_lastKnownPN.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_MSAssociations& operator= (const mu_1_MSAssociations& from) { mu_session = from.mu_session; mu_sid.value(from.mu_sid.value()); mu_peer.value(from.mu_peer.value()); mu_MSnonce.value(from.mu_MSnonce.value()); mu_BSnonce.value(from.mu_BSnonce.value()); mu_TEKnonce.value(from.mu_TEKnonce.value()); mu_lastKnownPN.value(from.mu_lastKnownPN.value()); return *this; }; }; void mu_1_MSAssociations::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_MSAssociations::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_MSAssociations::set_self(char *n, int os) { name = n; mu_session.set_self_2(name, ".session", os + 0 ); mu_sid.set_self_2(name, ".sid", os + 22 ); mu_peer.set_self_2(name, ".peer", os + 24 ); mu_MSnonce.set_self_2(name, ".MSnonce", os + 26 ); mu_BSnonce.set_self_2(name, ".BSnonce", os + 31 ); mu_TEKnonce.set_self_2(name, ".TEKnonce", os + 36 ); mu_lastKnownPN.set_self_2(name, ".lastKnownPN", os + 41 ); } mu_1_MSAssociations::~mu_1_MSAssociations() { } /*** end record declaration ***/ mu_1_MSAssociations mu_1_MSAssociations_undefined_var; class mu_1__type_2 { public: mu_1_MSAssociations array[ 3 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_2 (char *n, int os) { set_self(n, os); }; mu_1__type_2 ( void ) {}; virtual ~mu_1__type_2 (); mu_1_MSAssociations& operator[] (int index) /* const */ { if ( ( index >= 1 ) && ( index <= 1 ) ) return array[ index - (1) ]; if ( ( index >= 2 ) && ( index <= 2 ) ) return array[ index - (1) ]; if ( ( index >= 3 ) && ( index <= 3 ) ) return array[ index - (1) ]; if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s. (Internal Error in Type Checking.",index, name); return array[0]; } mu_1__type_2& operator= (const mu_1__type_2& from) { for (int i = 0; i < 3; i++) array[i] = from.array[i]; return *this; } friend int CompareWeight(mu_1__type_2& a, mu_1__type_2& b) { int w; for (int i=0; i<3; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_2& a, mu_1__type_2& b) { int w; for (int i=0; i<3; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<3; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<3; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 3; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 3; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 3; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 3; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 3; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 3; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_2::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_2::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_2::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"MSId_1", i * 48 + os);i++; array[i].set_self_ar(n,"BSId_1", i * 48 + os);i++; array[i].set_self_ar(n,"IntruderId_1", i * 48 + os);i++; } mu_1__type_2::~mu_1__type_2() { } /*** end array declaration ***/ mu_1__type_2 mu_1__type_2_undefined_var; class mu_1_MS { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1__type_2 mu_associations; mu_1_MS ( char *n, int os ) { set_self(n,os); }; mu_1_MS ( void ) {}; virtual ~mu_1_MS(); friend int CompareWeight(mu_1_MS& a, mu_1_MS& b) { int w; w = CompareWeight(a.mu_associations, b.mu_associations); if (w!=0) return w; return 0; } friend int Compare(mu_1_MS& a, mu_1_MS& b) { int w; w = Compare(a.mu_associations, b.mu_associations); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_associations.MultisetSort(); } void print_statistic() { mu_associations.print_statistic(); } void clear() { mu_associations.clear(); }; void undefine() { mu_associations.undefine(); }; void reset() { mu_associations.reset(); }; void print() { mu_associations.print(); }; void print_diff(state *prevstate) { mu_associations.print_diff(prevstate); }; void to_state(state *thestate) { mu_associations.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_MS& operator= (const mu_1_MS& from) { mu_associations = from.mu_associations; return *this; }; }; void mu_1_MS::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_MS::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_MS::set_self(char *n, int os) { name = n; mu_associations.set_self_2(name, ".associations", os + 0 ); } mu_1_MS::~mu_1_MS() { } /*** end record declaration ***/ mu_1_MS mu_1_MS_undefined_var; class mu_1_BSStates: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1_BSStates& val) { return value(val.value()); }; static char *values[]; friend ostream& operator<< (ostream& s, mu_1_BSStates& val) { if (val.defined()) return ( s << mu_1_BSStates::values[ int(val) - 10] ); else return ( s << "Undefined" ); }; mu_1_BSStates (char *name, int os): mu__byte(10, 12, 2, name, os) {}; mu_1_BSStates (void): mu__byte(10, 12, 2) {}; mu_1_BSStates (int val): mu__byte(10, 12, 2, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return values[ value() -10]; }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; virtual void print() { if (defined()) cout << name << ":" << values[ value() -10] << '\n'; else cout << name << ":Undefined\n"; }; }; char *mu_1_BSStates::values[] = {"BS_START","BS_WAIT_REQ","BS_DONE",NULL }; /*** end of enum declaration ***/ mu_1_BSStates mu_1_BSStates_undefined_var; class mu_1__type_3: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1__type_3& val) { return mu__byte::operator=((int) val); }; mu_1__type_3 (char *name, int os): mu__byte(0, 200, 8, name, os) {}; mu_1__type_3 (void): mu__byte(0, 200, 8) {}; mu_1__type_3 (int val): mu__byte(0, 200, 8, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1__type_3 mu_1__type_3_undefined_var; class mu_1__type_4: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1__type_4& val) { return mu__byte::operator=((int) val); }; mu_1__type_4 (char *name, int os): mu__byte(0, 200, 8, name, os) {}; mu_1__type_4 (void): mu__byte(0, 200, 8) {}; mu_1__type_4 (int val): mu__byte(0, 200, 8, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1__type_4 mu_1__type_4_undefined_var; class mu_1_BSSessions { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_BSStates mu_state; mu_1_AK mu_ak; mu_1__type_3 mu_costs; mu_1__type_4 mu_intCosts; mu_1_BSSessions ( char *n, int os ) { set_self(n,os); }; mu_1_BSSessions ( void ) {}; virtual ~mu_1_BSSessions(); friend int CompareWeight(mu_1_BSSessions& a, mu_1_BSSessions& b) { int w; w = CompareWeight(a.mu_state, b.mu_state); if (w!=0) return w; w = CompareWeight(a.mu_ak, b.mu_ak); if (w!=0) return w; w = CompareWeight(a.mu_costs, b.mu_costs); if (w!=0) return w; w = CompareWeight(a.mu_intCosts, b.mu_intCosts); if (w!=0) return w; return 0; } friend int Compare(mu_1_BSSessions& a, mu_1_BSSessions& b) { int w; w = Compare(a.mu_state, b.mu_state); if (w!=0) return w; w = Compare(a.mu_ak, b.mu_ak); if (w!=0) return w; w = Compare(a.mu_costs, b.mu_costs); if (w!=0) return w; w = Compare(a.mu_intCosts, b.mu_intCosts); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_state.MultisetSort(); mu_ak.MultisetSort(); mu_costs.MultisetSort(); mu_intCosts.MultisetSort(); } void print_statistic() { mu_state.print_statistic(); mu_ak.print_statistic(); mu_costs.print_statistic(); mu_intCosts.print_statistic(); } void clear() { mu_state.clear(); mu_ak.clear(); mu_costs.clear(); mu_intCosts.clear(); }; void undefine() { mu_state.undefine(); mu_ak.undefine(); mu_costs.undefine(); mu_intCosts.undefine(); }; void reset() { mu_state.reset(); mu_ak.reset(); mu_costs.reset(); mu_intCosts.reset(); }; void print() { mu_state.print(); mu_ak.print(); mu_costs.print(); mu_intCosts.print(); }; void print_diff(state *prevstate) { mu_state.print_diff(prevstate); mu_ak.print_diff(prevstate); mu_costs.print_diff(prevstate); mu_intCosts.print_diff(prevstate); }; void to_state(state *thestate) { mu_state.to_state(thestate); mu_ak.to_state(thestate); mu_costs.to_state(thestate); mu_intCosts.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_BSSessions& operator= (const mu_1_BSSessions& from) { mu_state.value(from.mu_state.value()); mu_ak = from.mu_ak; mu_costs.value(from.mu_costs.value()); mu_intCosts.value(from.mu_intCosts.value()); return *this; }; }; void mu_1_BSSessions::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_BSSessions::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_BSSessions::set_self(char *n, int os) { name = n; mu_state.set_self_2(name, ".state", os + 0 ); mu_ak.set_self_2(name, ".ak", os + 2 ); mu_costs.set_self_2(name, ".costs", os + 6 ); mu_intCosts.set_self_2(name, ".intCosts", os + 14 ); } mu_1_BSSessions::~mu_1_BSSessions() { } /*** end record declaration ***/ mu_1_BSSessions mu_1_BSSessions_undefined_var; class mu_1_BSAssociations { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1_BSSessions mu_session; mu_1_SessionId mu_sid; mu_1_AgentId mu_peer; mu_1_Nonce mu_BSnonce; mu_1_Nonce mu_MSnonce; mu_1_Nonce mu_TEKnonce; mu_1_BSAssociations ( char *n, int os ) { set_self(n,os); }; mu_1_BSAssociations ( void ) {}; virtual ~mu_1_BSAssociations(); friend int CompareWeight(mu_1_BSAssociations& a, mu_1_BSAssociations& b) { int w; w = CompareWeight(a.mu_session, b.mu_session); if (w!=0) return w; w = CompareWeight(a.mu_sid, b.mu_sid); if (w!=0) return w; w = CompareWeight(a.mu_peer, b.mu_peer); if (w!=0) return w; w = CompareWeight(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = CompareWeight(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = CompareWeight(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; return 0; } friend int Compare(mu_1_BSAssociations& a, mu_1_BSAssociations& b) { int w; w = Compare(a.mu_session, b.mu_session); if (w!=0) return w; w = Compare(a.mu_sid, b.mu_sid); if (w!=0) return w; w = Compare(a.mu_peer, b.mu_peer); if (w!=0) return w; w = Compare(a.mu_BSnonce, b.mu_BSnonce); if (w!=0) return w; w = Compare(a.mu_MSnonce, b.mu_MSnonce); if (w!=0) return w; w = Compare(a.mu_TEKnonce, b.mu_TEKnonce); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_session.MultisetSort(); mu_sid.MultisetSort(); mu_peer.MultisetSort(); mu_BSnonce.MultisetSort(); mu_MSnonce.MultisetSort(); mu_TEKnonce.MultisetSort(); } void print_statistic() { mu_session.print_statistic(); mu_sid.print_statistic(); mu_peer.print_statistic(); mu_BSnonce.print_statistic(); mu_MSnonce.print_statistic(); mu_TEKnonce.print_statistic(); } void clear() { mu_session.clear(); mu_sid.clear(); mu_peer.clear(); mu_BSnonce.clear(); mu_MSnonce.clear(); mu_TEKnonce.clear(); }; void undefine() { mu_session.undefine(); mu_sid.undefine(); mu_peer.undefine(); mu_BSnonce.undefine(); mu_MSnonce.undefine(); mu_TEKnonce.undefine(); }; void reset() { mu_session.reset(); mu_sid.reset(); mu_peer.reset(); mu_BSnonce.reset(); mu_MSnonce.reset(); mu_TEKnonce.reset(); }; void print() { mu_session.print(); mu_sid.print(); mu_peer.print(); mu_BSnonce.print(); mu_MSnonce.print(); mu_TEKnonce.print(); }; void print_diff(state *prevstate) { mu_session.print_diff(prevstate); mu_sid.print_diff(prevstate); mu_peer.print_diff(prevstate); mu_BSnonce.print_diff(prevstate); mu_MSnonce.print_diff(prevstate); mu_TEKnonce.print_diff(prevstate); }; void to_state(state *thestate) { mu_session.to_state(thestate); mu_sid.to_state(thestate); mu_peer.to_state(thestate); mu_BSnonce.to_state(thestate); mu_MSnonce.to_state(thestate); mu_TEKnonce.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_BSAssociations& operator= (const mu_1_BSAssociations& from) { mu_session = from.mu_session; mu_sid.value(from.mu_sid.value()); mu_peer.value(from.mu_peer.value()); mu_BSnonce.value(from.mu_BSnonce.value()); mu_MSnonce.value(from.mu_MSnonce.value()); mu_TEKnonce.value(from.mu_TEKnonce.value()); return *this; }; }; void mu_1_BSAssociations::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_BSAssociations::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_BSAssociations::set_self(char *n, int os) { name = n; mu_session.set_self_2(name, ".session", os + 0 ); mu_sid.set_self_2(name, ".sid", os + 22 ); mu_peer.set_self_2(name, ".peer", os + 24 ); mu_BSnonce.set_self_2(name, ".BSnonce", os + 26 ); mu_MSnonce.set_self_2(name, ".MSnonce", os + 31 ); mu_TEKnonce.set_self_2(name, ".TEKnonce", os + 36 ); } mu_1_BSAssociations::~mu_1_BSAssociations() { } /*** end record declaration ***/ mu_1_BSAssociations mu_1_BSAssociations_undefined_var; class mu_1__type_5 { public: mu_1_BSAssociations array[ 3 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_5 (char *n, int os) { set_self(n, os); }; mu_1__type_5 ( void ) {}; virtual ~mu_1__type_5 (); mu_1_BSAssociations& operator[] (int index) /* const */ { if ( ( index >= 1 ) && ( index <= 1 ) ) return array[ index - (1) ]; if ( ( index >= 2 ) && ( index <= 2 ) ) return array[ index - (1) ]; if ( ( index >= 3 ) && ( index <= 3 ) ) return array[ index - (1) ]; if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s. (Internal Error in Type Checking.",index, name); return array[0]; } mu_1__type_5& operator= (const mu_1__type_5& from) { for (int i = 0; i < 3; i++) array[i] = from.array[i]; return *this; } friend int CompareWeight(mu_1__type_5& a, mu_1__type_5& b) { int w; for (int i=0; i<3; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_5& a, mu_1__type_5& b) { int w; for (int i=0; i<3; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<3; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<3; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 3; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 3; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 3; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 3; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 3; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 3; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_5::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_5::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_5::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"MSId_1", i * 41 + os);i++; array[i].set_self_ar(n,"BSId_1", i * 41 + os);i++; array[i].set_self_ar(n,"IntruderId_1", i * 41 + os);i++; } mu_1__type_5::~mu_1__type_5() { } /*** end array declaration ***/ mu_1__type_5 mu_1__type_5_undefined_var; class mu_1_BS { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1__type_5 mu_associations; mu_1_BS ( char *n, int os ) { set_self(n,os); }; mu_1_BS ( void ) {}; virtual ~mu_1_BS(); friend int CompareWeight(mu_1_BS& a, mu_1_BS& b) { int w; w = CompareWeight(a.mu_associations, b.mu_associations); if (w!=0) return w; return 0; } friend int Compare(mu_1_BS& a, mu_1_BS& b) { int w; w = Compare(a.mu_associations, b.mu_associations); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_associations.MultisetSort(); } void print_statistic() { mu_associations.print_statistic(); } void clear() { mu_associations.clear(); }; void undefine() { mu_associations.undefine(); }; void reset() { mu_associations.reset(); }; void print() { mu_associations.print(); }; void print_diff(state *prevstate) { mu_associations.print_diff(prevstate); }; void to_state(state *thestate) { mu_associations.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_BS& operator= (const mu_1_BS& from) { mu_associations = from.mu_associations; return *this; }; }; void mu_1_BS::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_BS::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_BS::set_self(char *n, int os) { name = n; mu_associations.set_self_2(name, ".associations", os + 0 ); } mu_1_BS::~mu_1_BS() { } /*** end record declaration ***/ mu_1_BS mu_1_BS_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_6_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_6_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_6_id () : mu__byte(0,9,0) {}; mu_1__type_6_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_6 { public: mu_1_Nonce array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_6 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_6 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_6 (); mu_1_Nonce& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_6& operator= (const mu_1__type_6& from) { for (int i = 0; i < 10; i++) { array[i].value(from.array[i].value()); valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_6& a, mu_1__type_6& b) { return 0; } friend int Compare(mu_1__type_6& a, mu_1__type_6& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_6_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Nonce temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_6::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_6::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_6::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 5 + os); k = os + i * 5; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_6::~mu_1__type_6() { } /*** end multiset declaration ***/ mu_1__type_6 mu_1__type_6_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_7_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_7_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_7_id () : mu__byte(0,9,0) {}; mu_1__type_7_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_7 { public: mu_1_Nonce array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_7 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_7 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_7 (); mu_1_Nonce& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_7& operator= (const mu_1__type_7& from) { for (int i = 0; i < 10; i++) { array[i].value(from.array[i].value()); valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_7& a, mu_1__type_7& b) { return 0; } friend int Compare(mu_1__type_7& a, mu_1__type_7& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_7_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Nonce temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_7::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_7::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_7::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 5 + os); k = os + i * 5; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_7::~mu_1__type_7() { } /*** end multiset declaration ***/ mu_1__type_7 mu_1__type_7_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_8_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_8_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_8_id () : mu__byte(0,9,0) {}; mu_1__type_8_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_8 { public: mu_1_MAC array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_8 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_8 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_8 (); mu_1_MAC& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_8& operator= (const mu_1__type_8& from) { for (int i = 0; i < 10; i++) { array[i] = from.array[i]; valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_8& a, mu_1__type_8& b) { return 0; } friend int Compare(mu_1__type_8& a, mu_1__type_8& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_8_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_MAC temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_8::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_8::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_8::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 21 + os); k = os + i * 21; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_8::~mu_1__type_8() { } /*** end multiset declaration ***/ mu_1__type_8 mu_1__type_8_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_9_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_9_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_9_id () : mu__byte(0,9,0) {}; mu_1__type_9_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_9 { public: mu_1_Message array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_9 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_9 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_9 (); mu_1_Message& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_9& operator= (const mu_1__type_9& from) { for (int i = 0; i < 10; i++) { array[i] = from.array[i]; valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_9& a, mu_1__type_9& b) { return 0; } friend int Compare(mu_1__type_9& a, mu_1__type_9& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_9_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Message temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_9::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_9::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_9::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 51 + os); k = os + i * 51; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_9::~mu_1__type_9() { } /*** end multiset declaration ***/ mu_1__type_9 mu_1__type_9_undefined_var; class mu_1_Intruder { public: char *name; char longname[BUFFER_SIZE/4]; void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); void set_self(char *n, int os); mu_1__type_6 mu_nonces; mu_1__type_7 mu_TEKnonces; mu_1__type_8 mu_macs; mu_1__type_9 mu_messages; mu_1_Intruder ( char *n, int os ) { set_self(n,os); }; mu_1_Intruder ( void ) {}; virtual ~mu_1_Intruder(); friend int CompareWeight(mu_1_Intruder& a, mu_1_Intruder& b) { int w; w = CompareWeight(a.mu_nonces, b.mu_nonces); if (w!=0) return w; w = CompareWeight(a.mu_TEKnonces, b.mu_TEKnonces); if (w!=0) return w; w = CompareWeight(a.mu_macs, b.mu_macs); if (w!=0) return w; w = CompareWeight(a.mu_messages, b.mu_messages); if (w!=0) return w; return 0; } friend int Compare(mu_1_Intruder& a, mu_1_Intruder& b) { int w; w = Compare(a.mu_nonces, b.mu_nonces); if (w!=0) return w; w = Compare(a.mu_TEKnonces, b.mu_TEKnonces); if (w!=0) return w; w = Compare(a.mu_macs, b.mu_macs); if (w!=0) return w; w = Compare(a.mu_messages, b.mu_messages); if (w!=0) return w; return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { mu_nonces.MultisetSort(); mu_TEKnonces.MultisetSort(); mu_macs.MultisetSort(); mu_messages.MultisetSort(); } void print_statistic() { mu_nonces.print_statistic(); mu_TEKnonces.print_statistic(); mu_macs.print_statistic(); mu_messages.print_statistic(); } void clear() { mu_nonces.clear(); mu_TEKnonces.clear(); mu_macs.clear(); mu_messages.clear(); }; void undefine() { mu_nonces.undefine(); mu_TEKnonces.undefine(); mu_macs.undefine(); mu_messages.undefine(); }; void reset() { mu_nonces.reset(); mu_TEKnonces.reset(); mu_macs.reset(); mu_messages.reset(); }; void print() { mu_nonces.print(); mu_TEKnonces.print(); mu_macs.print(); mu_messages.print(); }; void print_diff(state *prevstate) { mu_nonces.print_diff(prevstate); mu_TEKnonces.print_diff(prevstate); mu_macs.print_diff(prevstate); mu_messages.print_diff(prevstate); }; void to_state(state *thestate) { mu_nonces.to_state(thestate); mu_TEKnonces.to_state(thestate); mu_macs.to_state(thestate); mu_messages.to_state(thestate); }; virtual bool isundefined() { Error.Error("Checking undefinedness of a non-base type"); return TRUE;} virtual bool ismember() { Error.Error("Checking membership for a non-base type"); return TRUE;} mu_1_Intruder& operator= (const mu_1_Intruder& from) { mu_nonces = from.mu_nonces; mu_TEKnonces = from.mu_TEKnonces; mu_macs = from.mu_macs; mu_messages = from.mu_messages; return *this; }; }; void mu_1_Intruder::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1_Intruder::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1_Intruder::set_self(char *n, int os) { name = n; mu_nonces.set_self_2(name, ".nonces", os + 0 ); mu_TEKnonces.set_self_2(name, ".TEKnonces", os + 70 ); mu_macs.set_self_2(name, ".macs", os + 140 ); mu_messages.set_self_2(name, ".messages", os + 370 ); } mu_1_Intruder::~mu_1_Intruder() { } /*** end record declaration ***/ mu_1_Intruder mu_1_Intruder_undefined_var; /*** begin multiset declaration ***/ class mu_1__type_10_id: public mu__byte { public: inline int operator=(int val) { return value(val); }; inline int operator=(const mu_1__type_10_id& val) { return value(val.value()); }; inline operator int() const { return value(); }; mu_1__type_10_id () : mu__byte(0,9,0) {}; mu_1__type_10_id (int val) : mu__byte(0,9,0, "Parameter or function result.",0) {operator=(val); }; char * Name() { return tsprintf("%d", value()); }; }; class mu_1__type_10 { public: mu_1_Message array[ 10 ]; int max_size; int current_size; public: mu_0_boolean valid[ 10 ]; char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_10 (char *n, int os): current_size(0), max_size(0) { set_self(n, os); }; mu_1__type_10 ( void ): current_size(0), max_size(0) {}; virtual ~mu_1__type_10 (); mu_1_Message& operator[] (int index) /* const */ { if ((index >= 0) && (index <= 9) && valid[index].value()) return array[ index ]; else { Error.Error("Internal Error::%d not in index range of %s.", index, name); return array[0]; } }; mu_1__type_10& operator= (const mu_1__type_10& from) { for (int i = 0; i < 10; i++) { array[i] = from.array[i]; valid[i].value(from.valid[i].value()); }; current_size = from.get_current_size(); return *this; } friend int CompareWeight(mu_1__type_10& a, mu_1__type_10& b) { return 0; } friend int Compare(mu_1__type_10& a, mu_1__type_10& b) { int w; for (int i=0; i<10; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); void clear() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void undefine() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void reset() { for (int i = 0; i < 10; i++) { array[i].undefine(); valid[i].value(FALSE); } current_size = 0; }; void to_state(state *thestate) { for (int i = 0; i < 10; i++) { array[i].to_state(thestate); valid[i].to_state(thestate); } }; int get_current_size() const { int tmp = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) tmp++; return tmp; }; void update_size() { current_size = 0; for (int i = 0; i < 10; i++) if (valid[i].value()) current_size++; if (max_size= 10) Error.Error("Maximum size of MultiSet (%s) exceeded.",name); int i; for (i = 0; i < 10; i++) if (!valid[i].value()) { array[i] = element; valid[i].value(TRUE); break; } current_size++; return i; }; void multisetremove(const mu_1__type_10_id &id) { update_size(); if (!valid[(int)id].value()) Error.Error("Internal Error: Illegal Multiset element selected."); valid[(int)id].value(FALSE); array[(int)id].undefine(); current_size--; }; void MultisetSort() { static mu_1_Message temp; // compact int i,j; for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (Compare(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } } }; void mu_1__type_10::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_10::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_10::set_self( char *n, int os) { int i,k; name = n; for(i = 0; i < 10; i++) array[i].set_self(tsprintf("%s{%d}", n,i), i * 51 + os); k = os + i * 51; for(i = 0; i < 10; i++) valid[i].set_self("", i * 2 + k); }; mu_1__type_10::~mu_1__type_10() { } /*** end multiset declaration ***/ mu_1__type_10 mu_1__type_10_undefined_var; class mu_1__type_11 { public: mu_1_MS array[ 1 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_11 (char *n, int os) { set_self(n, os); }; mu_1__type_11 ( void ) {}; virtual ~mu_1__type_11 (); mu_1_MS& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 1 ) && ( index <= 1 ) ) return array[ index - 1 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s: MSId is internally represented from 1 to 1.\nInternal Error in Type checking.",index, name); return array[0]; } #else return array[ index - 1 ]; #endif }; mu_1__type_11& operator= (const mu_1__type_11& from) { array[0] = from.array[0]; return *this; } friend int CompareWeight(mu_1__type_11& a, mu_1__type_11& b) { int w; for (int i=0; i<1; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_11& a, mu_1__type_11& b) { int w; for (int i=0; i<1; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<1; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<1; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 1; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 1; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 1; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 1; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 1; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 1; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_11::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_11::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_11::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"MSId_1", i * 144 + os);i++; } mu_1__type_11::~mu_1__type_11() { } /*** end array declaration ***/ mu_1__type_11 mu_1__type_11_undefined_var; class mu_1__type_12 { public: mu_1_BS array[ 1 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_12 (char *n, int os) { set_self(n, os); }; mu_1__type_12 ( void ) {}; virtual ~mu_1__type_12 (); mu_1_BS& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 2 ) && ( index <= 2 ) ) return array[ index - 2 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s: BSId is internally represented from 2 to 2.\nInternal Error in Type checking.",index, name); return array[0]; } #else return array[ index - 2 ]; #endif }; mu_1__type_12& operator= (const mu_1__type_12& from) { array[0] = from.array[0]; return *this; } friend int CompareWeight(mu_1__type_12& a, mu_1__type_12& b) { int w; for (int i=0; i<1; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_12& a, mu_1__type_12& b) { int w; for (int i=0; i<1; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<1; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<1; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 1; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 1; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 1; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 1; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 1; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 1; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_12::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_12::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_12::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"BSId_1", i * 123 + os);i++; } mu_1__type_12::~mu_1__type_12() { } /*** end array declaration ***/ mu_1__type_12 mu_1__type_12_undefined_var; class mu_1__type_13 { public: mu_1_Intruder array[ 1 ]; public: char *name; char longname[BUFFER_SIZE/4]; void set_self( char *n, int os); void set_self_2( char *n, char *n2, int os); void set_self_ar( char *n, char *n2, int os); mu_1__type_13 (char *n, int os) { set_self(n, os); }; mu_1__type_13 ( void ) {}; virtual ~mu_1__type_13 (); mu_1_Intruder& operator[] (int index) /* const */ { #ifndef NO_RUN_TIME_CHECKING if ( ( index >= 3 ) && ( index <= 3 ) ) return array[ index - 3 ]; else { if (index==UNDEFVAL) Error.Error("Indexing to %s using an undefined value.", name); else Error.Error("Funny index value %d for %s: IntruderId is internally represented from 3 to 3.\nInternal Error in Type checking.",index, name); return array[0]; } #else return array[ index - 3 ]; #endif }; mu_1__type_13& operator= (const mu_1__type_13& from) { array[0] = from.array[0]; return *this; } friend int CompareWeight(mu_1__type_13& a, mu_1__type_13& b) { int w; for (int i=0; i<1; i++) { w = CompareWeight(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } friend int Compare(mu_1__type_13& a, mu_1__type_13& b) { int w; for (int i=0; i<1; i++) { w = Compare(a.array[i], b.array[i]); if (w!=0) return w; } return 0; } virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() { for (int i=0; i<1; i++) array[i].MultisetSort(); } void print_statistic() { for (int i=0; i<1; i++) array[i].print_statistic(); } void clear() { for (int i = 0; i < 1; i++) array[i].clear(); }; void undefine() { for (int i = 0; i < 1; i++) array[i].undefine(); }; void reset() { for (int i = 0; i < 1; i++) array[i].reset(); }; void to_state(state *thestate) { for (int i = 0; i < 1; i++) array[i].to_state(thestate); }; void print() { for (int i = 0; i < 1; i++) array[i].print(); }; void print_diff(state *prevstate) { for (int i = 0; i < 1; i++) array[i].print_diff(prevstate); }; }; void mu_1__type_13::set_self_ar( char *n1, char *n2, int os ) { int l1 = strlen(n1), l2 = strlen(n2); strcpy( longname, n1 ); longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void mu_1__type_13::set_self_2( char *n1, char *n2, int os ) { strcpy( longname, n1 ); strcat( longname, n2 ); set_self( longname, os ); }; void mu_1__type_13::set_self( char *n, int os) { int i=0; name = n; array[i].set_self_ar(n,"IntruderId_1", i * 900 + os);i++; } mu_1__type_13::~mu_1__type_13() { } /*** end array declaration ***/ mu_1__type_13 mu_1__type_13_undefined_var; class mu_1__type_14: public mu__byte { public: inline int operator=(int val) { return mu__byte::operator=(val); }; inline int operator=(const mu_1__type_14& val) { return mu__byte::operator=((int) val); }; mu_1__type_14 (char *name, int os): mu__byte(0, 5, 3, name, os) {}; mu_1__type_14 (void): mu__byte(0, 5, 3) {}; mu_1__type_14 (int val): mu__byte(0, 5, 3, "Parameter or function result.", 0) { operator=(val); }; char * Name() { return tsprintf("%d",value()); }; virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); virtual void MultisetLimit(PermSet& Perm); virtual void MultisetSort() {}; void print_statistic() {}; }; /*** end of subrange decl ***/ mu_1__type_14 mu_1__type_14_undefined_var; const int mu_BS_SEND_M1 = 6; const int mu_MS_RECV_M1 = 5; const int mu_MS_SEND_M2 = 6; const int mu_BS_RECV_M2 = 5; const int mu_BS_SEND_M3 = 8; const int mu_MS_RECV_M3 = 8; const int mu_INT_INTERCEPT = 4; const int mu_INT_COMPOSE = 4; const int mu_INT_SEND = 4; const int mu_MS_WAIT_RES_COST = 11; const int mu_INT_RES_THRESHOLD = 8; const int mu_INT_THRESHOLD = 16; const int mu_MS_DONE_COST = 19; const int mu_BS_DONE_COST = 19; const int mu_DOS_ENABLED = 1; const int mu_PN_ENABLED = 1; const int mu_NumMS = 1; const int mu_NumBS = 1; const int mu_NumIntruders = 1; const int mu_NetworkSize = 10; const int mu_MaxSessions = 1; const int mu_MaxIntruderActions = 5; const int mu_MaxIntruderCosts = 200; const int mu_MaxCost = 200; const int mu_MaxNonce = 30; const int mu_MaxPN = 100; const int mu_MaxKnowledge = 10; const int mu_MSId_1 = 1; const int mu_BSId_1 = 2; const int mu_IntruderId_1 = 3; const int mu_M_1 = 4; const int mu_M_2 = 5; const int mu_M_3 = 6; const int mu_MS_WAIT_CLG = 7; const int mu_MS_WAIT_RES = 8; const int mu_MS_DONE = 9; const int mu_BS_START = 10; const int mu_BS_WAIT_REQ = 11; const int mu_BS_DONE = 12; /*** Variable declaration ***/ mu_1__type_10 mu_net("net",0); /*** Variable declaration ***/ mu_1__type_11 mu_ms("ms",530); /*** Variable declaration ***/ mu_1__type_12 mu_bs("bs",674); /*** Variable declaration ***/ mu_1__type_13 mu_int("int",797); /*** Variable declaration ***/ mu_1__type_14 mu_actionCount("actionCount",1697); /*** Variable declaration ***/ mu_1_Nonce mu_nextNonce("nextNonce",1700); /*** Variable declaration ***/ mu_1_PN mu_nextPN("nextPN",1705); mu_1_Nonce mu_freshNonce() { /*** Variable declaration ***/ mu_1_Nonce mu_tmp("tmp",0); if ( (mu_nextNonce) == (mu_MaxNonce) ) { Error.Error("Error: Run out of nonces!"); } if (mu_nextNonce.isundefined()) mu_tmp.undefine(); else mu_tmp = mu_nextNonce; mu_nextNonce = (mu_nextNonce) + (1); return mu_tmp; Error.Error("The end of function freshNonce reached without returning values."); }; /*** end function declaration ***/ mu_1_PN mu_freshPN() { /*** Variable declaration ***/ mu_1_PN mu_tmp("tmp",0); if ( (mu_nextPN) == (mu_MaxPN) ) { Error.Error("Error: Run out of PNs!"); } if (mu_nextPN.isundefined()) mu_tmp.undefine(); else mu_tmp = mu_nextPN; mu_nextPN = (mu_nextPN) + (1); return mu_tmp; Error.Error("The end of function freshPN reached without returning values."); }; /*** end function declaration ***/ mu_1_AK mu_useAK(const mu_1_AgentId& mu_peer1,const mu_1_AgentId& mu_peer2) { /*** Variable declaration ***/ mu_1_AK mu_tmp("tmp",0); if (mu_peer1.isundefined()) mu_tmp.mu_peer1.undefine(); else mu_tmp.mu_peer1 = mu_peer1; if (mu_peer2.isundefined()) mu_tmp.mu_peer2.undefine(); else mu_tmp.mu_peer2 = mu_peer2; return mu_tmp; Error.Error("The end of function useAK reached without returning values."); }; /*** end function declaration ***/ mu_1_MAC mu_computeMAC(mu_1_Message& mu_msg,mu_1_AK& mu_ak) { /*** Variable declaration ***/ mu_1_MAC mu_tmp("tmp",0); mu_tmp.mu_ak = mu_ak; mu_tmp.mu_BSnonce = mu_msg.mu_BSnonce; bool mu__boolexpr15; if ((mu_msg.mu_mtype) == (mu_M_2)) mu__boolexpr15 = TRUE ; else { mu__boolexpr15 = ((mu_msg.mu_mtype) == (mu_M_3)) ; } if ( mu__boolexpr15 ) { mu_tmp.mu_MSnonce = mu_msg.mu_MSnonce; } if ( (mu_msg.mu_mtype) == (mu_M_3) ) { mu_tmp.mu_TEKnonce = mu_msg.mu_TEKnonce; } mu_tmp.mu_mtype = mu_msg.mu_mtype; return mu_tmp; Error.Error("The end of function computeMAC reached without returning values."); }; /*** end function declaration ***/ mu_0_boolean mu_akEqual(mu_1_AK& mu_key1,mu_1_AK& mu_key2) { bool mu__boolexpr16; bool mu__boolexpr17; if (!((mu_key1.mu_peer1) == (mu_key2.mu_peer1))) mu__boolexpr17 = FALSE ; else { mu__boolexpr17 = ((mu_key1.mu_peer2) == (mu_key2.mu_peer2)) ; } if (mu__boolexpr17) mu__boolexpr16 = TRUE ; else { bool mu__boolexpr18; if (!((mu_key1.mu_peer2) == (mu_key2.mu_peer1))) mu__boolexpr18 = FALSE ; else { mu__boolexpr18 = ((mu_key1.mu_peer1) == (mu_key2.mu_peer2)) ; } mu__boolexpr16 = (mu__boolexpr18) ; } return mu__boolexpr16; Error.Error("The end of function akEqual reached without returning values."); }; /*** end function declaration ***/ mu_0_boolean mu_macEqual(mu_1_MAC& mu_mac1,mu_1_MAC& mu_mac2) { if ( !(mu_akEqual( mu_mac1.mu_ak, mu_mac2.mu_ak )) ) { return mu_false; } if ( !((mu_mac1.mu_mtype) == (mu_mac2.mu_mtype)) ) { return mu_false; } if ( !((mu_mac1.mu_BSnonce) == (mu_mac2.mu_BSnonce)) ) { return mu_false; } bool mu__boolexpr19; bool mu__boolexpr20; if ((mu_mac1.mu_mtype) == (mu_M_2)) mu__boolexpr20 = TRUE ; else { mu__boolexpr20 = ((mu_mac1.mu_mtype) == (mu_M_3)) ; } if (!(mu__boolexpr20)) mu__boolexpr19 = FALSE ; else { mu__boolexpr19 = (!((mu_mac1.mu_MSnonce) == (mu_mac2.mu_MSnonce))) ; } if ( mu__boolexpr19 ) { return mu_false; } bool mu__boolexpr21; if (!((mu_mac1.mu_mtype) == (mu_M_3))) mu__boolexpr21 = FALSE ; else { mu__boolexpr21 = (!((mu_mac1.mu_TEKnonce) == (mu_mac2.mu_TEKnonce))) ; } if ( mu__boolexpr21 ) { return mu_false; } return mu_true; Error.Error("The end of function macEqual reached without returning values."); }; /*** end function declaration ***/ /******************** The world ********************/ void world_class::clear() { mu_net.clear(); mu_ms.clear(); mu_bs.clear(); mu_int.clear(); mu_actionCount.clear(); mu_nextNonce.clear(); mu_nextPN.clear(); } void world_class::undefine() { mu_net.undefine(); mu_ms.undefine(); mu_bs.undefine(); mu_int.undefine(); mu_actionCount.undefine(); mu_nextNonce.undefine(); mu_nextPN.undefine(); } void world_class::reset() { mu_net.reset(); mu_ms.reset(); mu_bs.reset(); mu_int.reset(); mu_actionCount.reset(); mu_nextNonce.reset(); mu_nextPN.reset(); } void world_class::print() { static int num_calls = 0; /* to ward off recursive calls. */ if ( num_calls == 0 ) { num_calls++; mu_net.print(); mu_ms.print(); mu_bs.print(); mu_int.print(); mu_actionCount.print(); mu_nextNonce.print(); mu_nextPN.print(); num_calls--; } } void world_class::print_statistic() { static int num_calls = 0; /* to ward off recursive calls. */ if ( num_calls == 0 ) { num_calls++; mu_net.print_statistic(); mu_ms.print_statistic(); mu_bs.print_statistic(); mu_int.print_statistic(); mu_actionCount.print_statistic(); mu_nextNonce.print_statistic(); mu_nextPN.print_statistic(); num_calls--; } } void world_class::print_diff( state *prevstate ) { if ( prevstate != NULL ) { mu_net.print_diff(prevstate); mu_ms.print_diff(prevstate); mu_bs.print_diff(prevstate); mu_int.print_diff(prevstate); mu_actionCount.print_diff(prevstate); mu_nextNonce.print_diff(prevstate); mu_nextPN.print_diff(prevstate); } else print(); } void world_class::to_state(state *newstate) { mu_net.to_state( newstate ); mu_ms.to_state( newstate ); mu_bs.to_state( newstate ); mu_int.to_state( newstate ); mu_actionCount.to_state( newstate ); mu_nextNonce.to_state( newstate ); mu_nextPN.to_state( newstate ); } void world_class::setstate(state *thestate) { } /******************** Rule declarations ********************/ /******************** RuleBase0 ********************/ class RuleBase0 { public: int Priority() { return 30; } char * Name(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_MSId mu_j; mu_j.value((r % 1) + 1); r = r / 1; static mu_1_BSId mu_k; mu_k.value((r % 1) + 2); r = r / 1; static mu_1__type_6_id mu_n; mu_n.value((r % 10) + 0); r = r / 10; static mu_1__type_8_id mu_m; mu_m.value((r % 10) + 0); r = r / 10; return tsprintf("Intruders compose message 1 and send to agents, i:%s, j:%s, k:%s, n:%s, m:%s", mu_i.Name(), mu_j.Name(), mu_k.Name(), mu_n.Name(), mu_m.Name()); } bool Condition(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_MSId mu_j; mu_j.value((r % 1) + 1); r = r / 1; static mu_1_BSId mu_k; mu_k.value((r % 1) + 2); r = r / 1; static mu_1__type_6_id mu_n; mu_n.value((r % 10) + 0); r = r / 10; static mu_1__type_8_id mu_m; mu_m.value((r % 10) + 0); r = r / 10; if (!mu_int[mu_i].mu_nonces.in(mu_n)) { return FALSE; } if (!mu_int[mu_i].mu_macs.in(mu_m)) { return FALSE; } bool mu__boolexpr22; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr22 = FALSE ; else { /*** begin multisetcount 8 declaration ***/ int mu__intexpr23 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr23++; } if (mu_l == 10-1) break; } } /*** end multisetcount 8 declaration ***/ mu__boolexpr22 = ((mu__intexpr23) < (mu_NetworkSize)) ; } return mu__boolexpr22; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 0; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_MSId mu_j; mu_j.value((r % 1) + 1); r = r / 1; static mu_1_BSId mu_k; mu_k.value((r % 1) + 2); r = r / 1; static mu_1__type_6_id mu_n; mu_n.value((r % 10) + 0); r = r / 10; static mu_1__type_8_id mu_m; mu_m.value((r % 10) + 0); r = r / 10; while (what_rule < 100 && mu_n.value()<10 && mu_m.value()<10 ) { if ( ( TRUE ) ) { bool mu__boolexpr24; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr24 = FALSE ; else { /*** begin multisetcount 8 declaration ***/ int mu__intexpr25 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr25++; } if (mu_l == 10-1) break; } } /*** end multisetcount 8 declaration ***/ mu__boolexpr24 = ((mu__intexpr25) < (mu_NetworkSize)) ; } if (mu__boolexpr24) { if ( ( TRUE && mu_int[mu_i].mu_macs.in(mu_m)&& mu_int[mu_i].mu_nonces.in(mu_n) ) ) return; else what_rule++; } else what_rule += 100; } else what_rule += 100; r = what_rule - 0; mu_i.value((r % 1) + 3); r = r / 1; mu_j.value((r % 1) + 1); r = r / 1; mu_k.value((r % 1) + 2); r = r / 1; mu_n.value((r % 10) + 0); r = r / 10; mu_m.value((r % 10) + 0); r = r / 10; } } void Code(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1_MSId mu_j; mu_j.value((r % 1) + 1); r = r / 1; static mu_1_BSId mu_k; mu_k.value((r % 1) + 2); r = r / 1; static mu_1__type_6_id mu_n; mu_n.value((r % 10) + 0); r = r / 10; static mu_1__type_8_id mu_m; mu_m.value((r % 10) + 0); r = r / 10; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_j; mu_outM.mu_mtype = mu_M_1; mu_outM.mu_BSnonce = mu_int[mu_i].mu_nonces[mu_n]; mu_outM.mu_address = mu_k; mu_outM.mu_mac = mu_int[mu_i].mu_macs[mu_m]; mu_outM.mu_pn = -1; mu_net.multisetadd(mu_outM); mu_actionCount = (mu_actionCount) + (1); mu_ms[mu_j].mu_associations[mu_k].mu_session.mu_intCosts = ((mu_ms[mu_j].mu_associations[mu_k].mu_session.mu_intCosts) + (mu_INT_INTERCEPT)) + (mu_INT_COMPOSE); }; bool UnFair() { return FALSE; } }; /******************** RuleBase1 ********************/ class RuleBase1 { public: int Priority() { return 30; } char * Name(unsigned r) { static mu_1__type_9_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 3); r = r / 3; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; return tsprintf("Messages Replayed to every agent, j:%s, k:%s, i:%s", mu_j.Name(), mu_k.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_9_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 3); r = r / 3; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; if (!mu_int[mu_i].mu_messages.in(mu_j)) { return FALSE; } bool mu__boolexpr26; bool mu__boolexpr27; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr27 = FALSE ; else { mu__boolexpr27 = ((mu_i) != (mu_k)) ; } if (!(mu__boolexpr27)) mu__boolexpr26 = FALSE ; else { /*** begin multisetcount 7 declaration ***/ int mu__intexpr28 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr28++; } if (mu_l == 10-1) break; } } /*** end multisetcount 7 declaration ***/ mu__boolexpr26 = ((mu__intexpr28) < (mu_NetworkSize)) ; } return mu__boolexpr26; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 100; static mu_1__type_9_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 3); r = r / 3; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; while (what_rule < 130 && mu_j.value()<10 ) { if ( ( TRUE ) ) { bool mu__boolexpr29; bool mu__boolexpr30; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr30 = FALSE ; else { mu__boolexpr30 = ((mu_i) != (mu_k)) ; } if (!(mu__boolexpr30)) mu__boolexpr29 = FALSE ; else { /*** begin multisetcount 7 declaration ***/ int mu__intexpr31 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr31++; } if (mu_l == 10-1) break; } } /*** end multisetcount 7 declaration ***/ mu__boolexpr29 = ((mu__intexpr31) < (mu_NetworkSize)) ; } if (mu__boolexpr29) { if ( ( TRUE && mu_int[mu_i].mu_messages.in(mu_j) ) ) return; else what_rule++; } else what_rule += 10; } else what_rule += 10; r = what_rule - 100; mu_j.value((r % 10) + 0); r = r / 10; mu_k.unionassign(r % 3); r = r / 3; mu_i.value((r % 1) + 3); r = r / 1; } } void Code(unsigned r) { static mu_1__type_9_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_AgentId mu_k; mu_k.unionassign(r % 3); r = r / 3; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); mu_outM.undefine(); mu_outM = mu_int[mu_i].mu_messages[mu_j]; mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_k; mu_net.multisetadd(mu_outM); mu_actionCount = (mu_actionCount) + (1); bool mu__boolexpr32; if (!((mu_k>=1 && mu_k<=1))) mu__boolexpr32 = FALSE ; else { mu__boolexpr32 = ((mu_outM.mu_address>=2 && mu_outM.mu_address<=2)) ; } if ( mu__boolexpr32 ) { mu_ms[mu_k].mu_associations[mu_outM.mu_address].mu_session.mu_intCosts = ((mu_ms[mu_k].mu_associations[mu_outM.mu_address].mu_session.mu_intCosts) + (mu_INT_INTERCEPT)) + (mu_INT_SEND); } }; bool UnFair() { return FALSE; } }; /******************** RuleBase2 ********************/ class RuleBase2 { public: int Priority() { return 10; } char * Name(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; return tsprintf("Intruders intercept a message, i:%s, j:%s", mu_i.Name(), mu_j.Name()); } bool Condition(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; if (!mu_net.in(mu_j)) { return FALSE; } bool mu__boolexpr33; bool mu__boolexpr34; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr34 = FALSE ; else { /*** begin multisetcount 1 declaration ***/ int mu__intexpr35 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr35++; } if (mu_l == 10-1) break; } } /*** end multisetcount 1 declaration ***/ mu__boolexpr34 = ((mu__intexpr35) > (0)) ; } if (!(mu__boolexpr34)) mu__boolexpr33 = FALSE ; else { mu__boolexpr33 = (!((mu_net[mu_j].mu_source>=3 && mu_net[mu_j].mu_source<=3))) ; } return mu__boolexpr33; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 130; static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; while (what_rule < 140 && mu_j.value()<10 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { bool mu__boolexpr36; bool mu__boolexpr37; if (!((mu_actionCount) < (mu_MaxIntruderActions))) mu__boolexpr37 = FALSE ; else { /*** begin multisetcount 1 declaration ***/ int mu__intexpr38 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr38++; } if (mu_l == 10-1) break; } } /*** end multisetcount 1 declaration ***/ mu__boolexpr37 = ((mu__intexpr38) > (0)) ; } if (!(mu__boolexpr37)) mu__boolexpr36 = FALSE ; else { mu__boolexpr36 = (!((mu_net[mu_j].mu_source>=3 && mu_net[mu_j].mu_source<=3))) ; } if (mu__boolexpr36) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 130; mu_i.value((r % 1) + 3); r = r / 1; mu_j.value((r % 10) + 0); r = r / 10; } } void Code(unsigned r) { static mu_1_IntruderId mu_i; mu_i.value((r % 1) + 3); r = r / 1; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; /*** Variable declaration ***/ mu_1_Message mu_inM("inM",0); { mu_1__type_9& mu_msg = mu_int[mu_i].mu_messages; mu_1__type_6& mu_nc = mu_int[mu_i].mu_nonces; mu_1__type_7& mu_teknc = mu_int[mu_i].mu_TEKnonces; mu_1__type_8& mu_mc = mu_int[mu_i].mu_macs; mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); /*** begin multisetcount 2 declaration ***/ int mu__intexpr39 = 0; { mu_1__type_9_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_msg.valid[(int)mu_l].value()) { bool mu__boolexpr40; bool mu__boolexpr41; bool mu__boolexpr42; bool mu__boolexpr43; bool mu__boolexpr44; if (!((mu_msg[mu_l].mu_mtype) == (mu_inM.mu_mtype))) mu__boolexpr44 = FALSE ; else { mu__boolexpr44 = ((mu_msg[mu_l].mu_BSnonce) == (mu_inM.mu_BSnonce)) ; } if (!(mu__boolexpr44)) mu__boolexpr43 = FALSE ; else { bool mu__boolexpr45; if ((mu_msg[mu_l].mu_mtype) == (mu_M_1)) mu__boolexpr45 = TRUE ; else { mu__boolexpr45 = ((mu_msg[mu_l].mu_MSnonce) == (mu_inM.mu_MSnonce)) ; } mu__boolexpr43 = (mu__boolexpr45) ; } if (!(mu__boolexpr43)) mu__boolexpr42 = FALSE ; else { bool mu__boolexpr46; bool mu__boolexpr47; if ((mu_msg[mu_l].mu_mtype) == (mu_M_1)) mu__boolexpr47 = TRUE ; else { mu__boolexpr47 = ((mu_msg[mu_l].mu_mtype) == (mu_M_2)) ; } if (mu__boolexpr47) mu__boolexpr46 = TRUE ; else { mu__boolexpr46 = ((mu_msg[mu_l].mu_TEKnonce) == (mu_inM.mu_TEKnonce)) ; } mu__boolexpr42 = (mu__boolexpr46) ; } if (!(mu__boolexpr42)) mu__boolexpr41 = FALSE ; else { mu__boolexpr41 = ((mu_msg[mu_l].mu_address) == (mu_inM.mu_address)) ; } if (!(mu__boolexpr41)) mu__boolexpr40 = FALSE ; else { mu__boolexpr40 = (mu_macEqual( mu_msg[mu_l].mu_mac, mu_inM.mu_mac )) ; } if ( mu__boolexpr40 ) mu__intexpr39++; } if (mu_l == 10-1) break; } } /*** end multisetcount 2 declaration ***/ if ( (mu__intexpr39) == (0) ) { mu_inM.mu_source.undefine(); mu_inM.mu_dest.undefine(); mu_int[mu_i].mu_messages.multisetadd(mu_inM); } /*** begin multisetcount 3 declaration ***/ int mu__intexpr48 = 0; { mu_1__type_6_id mu_n; for (mu_n = 0; ; mu_n=mu_n+1) { if (mu_nc.valid[(int)mu_n].value()) { if ( (mu_nc[mu_n]) == (mu_inM.mu_BSnonce) ) mu__intexpr48++; } if (mu_n == 10-1) break; } } /*** end multisetcount 3 declaration ***/ if ( (mu__intexpr48) == (0) ) { mu_int[mu_i].mu_nonces.multisetadd(mu_inM.mu_BSnonce); } /*** begin multisetcount 4 declaration ***/ int mu__intexpr49 = 0; { mu_1__type_6_id mu_n; for (mu_n = 0; ; mu_n=mu_n+1) { if (mu_nc.valid[(int)mu_n].value()) { bool mu__boolexpr50; if ((mu_inM.mu_mtype) == (mu_M_1)) mu__boolexpr50 = TRUE ; else { mu__boolexpr50 = ((mu_nc[mu_n]) == (mu_inM.mu_MSnonce)) ; } if ( mu__boolexpr50 ) mu__intexpr49++; } if (mu_n == 10-1) break; } } /*** end multisetcount 4 declaration ***/ if ( (mu__intexpr49) == (0) ) { mu_int[mu_i].mu_nonces.multisetadd(mu_inM.mu_MSnonce); } /*** begin multisetcount 5 declaration ***/ int mu__intexpr51 = 0; { mu_1__type_7_id mu_n; for (mu_n = 0; ; mu_n=mu_n+1) { if (mu_teknc.valid[(int)mu_n].value()) { bool mu__boolexpr52; bool mu__boolexpr53; if ((mu_inM.mu_mtype) == (mu_M_1)) mu__boolexpr53 = TRUE ; else { mu__boolexpr53 = ((mu_inM.mu_mtype) == (mu_M_2)) ; } if (mu__boolexpr53) mu__boolexpr52 = TRUE ; else { mu__boolexpr52 = ((mu_teknc[mu_n]) == (mu_inM.mu_TEKnonce)) ; } if ( mu__boolexpr52 ) mu__intexpr51++; } if (mu_n == 10-1) break; } } /*** end multisetcount 5 declaration ***/ if ( (mu__intexpr51) == (0) ) { if ( (mu_inM.mu_mtype) == (mu_M_3) ) { mu_int[mu_i].mu_TEKnonces.multisetadd(mu_inM.mu_TEKnonce); } } /*** begin multisetcount 6 declaration ***/ int mu__intexpr54 = 0; { mu_1__type_8_id mu_m; for (mu_m = 0; ; mu_m=mu_m+1) { if (mu_mc.valid[(int)mu_m].value()) { if ( mu_macEqual( mu_mc[mu_m], mu_inM.mu_mac ) ) mu__intexpr54++; } if (mu_m == 10-1) break; } } /*** end multisetcount 6 declaration ***/ if ( (mu__intexpr54) == (0) ) { mu_int[mu_i].mu_macs.multisetadd(mu_inM.mu_mac); } mu_actionCount = (mu_actionCount) + (1); } }; bool UnFair() { return FALSE; } }; /******************** RuleBase3 ********************/ class RuleBase3 { public: int Priority() { return 291; } char * Name(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; return tsprintf("MS transitions from MS_DONE->MS_WAIT_CLG, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; return (mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_MS_DONE); } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 140; static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; while (what_rule < 143 ) { if ( ( TRUE ) ) { if ((mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_MS_DONE)) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 140; mu_j.unionassign(r % 3); r = r / 3; mu_i.value((r % 1) + 1); r = r / 1; } } void Code(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_state = mu_MS_WAIT_CLG; if ( !(mu_DOS_ENABLED) ) { mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_costs = 0; mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_intCosts = 0; } }; bool UnFair() { return FALSE; } }; /******************** RuleBase4 ********************/ class RuleBase4 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; return tsprintf("MS processes message 3, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } bool mu__boolexpr55; bool mu__boolexpr56; bool mu__boolexpr57; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr57 = FALSE ; else { mu__boolexpr57 = ((mu_net[mu_j].mu_mtype) == (mu_M_3)) ; } if (!(mu__boolexpr57)) mu__boolexpr56 = FALSE ; else { mu__boolexpr56 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr56)) mu__boolexpr55 = FALSE ; else { mu__boolexpr55 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_MS_WAIT_RES)) ; } return mu__boolexpr55; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 143; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; while (what_rule < 153 && mu_j.value()<10 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { bool mu__boolexpr58; bool mu__boolexpr59; bool mu__boolexpr60; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr60 = FALSE ; else { mu__boolexpr60 = ((mu_net[mu_j].mu_mtype) == (mu_M_3)) ; } if (!(mu__boolexpr60)) mu__boolexpr59 = FALSE ; else { mu__boolexpr59 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr59)) mu__boolexpr58 = FALSE ; else { mu__boolexpr58 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_MS_WAIT_RES)) ; } if (mu__boolexpr58) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 143; mu_j.value((r % 10) + 0); r = r / 10; mu_i.value((r % 1) + 1); r = r / 1; } } void Code(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_inM("inM",0); /*** Variable declaration ***/ mu_1_MAC mu_mac("mac",51); /*** Variable declaration ***/ mu_1_AK mu_outAK("outAK",72); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_outAK = mu_useAK( (int)mu_i, mu_inM.mu_address ); mu_mac = mu_computeMAC( mu_inM, mu_outAK ); if ( mu_macEqual( mu_mac, mu_inM.mu_mac ) ) { mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_peer = mu_inM.mu_source; mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_TEKnonce = mu_inM.mu_TEKnonce; mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_state = mu_MS_DONE; mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs = (mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs) + (mu_MS_RECV_M3); } }; bool UnFair() { return FALSE; } }; /******************** RuleBase5 ********************/ class RuleBase5 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; return tsprintf("BS processes message 2, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } bool mu__boolexpr61; bool mu__boolexpr62; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr62 = FALSE ; else { mu__boolexpr62 = ((mu_net[mu_j].mu_mtype) == (mu_M_2)) ; } if (!(mu__boolexpr62)) mu__boolexpr61 = FALSE ; else { bool mu__boolexpr63; if (mu_DOS_ENABLED) mu__boolexpr63 = TRUE ; else { mu__boolexpr63 = ((mu_bs[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_BS_WAIT_REQ)) ; } mu__boolexpr61 = (mu__boolexpr63) ; } return mu__boolexpr61; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 153; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; while (what_rule < 163 && mu_j.value()<10 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { bool mu__boolexpr64; bool mu__boolexpr65; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr65 = FALSE ; else { mu__boolexpr65 = ((mu_net[mu_j].mu_mtype) == (mu_M_2)) ; } if (!(mu__boolexpr65)) mu__boolexpr64 = FALSE ; else { bool mu__boolexpr66; if (mu_DOS_ENABLED) mu__boolexpr66 = TRUE ; else { mu__boolexpr66 = ((mu_bs[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_BS_WAIT_REQ)) ; } mu__boolexpr64 = (mu__boolexpr66) ; } if (mu__boolexpr64) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 153; mu_j.value((r % 10) + 0); r = r / 10; mu_i.value((r % 1) + 2); r = r / 1; } } void Code(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Message mu_inM("inM",51); /*** Variable declaration ***/ mu_1_MAC mu_mac("mac",102); /*** Variable declaration ***/ mu_1_AK mu_outAK("outAK",123); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_outAK = mu_useAK( (int)mu_i, mu_inM.mu_address ); mu_mac = mu_computeMAC( mu_inM, mu_outAK ); if ( mu_macEqual( mu_mac, mu_inM.mu_mac ) ) { mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_inM.mu_address; mu_outM.mu_mtype = mu_M_3; mu_outM.mu_BSnonce = mu_inM.mu_BSnonce; mu_outM.mu_MSnonce = mu_inM.mu_MSnonce; mu_outM.mu_TEKnonce = mu_freshNonce( ); mu_outM.mu_address = mu_i; mu_outM.mu_mac = mu_computeMAC( mu_outM, mu_outAK ); mu_net.multisetadd(mu_outM); mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_peer = mu_inM.mu_source; mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_MSnonce = mu_inM.mu_MSnonce; mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_TEKnonce = mu_outM.mu_TEKnonce; mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_state = mu_BS_DONE; if ( !(mu_DOS_ENABLED) ) { mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs = ((mu_bs[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs) + (mu_BS_RECV_M2)) + (mu_BS_SEND_M3); } } }; bool UnFair() { return FALSE; } }; /******************** RuleBase6 ********************/ class RuleBase6 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; return tsprintf("MS processes message 1, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; if (!mu_net.in(mu_j)) { return FALSE; } bool mu__boolexpr67; bool mu__boolexpr68; bool mu__boolexpr69; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr69 = FALSE ; else { mu__boolexpr69 = ((mu_net[mu_j].mu_mtype) == (mu_M_1)) ; } if (!(mu__boolexpr69)) mu__boolexpr68 = FALSE ; else { mu__boolexpr68 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr68)) mu__boolexpr67 = FALSE ; else { mu__boolexpr67 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_MS_WAIT_CLG)) ; } return mu__boolexpr67; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 163; static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; while (what_rule < 173 && mu_j.value()<10 ) { if ( ( TRUE && mu_net.in(mu_j) ) ) { bool mu__boolexpr70; bool mu__boolexpr71; bool mu__boolexpr72; if (!((mu_net[mu_j].mu_dest) == (mu_i))) mu__boolexpr72 = FALSE ; else { mu__boolexpr72 = ((mu_net[mu_j].mu_mtype) == (mu_M_1)) ; } if (!(mu__boolexpr72)) mu__boolexpr71 = FALSE ; else { mu__boolexpr71 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr71)) mu__boolexpr70 = FALSE ; else { mu__boolexpr70 = ((mu_ms[mu_i].mu_associations[mu_net[mu_j].mu_address].mu_session.mu_state) == (mu_MS_WAIT_CLG)) ; } if (mu__boolexpr70) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 163; mu_j.value((r % 10) + 0); r = r / 10; mu_i.value((r % 1) + 1); r = r / 1; } } void Code(unsigned r) { static mu_1__type_10_id mu_j; mu_j.value((r % 10) + 0); r = r / 10; static mu_1_MSId mu_i; mu_i.value((r % 1) + 1); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_Message mu_inM("inM",51); /*** Variable declaration ***/ mu_1_MAC mu_mac("mac",102); /*** Variable declaration ***/ mu_1_AK mu_outAK("outAK",123); mu_inM = mu_net[mu_j]; mu_net.multisetremove(mu_j); mu_outAK = mu_useAK( (int)mu_i, mu_inM.mu_address ); mu_mac = mu_computeMAC( mu_inM, mu_outAK ); bool mu__boolexpr73; if (!(mu_macEqual( mu_mac, mu_inM.mu_mac ))) mu__boolexpr73 = FALSE ; else { bool mu__boolexpr74; if (!(mu_PN_ENABLED)) mu__boolexpr74 = TRUE ; else { mu__boolexpr74 = ((mu_inM.mu_pn) > (mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_lastKnownPN)) ; } mu__boolexpr73 = (mu__boolexpr74) ; } if ( mu__boolexpr73 ) { mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_peer = mu_inM.mu_source; mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_ak = mu_useAK( (int)mu_i, mu_inM.mu_address ); mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_BSnonce = mu_inM.mu_BSnonce; mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_MSnonce = mu_freshNonce( ); mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_inM.mu_address; mu_outM.mu_mtype = mu_M_2; mu_outM.mu_BSnonce = mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_BSnonce; mu_outM.mu_MSnonce = mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_MSnonce; mu_outM.mu_address = mu_i; mu_outM.mu_mac = mu_computeMAC( mu_outM, mu_outAK ); mu_net.multisetadd(mu_outM); mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_state = mu_MS_WAIT_RES; if ( !(mu_DOS_ENABLED) ) { mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_sid = (mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_sid) + (1); } mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs = ((mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_session.mu_costs) + (mu_MS_RECV_M1)) + (mu_MS_SEND_M2); if ( !(mu_PN_ENABLED) ) { mu_ms[mu_i].mu_associations[mu_inM.mu_address].mu_lastKnownPN = mu_inM.mu_pn; } } }; bool UnFair() { return FALSE; } }; /******************** RuleBase7 ********************/ class RuleBase7 { public: int Priority() { return 20; } char * Name(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; return tsprintf("BS sends Message 1 to associated agents, j:%s, i:%s", mu_j.Name(), mu_i.Name()); } bool Condition(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; bool mu__boolexpr75; bool mu__boolexpr76; bool mu__boolexpr77; bool mu__boolexpr78; if (!(!((mu_j>=2 && mu_j<=2)))) mu__boolexpr78 = FALSE ; else { mu__boolexpr78 = (!((mu_j>=3 && mu_j<=3))) ; } if (!(mu__boolexpr78)) mu__boolexpr77 = FALSE ; else { mu__boolexpr77 = ((mu_bs[mu_i].mu_associations[mu_j].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr77)) mu__boolexpr76 = FALSE ; else { /*** begin multisetcount 0 declaration ***/ int mu__intexpr79 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr79++; } if (mu_l == 10-1) break; } } /*** end multisetcount 0 declaration ***/ mu__boolexpr76 = ((mu__intexpr79) < (mu_NetworkSize)) ; } if (!(mu__boolexpr76)) mu__boolexpr75 = FALSE ; else { bool mu__boolexpr80; if ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_START)) mu__boolexpr80 = TRUE ; else { mu__boolexpr80 = ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_DONE)) ; } mu__boolexpr75 = (mu__boolexpr80) ; } return mu__boolexpr75; } void NextRule(unsigned & what_rule) { unsigned r = what_rule - 173; static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; while (what_rule < 176 ) { if ( ( TRUE ) ) { bool mu__boolexpr81; bool mu__boolexpr82; bool mu__boolexpr83; bool mu__boolexpr84; if (!(!((mu_j>=2 && mu_j<=2)))) mu__boolexpr84 = FALSE ; else { mu__boolexpr84 = (!((mu_j>=3 && mu_j<=3))) ; } if (!(mu__boolexpr84)) mu__boolexpr83 = FALSE ; else { mu__boolexpr83 = ((mu_bs[mu_i].mu_associations[mu_j].mu_sid) < (mu_MaxSessions)) ; } if (!(mu__boolexpr83)) mu__boolexpr82 = FALSE ; else { /*** begin multisetcount 0 declaration ***/ int mu__intexpr85 = 0; { mu_1__type_10_id mu_l; for (mu_l = 0; ; mu_l=mu_l+1) { if (mu_net.valid[(int)mu_l].value()) { if ( mu_true ) mu__intexpr85++; } if (mu_l == 10-1) break; } } /*** end multisetcount 0 declaration ***/ mu__boolexpr82 = ((mu__intexpr85) < (mu_NetworkSize)) ; } if (!(mu__boolexpr82)) mu__boolexpr81 = FALSE ; else { bool mu__boolexpr86; if ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_START)) mu__boolexpr86 = TRUE ; else { mu__boolexpr86 = ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_DONE)) ; } mu__boolexpr81 = (mu__boolexpr86) ; } if (mu__boolexpr81) { if ( ( TRUE ) ) return; else what_rule++; } else what_rule += 1; } else what_rule += 1; r = what_rule - 173; mu_j.unionassign(r % 3); r = r / 3; mu_i.value((r % 1) + 2); r = r / 1; } } void Code(unsigned r) { static mu_1_AgentId mu_j; mu_j.unionassign(r % 3); r = r / 3; static mu_1_BSId mu_i; mu_i.value((r % 1) + 2); r = r / 1; /*** Variable declaration ***/ mu_1_Message mu_outM("outM",0); /*** Variable declaration ***/ mu_1_AK mu_outAK("outAK",51); mu_outM.undefine(); mu_outM.mu_source = mu_i; mu_outM.mu_dest = mu_j; mu_outM.mu_mtype = mu_M_1; mu_outM.mu_BSnonce = mu_freshNonce( ); mu_outM.mu_address = mu_i; mu_outM.mu_pn = mu_freshPN( ); mu_outAK = mu_useAK( (int)mu_i, mu_j ); mu_outM.mu_mac = mu_computeMAC( mu_outM, mu_outAK ); mu_net.multisetadd(mu_outM); mu_bs[mu_i].mu_associations[mu_j].mu_peer = mu_j; mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_ak = mu_useAK( (int)mu_i, mu_j ); mu_bs[mu_i].mu_associations[mu_j].mu_BSnonce = mu_outM.mu_BSnonce; mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state = mu_BS_WAIT_REQ; mu_bs[mu_i].mu_associations[mu_j].mu_sid = (mu_bs[mu_i].mu_associations[mu_j].mu_sid) + (1); mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_costs = mu_BS_SEND_M1; }; bool UnFair() { return FALSE; } }; class NextStateGenerator { RuleBase0 R0; RuleBase1 R1; RuleBase2 R2; RuleBase3 R3; RuleBase4 R4; RuleBase5 R5; RuleBase6 R6; RuleBase7 R7; public: void SetNextEnabledRule(unsigned & what_rule) { category = CONDITION; if (what_rule<100) { R0.NextRule(what_rule); if (what_rule<100) return; } if (what_rule>=100 && what_rule<130) { R1.NextRule(what_rule); if (what_rule<130) return; } if (what_rule>=130 && what_rule<140) { R2.NextRule(what_rule); if (what_rule<140) return; } if (what_rule>=140 && what_rule<143) { R3.NextRule(what_rule); if (what_rule<143) return; } if (what_rule>=143 && what_rule<153) { R4.NextRule(what_rule); if (what_rule<153) return; } if (what_rule>=153 && what_rule<163) { R5.NextRule(what_rule); if (what_rule<163) return; } if (what_rule>=163 && what_rule<173) { R6.NextRule(what_rule); if (what_rule<173) return; } if (what_rule>=173 && what_rule<176) { R7.NextRule(what_rule); if (what_rule<176) return; } } bool Condition(unsigned r) { category = CONDITION; if (r<=99) return R0.Condition(r-0); if (r>=100 && r<=129) return R1.Condition(r-100); if (r>=130 && r<=139) return R2.Condition(r-130); if (r>=140 && r<=142) return R3.Condition(r-140); if (r>=143 && r<=152) return R4.Condition(r-143); if (r>=153 && r<=162) return R5.Condition(r-153); if (r>=163 && r<=172) return R6.Condition(r-163); if (r>=173 && r<=175) return R7.Condition(r-173); Error.Notrace("Internal: NextStateGenerator -- checking condition for nonexisting rule."); } void Code(unsigned r) { if (r<=99) { R0.Code(r-0); return; } if (r>=100 && r<=129) { R1.Code(r-100); return; } if (r>=130 && r<=139) { R2.Code(r-130); return; } if (r>=140 && r<=142) { R3.Code(r-140); return; } if (r>=143 && r<=152) { R4.Code(r-143); return; } if (r>=153 && r<=162) { R5.Code(r-153); return; } if (r>=163 && r<=172) { R6.Code(r-163); return; } if (r>=173 && r<=175) { R7.Code(r-173); return; } } int Priority(unsigned short r) { if (r<=99) { return R0.Priority(); } if (r>=100 && r<=129) { return R1.Priority(); } if (r>=130 && r<=139) { return R2.Priority(); } if (r>=140 && r<=142) { return R3.Priority(); } if (r>=143 && r<=152) { return R4.Priority(); } if (r>=153 && r<=162) { return R5.Priority(); } if (r>=163 && r<=172) { return R6.Priority(); } if (r>=173 && r<=175) { return R7.Priority(); } } char * Name(unsigned r) { if (r<=99) return R0.Name(r-0); if (r>=100 && r<=129) return R1.Name(r-100); if (r>=130 && r<=139) return R2.Name(r-130); if (r>=140 && r<=142) return R3.Name(r-140); if (r>=143 && r<=152) return R4.Name(r-143); if (r>=153 && r<=162) return R5.Name(r-153); if (r>=163 && r<=172) return R6.Name(r-163); if (r>=173 && r<=175) return R7.Name(r-173); return NULL; } }; const unsigned numrules = 176; /******************** parameter ********************/ #define RULES_IN_WORLD 176 /******************** Startstate records ********************/ /******************** StartStateBase0 ********************/ class StartStateBase0 { public: char * Name(unsigned short r) { return tsprintf("Startstate 0"); } void Code(unsigned short r) { mu_nextNonce = 0; mu_nextPN = 0; mu_actionCount = 0; mu_net.undefine(); mu_ms.undefine(); { for(int mu_i = 1; mu_i <= 1; mu_i++) { { for(int mu_j = 1; mu_j <= 3; mu_j++) if (( ( mu_j >= 3 ) && ( mu_j <= 3 ) )|| ( ( mu_j >= 2 ) && ( mu_j <= 2 ) )|| ( ( mu_j >= 1 ) && ( mu_j <= 1 ) )) { mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_state = mu_MS_WAIT_CLG; mu_ms[mu_i].mu_associations[mu_j].mu_sid = 0; mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_ak = mu_useAK( (int)mu_i, mu_j ); mu_ms[mu_i].mu_associations[mu_j].mu_peer = mu_j; mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_costs = 0; mu_ms[mu_i].mu_associations[mu_j].mu_session.mu_intCosts = 0; mu_ms[mu_i].mu_associations[mu_j].mu_lastKnownPN = 0; }; }; }; }; mu_bs.undefine(); { for(int mu_i = 2; mu_i <= 2; mu_i++) { { for(int mu_j = 1; mu_j <= 3; mu_j++) if (( ( mu_j >= 3 ) && ( mu_j <= 3 ) )|| ( ( mu_j >= 2 ) && ( mu_j <= 2 ) )|| ( ( mu_j >= 1 ) && ( mu_j <= 1 ) )) { mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state = mu_BS_START; mu_bs[mu_i].mu_associations[mu_j].mu_sid = 0; mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_ak = mu_useAK( (int)mu_i, mu_j ); mu_bs[mu_i].mu_associations[mu_j].mu_peer = mu_j; mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_costs = 0; }; }; }; }; mu_int.undefine(); { for(int mu_i = 3; mu_i <= 3; mu_i++) { mu_int[mu_i].mu_messages.undefine(); }; }; }; bool UnFair() { return FALSE; } }; class StartStateGenerator { StartStateBase0 S0; public: void Code(unsigned short r) { if (r<=0) { S0.Code(r-0); return; } } char * Name(unsigned short r) { if (r<=0) return S0.Name(r-0); return NULL; } }; unsigned short StartStateManager::numstartstates = 1; /******************** Invariant records ********************/ int mu__invariant_87() // Invariant "If MS is DONE => costs = MS_DONE_COST and intCosts > threshold" { bool mu__quant88; mu__quant88 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant89; mu__quant89 = TRUE; { for(int mu_j = 1; mu_j <= 1; mu_j++) { bool mu__boolexpr90; if (!((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_state) == (mu_MS_DONE))) mu__boolexpr90 = TRUE ; else { bool mu__boolexpr91; if ((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_costs) <= (mu_MS_DONE_COST)) mu__boolexpr91 = TRUE ; else { mu__boolexpr91 = ((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_intCosts) > (mu_INT_THRESHOLD)) ; } mu__boolexpr90 = (mu__boolexpr91) ; } if ( !(mu__boolexpr90) ) { mu__quant89 = FALSE; break; } }; }; if ( !(mu__quant89) ) { mu__quant88 = FALSE; break; } }; }; return mu__quant88; }; bool mu__condition_92() // Condition for Rule "If MS is DONE => costs = MS_DONE_COST and intCosts > threshold" { return mu__invariant_87( ); } /**** end rule declaration ****/ int mu__invariant_93() // Invariant "When MS/BS complete handshake they share a TEK" { bool mu__quant94; mu__quant94 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant95; mu__quant95 = TRUE; { for(int mu_j = 1; mu_j <= 1; mu_j++) { bool mu__boolexpr96; bool mu__boolexpr97; bool mu__boolexpr98; if (!((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_state) == (mu_MS_DONE))) mu__boolexpr98 = FALSE ; else { mu__boolexpr98 = ((mu_ms[mu_j].mu_associations[mu_i].mu_sid) == (mu_bs[mu_i].mu_associations[mu_j].mu_sid)) ; } if (!(mu__boolexpr98)) mu__boolexpr97 = FALSE ; else { mu__boolexpr97 = ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_DONE)) ; } if (!(mu__boolexpr97)) mu__boolexpr96 = TRUE ; else { mu__boolexpr96 = ((mu_bs[mu_i].mu_associations[mu_j].mu_TEKnonce) == (mu_ms[mu_j].mu_associations[mu_i].mu_TEKnonce)) ; } if ( !(mu__boolexpr96) ) { mu__quant95 = FALSE; break; } }; }; if ( !(mu__quant95) ) { mu__quant94 = FALSE; break; } }; }; return mu__quant94; }; bool mu__condition_99() // Condition for Rule "When MS/BS complete handshake they share a TEK" { return mu__invariant_93( ); } /**** end rule declaration ****/ int mu__invariant_100() // Invariant "If MS is WAIT_RES => BS is in WAIT_REQ/DONE" { bool mu__quant101; mu__quant101 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant102; mu__quant102 = TRUE; { for(int mu_j = 1; mu_j <= 1; mu_j++) { bool mu__boolexpr103; bool mu__boolexpr104; if (!((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_state) == (mu_MS_WAIT_RES))) mu__boolexpr104 = FALSE ; else { mu__boolexpr104 = ((mu_ms[mu_j].mu_associations[mu_i].mu_sid) == (mu_bs[mu_i].mu_associations[mu_j].mu_sid)) ; } if (!(mu__boolexpr104)) mu__boolexpr103 = TRUE ; else { mu__boolexpr103 = (!((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_START))) ; } if ( !(mu__boolexpr103) ) { mu__quant102 = FALSE; break; } }; }; if ( !(mu__quant102) ) { mu__quant101 = FALSE; break; } }; }; return mu__quant101; }; bool mu__condition_105() // Condition for Rule "If MS is WAIT_RES => BS is in WAIT_REQ/DONE" { return mu__invariant_100( ); } /**** end rule declaration ****/ int mu__invariant_106() // Invariant "If MS is WAIT_CLG => BS is in START/WAIT_REQ" { bool mu__quant107; mu__quant107 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant108; mu__quant108 = TRUE; { for(int mu_j = 1; mu_j <= 1; mu_j++) { bool mu__boolexpr109; bool mu__boolexpr110; if (!((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_state) == (mu_MS_WAIT_CLG))) mu__boolexpr110 = FALSE ; else { mu__boolexpr110 = ((mu_ms[mu_j].mu_associations[mu_i].mu_sid) == (mu_bs[mu_i].mu_associations[mu_j].mu_sid)) ; } if (!(mu__boolexpr110)) mu__boolexpr109 = TRUE ; else { mu__boolexpr109 = (!((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_DONE))) ; } if ( !(mu__boolexpr109) ) { mu__quant108 = FALSE; break; } }; }; if ( !(mu__quant108) ) { mu__quant107 = FALSE; break; } }; }; return mu__quant107; }; bool mu__condition_111() // Condition for Rule "If MS is WAIT_CLG => BS is in START/WAIT_REQ" { return mu__invariant_106( ); } /**** end rule declaration ****/ int mu__invariant_112() // Invariant "If MS is DONE => BS is DONE" { bool mu__quant113; mu__quant113 = TRUE; { for(int mu_i = 2; mu_i <= 2; mu_i++) { bool mu__quant114; mu__quant114 = TRUE; { for(int mu_j = 1; mu_j <= 1; mu_j++) { bool mu__boolexpr115; bool mu__boolexpr116; if (!((mu_ms[mu_j].mu_associations[mu_i].mu_session.mu_state) == (mu_MS_DONE))) mu__boolexpr116 = FALSE ; else { mu__boolexpr116 = ((mu_ms[mu_j].mu_associations[mu_i].mu_sid) == (mu_bs[mu_i].mu_associations[mu_j].mu_sid)) ; } if (!(mu__boolexpr116)) mu__boolexpr115 = TRUE ; else { mu__boolexpr115 = ((mu_bs[mu_i].mu_associations[mu_j].mu_session.mu_state) == (mu_BS_DONE)) ; } if ( !(mu__boolexpr115) ) { mu__quant114 = FALSE; break; } }; }; if ( !(mu__quant114) ) { mu__quant113 = FALSE; break; } }; }; return mu__quant113; }; bool mu__condition_117() // Condition for Rule "If MS is DONE => BS is DONE" { return mu__invariant_112( ); } /**** end rule declaration ****/ const rulerec invariants[] = { {"If MS is DONE => BS is DONE", &mu__condition_117, NULL, FALSE}, {"If MS is WAIT_CLG => BS is in START/WAIT_REQ", &mu__condition_111, NULL, FALSE}, {"If MS is WAIT_RES => BS is in WAIT_REQ/DONE", &mu__condition_105, NULL, FALSE}, {"When MS/BS complete handshake they share a TEK", &mu__condition_99, NULL, FALSE}, {"If MS is DONE => costs = MS_DONE_COST and intCosts > threshold", &mu__condition_92, NULL, FALSE}, }; const unsigned short numinvariants = 5; /******************/ bool mu__true_live() { return TRUE; } /******************/ /******************** Liveness records ********************/ const liverec livenesses[] = { { NULL, NULL, NULL, NULL, E }}; const unsigned short numlivenesses = 0; /******************** Fairstates records ********************/ const rulerec fairnesses[] = { { NULL, NULL, NULL, FALSE }}; const unsigned short numfairnesses = 0; /******************** Normal/Canonicalization for scalarset ********************/ /* nextNonce:NoScalarset ms:NoScalarset bs:NoScalarset actionCount:NoScalarset nextPN:NoScalarset net:Complex int:Complex */ /******************** Code for symmetry ********************/ /******************** Permutation Set Class ********************/ class PermSet { public: // book keeping enum PresentationType {Simple, Explicit}; PresentationType Presentation; void ResetToSimple(); void ResetToExplicit(); void SimpleToExplicit(); void SimpleToOne(); bool NextPermutation(); void Print_in_size() { int ret=0; for (int i=0; isym_alg.mode == argsym_alg::Exhaustive_Fast_Canonicalize) { /******************** declaration of class variables ********************/ in = new bool[1]; // Set perm and revperm // setting up combination of permutations // for different scalarset int carry; size = 1; count = 1; for (i=0; i<1; i++) { carry = 1; in[i]= TRUE; } } else { /******************** declaration of class variables ********************/ in = new bool[1]; in[0] = TRUE; } } void PermSet::ResetToSimple() { int i; AlreadyOnlyOneRemain = FALSE; Presentation = Simple; } void PermSet::ResetToExplicit() { for (int i=0; i<1; i++) in[i] = TRUE; Presentation = Explicit; } void PermSet::SimpleToExplicit() { int i,j,k; int start, class_size; // Setup range for mapping // To be In or not to be // setup explicit representation // Set perm and revperm for (i=0; i<1; i++) { in[i] = TRUE; } Presentation = Explicit; if (args->test_parameter1.value==0) Print_in_size(); } void PermSet::SimpleToOne() { int i,j,k; int class_size; int start; // Setup range for mapping Presentation = Explicit; } bool PermSet::NextPermutation() { bool nexted = FALSE; int start, end; int class_size; int temp; int j,k; // algorithm // for each class // if forall in the same class reverse_sorted, // { sort again; goto next class } // else // { // nexted = TRUE; // for (j from l to r) // if (for all j+ are reversed sorted) // { // swap j, j+1 // sort all j+ again // break; // } // } if (!nexted) return FALSE; return TRUE; } /******************** Symmetry Class ********************/ class SymmetryClass { PermSet Perm; bool BestInitialized; state BestPermutedState; // utilities void SetBestResult(int i, state* temp); void ResetBestResult() {BestInitialized = FALSE;}; public: // initializer SymmetryClass() : Perm(), BestInitialized(FALSE) {}; ~SymmetryClass() {}; void Normalize(state* s); void Exhaustive_Fast_Canonicalize(state *s); void Heuristic_Fast_Canonicalize(state *s); void Heuristic_Small_Mem_Canonicalize(state *s); void Heuristic_Fast_Normalize(state *s); void MultisetSort(state* s); }; /******************** Symmetry Class Members ********************/ void SymmetryClass::MultisetSort(state* s) { mu_nextNonce.MultisetSort(); mu_ms.MultisetSort(); mu_bs.MultisetSort(); mu_actionCount.MultisetSort(); mu_nextPN.MultisetSort(); mu_net.MultisetSort(); mu_int.MultisetSort(); } void SymmetryClass::Normalize(state* s) { switch (args->sym_alg.mode) { case argsym_alg::Exhaustive_Fast_Canonicalize: Exhaustive_Fast_Canonicalize(s); break; case argsym_alg::Heuristic_Fast_Canonicalize: Heuristic_Fast_Canonicalize(s); break; case argsym_alg::Heuristic_Small_Mem_Canonicalize: Heuristic_Small_Mem_Canonicalize(s); break; case argsym_alg::Heuristic_Fast_Normalize: Heuristic_Fast_Normalize(s); break; default: Heuristic_Fast_Canonicalize(s); } } /******************** Permute and Canonicalize function for different types ********************/ void mu_1_MSId::Permute(PermSet& Perm, int i) {} void mu_1_MSId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_MSId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_MSId::SimpleLimit(PermSet& Perm) {} void mu_1_MSId::ArrayLimit(PermSet& Perm) {} void mu_1_MSId::Limit(PermSet& Perm) {} void mu_1_MSId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_BSId::Permute(PermSet& Perm, int i) {} void mu_1_BSId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_BSId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_BSId::SimpleLimit(PermSet& Perm) {} void mu_1_BSId::ArrayLimit(PermSet& Perm) {} void mu_1_BSId::Limit(PermSet& Perm) {} void mu_1_BSId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_IntruderId::Permute(PermSet& Perm, int i) {} void mu_1_IntruderId::SimpleCanonicalize(PermSet& Perm) {} void mu_1_IntruderId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_IntruderId::SimpleLimit(PermSet& Perm) {} void mu_1_IntruderId::ArrayLimit(PermSet& Perm) {} void mu_1_IntruderId::Limit(PermSet& Perm) {} void mu_1_IntruderId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset type.\n"); }; void mu_1_AgentId::Permute(PermSet& Perm, int i) { if (Perm.Presentation != PermSet::Explicit) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::SimpleCanonicalize(PermSet& Perm) { int i, class_number; if (Perm.Presentation != PermSet::Simple) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::Canonicalize(PermSet& Perm) { Error.Error("Calling canonicalize() for Scalarset."); } void mu_1_AgentId::SimpleLimit(PermSet& Perm) { int i, class_number; if (Perm.Presentation != PermSet::Simple) Error.Error("Internal Error: Wrong Sequence of Normalization"); if (defined()) { } } void mu_1_AgentId::ArrayLimit(PermSet& Perm) {} void mu_1_AgentId::Limit(PermSet& Perm) {} void mu_1_AgentId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for union type.\n"); }; void mu_1_Nonce::Permute(PermSet& Perm, int i) {}; void mu_1_Nonce::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_Nonce::Canonicalize(PermSet& Perm) {}; void mu_1_Nonce::SimpleLimit(PermSet& Perm) {}; void mu_1_Nonce::ArrayLimit(PermSet& Perm) {}; void mu_1_Nonce::Limit(PermSet& Perm) {}; void mu_1_Nonce::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_PN::Permute(PermSet& Perm, int i) {}; void mu_1_PN::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_PN::Canonicalize(PermSet& Perm) {}; void mu_1_PN::SimpleLimit(PermSet& Perm) {}; void mu_1_PN::ArrayLimit(PermSet& Perm) {}; void mu_1_PN::Limit(PermSet& Perm) {}; void mu_1_PN::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_SessionId::Permute(PermSet& Perm, int i) {}; void mu_1_SessionId::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_SessionId::Canonicalize(PermSet& Perm) {}; void mu_1_SessionId::SimpleLimit(PermSet& Perm) {}; void mu_1_SessionId::ArrayLimit(PermSet& Perm) {}; void mu_1_SessionId::Limit(PermSet& Perm) {}; void mu_1_SessionId::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_AK::Permute(PermSet& Perm, int i) { }; void mu_1_AK::SimpleCanonicalize(PermSet& Perm) { mu_peer1.SimpleCanonicalize(Perm); mu_peer2.SimpleCanonicalize(Perm); }; void mu_1_AK::Canonicalize(PermSet& Perm) { }; void mu_1_AK::SimpleLimit(PermSet& Perm) { mu_peer1.SimpleLimit(Perm); mu_peer2.SimpleLimit(Perm); }; void mu_1_AK::ArrayLimit(PermSet& Perm){} void mu_1_AK::Limit(PermSet& Perm) { }; void mu_1_AK::MultisetLimit(PermSet& Perm) { }; void mu_1_MessageType::Permute(PermSet& Perm, int i) {}; void mu_1_MessageType::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_MessageType::Canonicalize(PermSet& Perm) {}; void mu_1_MessageType::SimpleLimit(PermSet& Perm) {}; void mu_1_MessageType::ArrayLimit(PermSet& Perm) {}; void mu_1_MessageType::Limit(PermSet& Perm) {}; void mu_1_MessageType::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for enum type.\n"); }; void mu_1_MAC::Permute(PermSet& Perm, int i) { }; void mu_1_MAC::SimpleCanonicalize(PermSet& Perm) { mu_ak.SimpleCanonicalize(Perm); }; void mu_1_MAC::Canonicalize(PermSet& Perm) { }; void mu_1_MAC::SimpleLimit(PermSet& Perm) { mu_ak.SimpleLimit(Perm); }; void mu_1_MAC::ArrayLimit(PermSet& Perm){} void mu_1_MAC::Limit(PermSet& Perm) { }; void mu_1_MAC::MultisetLimit(PermSet& Perm) { }; void mu_1_Message::Permute(PermSet& Perm, int i) { }; void mu_1_Message::SimpleCanonicalize(PermSet& Perm) { mu_source.SimpleCanonicalize(Perm); mu_dest.SimpleCanonicalize(Perm); mu_address.SimpleCanonicalize(Perm); mu_mac.SimpleCanonicalize(Perm); }; void mu_1_Message::Canonicalize(PermSet& Perm) { }; void mu_1_Message::SimpleLimit(PermSet& Perm) { mu_source.SimpleLimit(Perm); mu_dest.SimpleLimit(Perm); mu_address.SimpleLimit(Perm); mu_mac.SimpleLimit(Perm); }; void mu_1_Message::ArrayLimit(PermSet& Perm){} void mu_1_Message::Limit(PermSet& Perm) { }; void mu_1_Message::MultisetLimit(PermSet& Perm) { }; void mu_1_MSStates::Permute(PermSet& Perm, int i) {}; void mu_1_MSStates::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_MSStates::Canonicalize(PermSet& Perm) {}; void mu_1_MSStates::SimpleLimit(PermSet& Perm) {}; void mu_1_MSStates::ArrayLimit(PermSet& Perm) {}; void mu_1_MSStates::Limit(PermSet& Perm) {}; void mu_1_MSStates::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for enum type.\n"); }; void mu_1__type_0::Permute(PermSet& Perm, int i) {}; void mu_1__type_0::SimpleCanonicalize(PermSet& Perm) {}; void mu_1__type_0::Canonicalize(PermSet& Perm) {}; void mu_1__type_0::SimpleLimit(PermSet& Perm) {}; void mu_1__type_0::ArrayLimit(PermSet& Perm) {}; void mu_1__type_0::Limit(PermSet& Perm) {}; void mu_1__type_0::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1__type_1::Permute(PermSet& Perm, int i) {}; void mu_1__type_1::SimpleCanonicalize(PermSet& Perm) {}; void mu_1__type_1::Canonicalize(PermSet& Perm) {}; void mu_1__type_1::SimpleLimit(PermSet& Perm) {}; void mu_1__type_1::ArrayLimit(PermSet& Perm) {}; void mu_1__type_1::Limit(PermSet& Perm) {}; void mu_1__type_1::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_MSSessions::Permute(PermSet& Perm, int i) { }; void mu_1_MSSessions::SimpleCanonicalize(PermSet& Perm) { mu_ak.SimpleCanonicalize(Perm); }; void mu_1_MSSessions::Canonicalize(PermSet& Perm) { }; void mu_1_MSSessions::SimpleLimit(PermSet& Perm) { mu_ak.SimpleLimit(Perm); }; void mu_1_MSSessions::ArrayLimit(PermSet& Perm){} void mu_1_MSSessions::Limit(PermSet& Perm) { }; void mu_1_MSSessions::MultisetLimit(PermSet& Perm) { }; void mu_1_MSAssociations::Permute(PermSet& Perm, int i) { }; void mu_1_MSAssociations::SimpleCanonicalize(PermSet& Perm) { mu_session.SimpleCanonicalize(Perm); mu_peer.SimpleCanonicalize(Perm); }; void mu_1_MSAssociations::Canonicalize(PermSet& Perm) { }; void mu_1_MSAssociations::SimpleLimit(PermSet& Perm) { mu_session.SimpleLimit(Perm); mu_peer.SimpleLimit(Perm); }; void mu_1_MSAssociations::ArrayLimit(PermSet& Perm){} void mu_1_MSAssociations::Limit(PermSet& Perm) { }; void mu_1_MSAssociations::MultisetLimit(PermSet& Perm) { }; void mu_1__type_2::Permute(PermSet& Perm, int i) { static mu_1__type_2 temp("Permute_mu_1__type_2",-1); int j; for (j=0; j<3; j++) array[j].Permute(Perm, i); }; void mu_1__type_2::SimpleCanonicalize(PermSet& Perm) { for (int j=0; j<3; j++) array[j].SimpleCanonicalize(Perm); } void mu_1__type_2::Canonicalize(PermSet& Perm) { // indexes int i,j,k,z; // sorting static mu_1_MSAssociations value[3]; int compare; // limit bool exists; bool split; // range mapping int start; int class_size; // canonicalization static mu_1__type_2 temp; } void mu_1__type_2::SimpleLimit(PermSet& Perm) { for (int j=0; j<3; j++) { array[j].SimpleLimit(Perm); } } void mu_1__type_2::ArrayLimit(PermSet& Perm) { // indexes int i,j,k,z; // sorting int compare; static mu_1_MSAssociations value[3]; // limit bool exists; bool split; } void mu_1__type_2::Limit(PermSet& Perm) { // indexes int i,j,k,z; // while guard bool while_guard, while_guard_temp; // sorting static mu_1_MSAssociations value[3]; // limit bool exists; bool split; int i0; // refinement -- checking priority in general while_guard = FALSE; while ( while_guard ) { while_guard = FALSE; while_guard_temp = while_guard; while_guard = FALSE; while_guard = while_guard && while_guard_temp; } // end while } void mu_1__type_2::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset array.\n"); }; void mu_1_MS::Permute(PermSet& Perm, int i) { }; void mu_1_MS::SimpleCanonicalize(PermSet& Perm) { mu_associations.SimpleCanonicalize(Perm); }; void mu_1_MS::Canonicalize(PermSet& Perm) { }; void mu_1_MS::SimpleLimit(PermSet& Perm) { mu_associations.SimpleLimit(Perm); }; void mu_1_MS::ArrayLimit(PermSet& Perm){} void mu_1_MS::Limit(PermSet& Perm) { }; void mu_1_MS::MultisetLimit(PermSet& Perm) { }; void mu_1_BSStates::Permute(PermSet& Perm, int i) {}; void mu_1_BSStates::SimpleCanonicalize(PermSet& Perm) {}; void mu_1_BSStates::Canonicalize(PermSet& Perm) {}; void mu_1_BSStates::SimpleLimit(PermSet& Perm) {}; void mu_1_BSStates::ArrayLimit(PermSet& Perm) {}; void mu_1_BSStates::Limit(PermSet& Perm) {}; void mu_1_BSStates::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for enum type.\n"); }; void mu_1__type_3::Permute(PermSet& Perm, int i) {}; void mu_1__type_3::SimpleCanonicalize(PermSet& Perm) {}; void mu_1__type_3::Canonicalize(PermSet& Perm) {}; void mu_1__type_3::SimpleLimit(PermSet& Perm) {}; void mu_1__type_3::ArrayLimit(PermSet& Perm) {}; void mu_1__type_3::Limit(PermSet& Perm) {}; void mu_1__type_3::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1__type_4::Permute(PermSet& Perm, int i) {}; void mu_1__type_4::SimpleCanonicalize(PermSet& Perm) {}; void mu_1__type_4::Canonicalize(PermSet& Perm) {}; void mu_1__type_4::SimpleLimit(PermSet& Perm) {}; void mu_1__type_4::ArrayLimit(PermSet& Perm) {}; void mu_1__type_4::Limit(PermSet& Perm) {}; void mu_1__type_4::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for subrange type.\n"); }; void mu_1_BSSessions::Permute(PermSet& Perm, int i) { }; void mu_1_BSSessions::SimpleCanonicalize(PermSet& Perm) { mu_ak.SimpleCanonicalize(Perm); }; void mu_1_BSSessions::Canonicalize(PermSet& Perm) { }; void mu_1_BSSessions::SimpleLimit(PermSet& Perm) { mu_ak.SimpleLimit(Perm); }; void mu_1_BSSessions::ArrayLimit(PermSet& Perm){} void mu_1_BSSessions::Limit(PermSet& Perm) { }; void mu_1_BSSessions::MultisetLimit(PermSet& Perm) { }; void mu_1_BSAssociations::Permute(PermSet& Perm, int i) { }; void mu_1_BSAssociations::SimpleCanonicalize(PermSet& Perm) { mu_session.SimpleCanonicalize(Perm); mu_peer.SimpleCanonicalize(Perm); }; void mu_1_BSAssociations::Canonicalize(PermSet& Perm) { }; void mu_1_BSAssociations::SimpleLimit(PermSet& Perm) { mu_session.SimpleLimit(Perm); mu_peer.SimpleLimit(Perm); }; void mu_1_BSAssociations::ArrayLimit(PermSet& Perm){} void mu_1_BSAssociations::Limit(PermSet& Perm) { }; void mu_1_BSAssociations::MultisetLimit(PermSet& Perm) { }; void mu_1__type_5::Permute(PermSet& Perm, int i) { static mu_1__type_5 temp("Permute_mu_1__type_5",-1); int j; for (j=0; j<3; j++) array[j].Permute(Perm, i); }; void mu_1__type_5::SimpleCanonicalize(PermSet& Perm) { for (int j=0; j<3; j++) array[j].SimpleCanonicalize(Perm); } void mu_1__type_5::Canonicalize(PermSet& Perm) { // indexes int i,j,k,z; // sorting static mu_1_BSAssociations value[3]; int compare; // limit bool exists; bool split; // range mapping int start; int class_size; // canonicalization static mu_1__type_5 temp; } void mu_1__type_5::SimpleLimit(PermSet& Perm) { for (int j=0; j<3; j++) { array[j].SimpleLimit(Perm); } } void mu_1__type_5::ArrayLimit(PermSet& Perm) { // indexes int i,j,k,z; // sorting int compare; static mu_1_BSAssociations value[3]; // limit bool exists; bool split; } void mu_1__type_5::Limit(PermSet& Perm) { // indexes int i,j,k,z; // while guard bool while_guard, while_guard_temp; // sorting static mu_1_BSAssociations value[3]; // limit bool exists; bool split; int i0; // refinement -- checking priority in general while_guard = FALSE; while ( while_guard ) { while_guard = FALSE; while_guard_temp = while_guard; while_guard = FALSE; while_guard = while_guard && while_guard_temp; } // end while } void mu_1__type_5::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for scalarset array.\n"); }; void mu_1_BS::Permute(PermSet& Perm, int i) { }; void mu_1_BS::SimpleCanonicalize(PermSet& Perm) { mu_associations.SimpleCanonicalize(Perm); }; void mu_1_BS::Canonicalize(PermSet& Perm) { }; void mu_1_BS::SimpleLimit(PermSet& Perm) { mu_associations.SimpleLimit(Perm); }; void mu_1_BS::ArrayLimit(PermSet& Perm){} void mu_1_BS::Limit(PermSet& Perm) { }; void mu_1_BS::MultisetLimit(PermSet& Perm) { }; void mu_1__type_6::Permute(PermSet& Perm, int i) { static mu_1__type_6 temp("Permute_mu_1__type_6",-1); int j; for (j=0; j<10; j++) array[j].Permute(Perm, i); }; void mu_1__type_6::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: calling SimpleCanonicalize for a multiset.\n"); }; void mu_1__type_6::Canonicalize(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_6::SimpleLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_6::ArrayLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_6::Limit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_6::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for multiset type of scalarset-free elements.\n"); }; void mu_1__type_7::Permute(PermSet& Perm, int i) { static mu_1__type_7 temp("Permute_mu_1__type_7",-1); int j; for (j=0; j<10; j++) array[j].Permute(Perm, i); }; void mu_1__type_7::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: calling SimpleCanonicalize for a multiset.\n"); }; void mu_1__type_7::Canonicalize(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_7::SimpleLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_7::ArrayLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_7::Limit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_7::MultisetLimit(PermSet& Perm) { Error.Error("Internal: calling MultisetLimit for multiset type of scalarset-free elements.\n"); }; void mu_1__type_8::Permute(PermSet& Perm, int i) { static mu_1__type_8 temp("Permute_mu_1__type_8",-1); int j; for (j=0; j<10; j++) array[j].Permute(Perm, i); }; void mu_1__type_8::SimpleCanonicalize(PermSet& Perm) { Error.Error("Internal: calling SimpleCanonicalize for a multiset.\n"); }; void mu_1__type_8::Canonicalize(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_8::SimpleLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_8::ArrayLimit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_8::Limit(PermSet& Perm) { Error.Error("You cannot use this symmetry algorithm with Multiset.\n"); }; void mu_1__type_8::MultisetLimit(PermSet& Perm) { // indexes int i,j,k,z; // while guard bool while_guard, while_guard_temp; // sorting static mu_1_MAC value[10]; // limit bool exists; bool split; int i0; int count_multisetindex, oldcount_multisetindex; bool pos_multisetindex[10][10]; bool goodset_multisetindex[10]; mu_1_MAC temp; // compact for (i = 0, j = 0; i < 10; i++) if (valid[i].value()) { if (j!=i) array[j++] = array[i]; else j++; } if (j != current_size) current_size = j; for (i = j; i < 10; i++) array[i].undefine(); for (i = 0; i < j; i++) valid[i].value(TRUE); for (i = j; i < 10; i++) valid[i].value(FALSE); // bubble sort for (i = 0; i < current_size; i++) for (j = i+1; j < current_size; j++) if (CompareWeight(array[i],array[j])>0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } // initializing pos array for (i=0; i0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } // initializing pos array for (i=0; i0) { temp = array[i]; array[i] = array[j]; array[j] = temp; } // initializing pos array for (i=0; isymmetry_reduction.value) { if ( args->sym_alg.mode == argsym_alg::Exhaustive_Fast_Canonicalize) { Perm.ResetToExplicit(); for (i=0; imultiset_reduction.value) mu_nextNonce.MultisetSort(); mu_ms.Permute(Perm,i); if (args->multiset_reduction.value) mu_ms.MultisetSort(); mu_bs.Permute(Perm,i); if (args->multiset_reduction.value) mu_bs.MultisetSort(); mu_actionCount.Permute(Perm,i); if (args->multiset_reduction.value) mu_actionCount.MultisetSort(); mu_nextPN.Permute(Perm,i); if (args->multiset_reduction.value) mu_nextPN.MultisetSort(); mu_net.Permute(Perm,i); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,i); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } } StateCopy(workingstate,&temp); return FALSE; } else { Perm.ResetToSimple(); Perm.SimpleToOne(); if (ns != workingstate) StateCopy(workingstate, ns); mu_nextNonce.Permute(Perm,0); if (args->multiset_reduction.value) mu_nextNonce.MultisetSort(); mu_ms.Permute(Perm,0); if (args->multiset_reduction.value) mu_ms.MultisetSort(); mu_bs.Permute(Perm,0); if (args->multiset_reduction.value) mu_bs.MultisetSort(); mu_actionCount.Permute(Perm,0); if (args->multiset_reduction.value) mu_actionCount.MultisetSort(); mu_nextPN.Permute(Perm,0); if (args->multiset_reduction.value) mu_nextPN.MultisetSort(); mu_net.Permute(Perm,0); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,0); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } while (Perm.NextPermutation()) { if (ns != workingstate) StateCopy(workingstate, ns); mu_nextNonce.Permute(Perm,0); if (args->multiset_reduction.value) mu_nextNonce.MultisetSort(); mu_ms.Permute(Perm,0); if (args->multiset_reduction.value) mu_ms.MultisetSort(); mu_bs.Permute(Perm,0); if (args->multiset_reduction.value) mu_bs.MultisetSort(); mu_actionCount.Permute(Perm,0); if (args->multiset_reduction.value) mu_actionCount.MultisetSort(); mu_nextPN.Permute(Perm,0); if (args->multiset_reduction.value) mu_nextPN.MultisetSort(); mu_net.Permute(Perm,0); if (args->multiset_reduction.value) mu_net.MultisetSort(); mu_int.Permute(Perm,0); if (args->multiset_reduction.value) mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } } StateCopy(workingstate,&temp); return FALSE; } } if (!args->symmetry_reduction.value && args->multiset_reduction.value) { if (ns != workingstate) StateCopy(workingstate, ns); mu_nextNonce.MultisetSort(); mu_ms.MultisetSort(); mu_bs.MultisetSort(); mu_actionCount.MultisetSort(); mu_nextPN.MultisetSort(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (p.compare(workingstate)) { StateCopy(workingstate,&temp); return TRUE; } StateCopy(workingstate,&temp); return FALSE; } return (p.compare(ns)); } /******************** Canonicalization by fast exhaustive generation of all permutations ********************/ void SymmetryClass::Exhaustive_Fast_Canonicalize(state* s) { int i; static state temp; Perm.ResetToExplicit(); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_nextNonce.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_ms.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_bs.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_actionCount.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_nextPN.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_net.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); StateCopy(&temp, workingstate); ResetBestResult(); for (i=0; imultiset_reduction.value) mu_int.MultisetSort(); SetBestResult(i, workingstate); } StateCopy(workingstate, &BestPermutedState); }; /******************** Canonicalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and fast exhaustive generation of all permutations for other variables ********************/ void SymmetryClass::Heuristic_Fast_Canonicalize(state* s) { int i; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_ms.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_bs.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_net.MultisetLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_int.MultisetLimit(Perm); } }; /******************** Canonicalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and fast exhaustive generation of all permutations for other variables and use less local memory ********************/ void SymmetryClass::Heuristic_Small_Mem_Canonicalize(state* s) { unsigned long cycle; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_ms.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_bs.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_net.MultisetLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_int.MultisetLimit(Perm); } }; /******************** Normalization by fast simple variable canonicalization, fast simple scalarset array canonicalization, fast restriction on permutation set with simple scalarset array of scalarset, and for all other variables, pick any remaining permutation ********************/ void SymmetryClass::Heuristic_Fast_Normalize(state* s) { int i; static state temp; Perm.ResetToSimple(); mu_net.MultisetSort(); mu_int.MultisetSort(); if (Perm.MoreThanOneRemain()) { mu_ms.SimpleLimit(Perm); } if (Perm.MoreThanOneRemain()) { mu_bs.SimpleLimit(Perm); } }; /******************** Include ********************/ #include "mu_epilog.inc"