andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

BUGFIX: Use name as reference point, not after deVar.

Browse Source 
This is not a real bug but only in the sense that the heuristic didn't always work as intended for choosing names.
This commit is contained in:
Cas Cremers 2014-06-30 23:11:39 +01:00
parent b0e5128e23
commit 277bb0a256
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/arachne.c
View File

@ -1849,12 +1849,12 @@ chooseBestCandidate (Termlist candidatelist, Term var)
* - seen is a termlist that contains newly generated terms (usage: seen = createNewTerm(seen,.. )
* - typeterm is the type name term (e.g., "Agent" term, "Data" in case not clear.)
* - isagent is a boolean that is true iff we are looking for an agent name from the initial knowledge for a role
* - var is the variable term
* - var is the variable term of which we use the name
*
* Output: the first element of the returned list, which is otherwise equal to seen.
*/
Termlist
createNewTerm (Termlist seen, Term typeterm, int isagent, Term var)
createNewTerm (Termlist seen, Term typeterm, int isagent, Term nameterm)
{
/* Does if have an explicit type?
* If so, we try to find a fresh name from the intruder knowledge first.
@ -1868,7 +1868,7 @@ createNewTerm (Termlist seen, Term typeterm, int isagent, Term var)
{
Term t;
t = chooseBestCandidate (candidatelist, var);
t = chooseBestCandidate (candidatelist, nameterm);
termlistDelete (candidatelist);
return termlistPrepend (seen, t);
}
@ -1943,7 +1943,8 @@ makeTraceConcrete (const System sys)
}
// We should turn this into an actual term
tlnew =
createNewTerm (tlnew, name, isAgentType (var->stype), var);
createNewTerm (tlnew, name, isAgentType (var->stype),
tl->term);
var->subst = tlnew->term;
// Store for undo later