/****************************** 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__boolexpr6