diff --git a/src/compiler.c b/src/compiler.c index 8f803ef..98d4296 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -466,7 +466,7 @@ isClaimlabelUsed (const System sys, const Term label) //! Generate a fresh claim label Term generateFreshClaimlabel (const System sys, const Protocol protocol, - const Role role, const Term claim) + const Role role, const Term claim, const int n) { Term label; @@ -489,13 +489,16 @@ claimCreate (const System sys, const Protocol protocol, const Role role, const Term claim, Term label, const Term msg, const int lineno) { Claimlist cl; + int len; + + len = roledef_length (role->roledef); /* generate full unique label */ /* is the label empty or used? */ if (label == NULL || isClaimlabelUsed (sys, label)) { /* simply generate a fresh one */ - label = generateFreshClaimlabel (sys, protocol, role, claim); + label = generateFreshClaimlabel (sys, protocol, role, claim, len); } // Assert: label is unique, add claimlist info @@ -606,7 +609,18 @@ commEvent (int event, Tac tc) * This can be a weird choice if it is a read or send, because in that case * we cannot chain them anymore and the send-read correspondence is lost. */ - label = freshTermPrefix (thisRole->nameterm); + int n; + Roledef rd; + + n = 1; + for (rd = thisRole->roledef; rd != NULL; rd = rd->next) + { + if (rd->type == CLAIM) + { + n++; + } + } + label = intTermPrefix (n, thisRole->nameterm); } else { diff --git a/src/symbol.c b/src/symbol.c index 53f4429..48ca4ac 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -291,6 +291,60 @@ symbolNextFree (Symbol prefixsymbol) return NULL; } +//! Return symbol according to integer +Symbol +symbolFromInt (int n, Symbol prefixsymbol) +{ + char *prefixstr; + int len; + + if (!(n <= 9999)) + { + error ("Can only make symbol from int when smaller than 10000"); + } + + if (prefixsymbol != NULL) + { + prefixstr = (char *) prefixsymbol->text; + len = strlen (prefixstr); + } + else + { + prefixstr = ""; + len = 0; + } + + /* + * The construction below (variable buffer length) is not allowed in ISO C90 + */ + char buffer[len + 5]; // thus we must enforce a maximum of 9.999 (allowing for storage of \0 ) + Symbol symb; + int slen; + + slen = sprintf (buffer, "%s%i", prefixstr, n); + buffer[slen] = EOS; + symb = lookup (buffer); + if (symb == NULL) + { + char *newstring; + // Copy the buffer to something that will survive + /** + * Memory leak: although this routine should not be called recursively, it will never de-allocate this memory. + * Thus, some precaution is necessary. + * [x][CC] + */ + newstring = (char *) malloc (slen + 1); + memcpy (newstring, buffer, slen + 1); + + /* This persistent string can be used to return a fresh symbol */ + + symb = symbolSysConst (newstring); + } + + return symb; + +} + //! Fix all the unset keylevels void symbol_fix_keylevels (void) diff --git a/src/symbol.h b/src/symbol.h index c71b943..09cbb8c 100644 --- a/src/symbol.h +++ b/src/symbol.h @@ -67,6 +67,7 @@ void symbolPrintAll (void); Symbol symbolSysConst (const char *str); void symbol_fix_keylevels (void); Symbol symbolNextFree (Symbol prefixsymbol); +Symbol symbolFromInt (int n, Symbol prefixsymbol); void eprintf (char *fmt, ...); void veprintf (const char *fmt, va_list args); diff --git a/src/term.c b/src/term.c index 4590e4f..da02e9d 100644 --- a/src/term.c +++ b/src/term.c @@ -1386,6 +1386,22 @@ freshTermPrefix (Term prefixterm) return makeTermType (GLOBAL, freshsymbol, -1); } +//! Generate a term from an int, prefixed with the string of the given term. +Term +intTermPrefix (const int n, Term prefixterm) +{ + Symbol prefixsymbol; + Symbol freshsymbol; + + prefixsymbol = NULL; + if (prefixterm != NULL && realTermLeaf (prefixterm)) + { + prefixsymbol = TermSymb (prefixterm); + } + freshsymbol = symbolFromInt (n, prefixsymbol); + return makeTermType (GLOBAL, freshsymbol, -1); +} + //! Determine whether a term is a functor int isTermFunctionName (Term t) diff --git a/src/term.h b/src/term.h index 0891842..377ad47 100644 --- a/src/term.h +++ b/src/term.h @@ -201,6 +201,7 @@ void term_set_keylevels (const Term term); void termPrintDiff (Term t1, Term t2); int isLeafNameEqual (Term t1, Term t2); Term freshTermPrefix (Term prefixterm); +Term intTermPrefix (const int n, Term prefixterm); int isTermFunctionName (Term t); Term getTermFunction (Term t); unsigned int termHidelevel (const Term tsmall, Term tbig);