From 0fee6b5797e3ff016811c623aacb87e0f55d81a8 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sat, 14 Aug 2004 19:19:23 +0000
Subject: [PATCH] - Secrecy claims are now handled fairly okayish, as long as
 only one   term is in the claim. This should be tupling-or, really, for  
 convenience.

---
 src/arachne.c  | 27 ++++++++++++++++++++++++++-
 src/compiler.c |  3 +++
 src/role.h     |  2 ++
 3 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/arachne.c b/src/arachne.c
index 53728c1..3c88c7e 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -18,6 +18,10 @@
 #include "claim.h"
 #include "debug.h"
 
+extern CLAIM_Secret;
+extern CLAIM_Nisynch;
+extern CLAIM_Niagree;
+
 static System sys;
 Protocol INTRUDER;		// Pointers, to be set by the Init
 Role I_GOAL;			// Same here.
@@ -715,6 +719,18 @@ prune ()
   return 0;
 }
 
+//! Setup system for specific claim test
+add_claim_specifics (Claimlist cl, Roledef rd)
+{
+  if (isTermEqual (cl->type, CLAIM_Secret))
+    {
+      /**
+       * Secrecy claim
+       */
+      create_intruder_goal (rd->message);
+    }
+}
+
 //------------------------------------------------------------------------
 // Main logic core
 //------------------------------------------------------------------------
@@ -877,6 +893,12 @@ arachne ()
 
       roleInstance (sys, p, r, NULL);
       sys->runs[0].length = cl->ev + 1;
+
+      /**
+       * Add specific goal info
+       */
+      add_claim_specifics (cl, roledef_shift(sys->runs[0].start, cl->ev));
+
 #ifdef DEBUG
       if (DEBUGL (5))
 	{
@@ -890,7 +912,10 @@ arachne ()
       iterate ();
 
       //! Destroy
-      roleInstanceDestroy (sys);
+      while (sys->maxruns > 0)
+	{
+          roleInstanceDestroy (sys);
+	}
 
       // next
       cl = cl->next;
diff --git a/src/compiler.c b/src/compiler.c
index 1542aaf..6bd20f6 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -467,6 +467,7 @@ commEvent (int event, Tac tc)
       cl->protocol = thisProtocol;
       cl->rolename = fromrole;
       cl->role = thisRole;
+      cl->roledef = NULL;
       cl->count = 0;
       cl->failed = 0;
       cl->prec = NULL;
@@ -1113,6 +1114,8 @@ compute_prec_sets (const System sys)
       // Store in claimlist structure
       cl->r = r1;
       cl->ev = ev1;
+      cl->roledef = rd;
+
       /*
        * We have found the claim roledef, and r1,ev1
        * Now we compute the preceding label set
diff --git a/src/role.h b/src/role.h
index 7b5c183..3d791b7 100644
--- a/src/role.h
+++ b/src/role.h
@@ -24,6 +24,8 @@ struct claimlist
   Term rolename;
   //! The pointer to the role structure
   void *role;
+  //! The pointer to the roledef
+  void *roledef;
   //! Number of occurrences in system exploration.
   states_t count;
   //! Number of occurrences that failed.