From 27d3bb40614d06dacba164fa6b9a5baebd090c90 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 14 Jul 2004 12:46:11 +0000
Subject: [PATCH] - Previous entry was buggy; killing the roledef removed very
 extensive   parts of the tree. Solved by restoring it after recursing, which
 is   waht should have happened in the first place. - It's still a good
 improvement though.

---
 src/modelchecker.c | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/modelchecker.c b/src/modelchecker.c
index 89510c6..823d55c 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -193,7 +193,7 @@ executeStep (const System sys, const int run)
 /**
  * remove from a roledef that is instantiated, the uninteresting ends bits
  */
-void removeIrrelevant (const System sys, const int run, Roledef rd)
+Roledef removeIrrelevant (const System sys, const int run, Roledef rd)
 {
   Roledef rdkill;
   int killclaims;
@@ -227,8 +227,7 @@ void removeIrrelevant (const System sys, const int run, Roledef rd)
   */
 
   /* remove after rdkill */
-  roledefDelete (rdkill->next);
-  rdkill->next = NULL;
+  return rdkill;
 }
 
 //! Explores the system state given by the next step of a run.
@@ -242,9 +241,11 @@ explorify (const System sys, const int run)
   Roledef rd;
   int flag;
   int myStep;
+  Roledef roleCap, roleCapPart;
 
   rd = runPointerGet (sys, run);
   myStep = sys->runs[run].step;
+  roleCap = NULL;
 
   if (rd == NULL)
     {
@@ -341,7 +342,7 @@ explorify (const System sys, const int run)
       /* Special check 3: if after choosing, this run ends on (read|skippedclaim)*, we can remove that part already.
        */
 
-      removeIrrelevant (sys, run, rd);
+      roleCap = removeIrrelevant (sys, run, rd);
 
       /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted,
        * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not
@@ -362,6 +363,12 @@ explorify (const System sys, const int run)
     }
 
   /* Apparently, all is well, and we can explore further */
+  flag = 0;
+  if (roleCap != NULL)
+    {
+      roleCapPart = roleCap->next;
+      roleCap->next = NULL;
+    }
   if (executeStep (sys, run))
     {
       /* traverse the system after the step */
@@ -370,9 +377,12 @@ explorify (const System sys, const int run)
       sys->runs[run].step = myStep;	// reset local index
       sys->step--;
       indentSet (sys->step);
-      return flag;
     }
-  return 0;
+  if (roleCap != NULL)
+    {
+      roleCap->next = roleCapPart;
+    }
+  return flag;
 }
 
 int