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

BUGFIX: --one-role-per-agent switch had a bug that made it cut too many patterns.

Browse Source
This commit is contained in:
Cas Cremers 2014-06-20 17:02:23 +01:00
parent 4f252d55a7
commit e966bc88dd
1 changed files with 17 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
src/prune_theorems.c
View File

@ -258,35 +258,30 @@ multipleRolePrune (const System sys)
p = sys->runs[run].protocol;
if ((p != INTRUDER) && (!isHelperProtocol (p)))
{
Role r;
Term rolename;
Term agent;
Termlist tl;
for (r = p->roles; r != NULL; r = r->next)
rolename = sys->runs[run].role->nameterm;
agent = agentOfRun (sys, run);
// Does this agent already occur yet in the list?
for (tl = agentrole; tl != NULL; tl = (tl->next)->next)
{
Term role, agent;
Termlist tl;
// Find mapping role->agent
role = r->nameterm;
agent = agentOfRunRole (sys, run, role);
// Does this agent already occur yet in the list?
for (tl = agentrole; tl != NULL; tl = (tl->next)->next)
if (isTermEqual (agent, tl->term))
{
if (isTermEqual (agent, tl->term))
if (!isTermEqual (rolename, (tl->next)->term))
{
if (!isTermEqual (role, (tl->next)->term))
{
// Same agent, but different role! This is not allowed.
termlistDelete (agentrole); // cleanup
return true;
}
// Same agent, but different role! This is not allowed.
termlistDelete (agentrole); // cleanup
return true;
}
}
// Does not occur yet, so add
// Note we add the elements in front, so we need to reverse the order
agentrole = termlistPrepend (agentrole, role);
agentrole = termlistPrepend (agentrole, agent);
}
// Does not occur yet, so add
// Note we add the elements in front, so we need to reverse the order
agentrole = termlistPrepend (agentrole, rolename);
agentrole = termlistPrepend (agentrole, agent);
}
}
termlistDelete (agentrole);