From 6374683d1736c5e75a0db04f4b34a4f0020c4356 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Mon, 30 Jun 2014 23:11:39 +0100
Subject: [PATCH] Visualisation improvement: role variables get priority in
 assigning concrete values.

Previously, if a local (non-role) variable would have (implicit) agent type,
it would be assigned a concrete term before the roles. This would lead to
non-optimal choices, since we care more about the role instantiations than about other variables.

However, when making traces concrete, we use the run's 'locals' list. Because of
the way this is constructed (in reverse), non-role variables precede the role variables.
We therefore choose to traverse the list in reverse.
---
 src/arachne.c | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 1dbbc1d..174f166 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -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);
 	}
@@ -1912,24 +1912,27 @@ makeTraceConcrete (const System sys)
 
   changedvars = NULL;
   tlnew = findUsedConstants (sys);
-  run = 0;
 
-  while (run < sys->maxruns)
+  for (run = 0; run < sys->maxruns; run++)
     {
       Termlist tl;
 
-      tl = sys->runs[run].locals;
-      while (tl != NULL)
+      for (tl = termlistForward (sys->runs[run].locals); tl != NULL;
+	   tl = tl->prev)
 	{
+	  Term basevar;
+
+	  basevar = tl->term;
+
 	  /* variable, and of some run? */
-	  if (isTermVariable (tl->term) && TermRunid (tl->term) >= 0)
+	  if (isTermVariable (basevar) && TermRunid (basevar) >= 0)
 	    {
 	      Term var;
 	      Term name;
 	      Termlist vartype;
 
-	      var = deVar (tl->term);
-	      vartype = var->stype;
+	      var = deVar (basevar);
+	      vartype = basevar->stype;
 	      // Determine class name
 	      if (vartype != NULL)
 		{
@@ -1943,15 +1946,14 @@ 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),
+			       basevar);
 	      var->subst = tlnew->term;
 
 	      // Store for undo later
-	      changedvars = termlistAdd (changedvars, var);
+	      TERMLISTADD (changedvars, var);
 	    }
-	  tl = tl->next;
 	}
-      run++;
     }
   termlistDelete (tlnew);
   return changedvars;