From 9634034ebbc400e2ca127b9bc299535d21621a84 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 14 Jun 2004 22:08:47 +0000
Subject: [PATCH] - First broken steps towards prec() computation for each
 claim label.

---
 src/compiler.c | 50 +++++++++++++++++++++++++++++++++++++++++++++++++-
 src/compiler.h |  1 +
 src/main.c     |  3 +++
 src/runs.c     | 12 ++++++++++++
 src/runs.h     | 24 ++++++++++++++++++++++++
 5 files changed, 89 insertions(+), 1 deletion(-)

diff --git a/src/compiler.c b/src/compiler.c
index 7694375..a8fd0f5 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -3,6 +3,7 @@
 #include "tac.h"
 #include "terms.h"
 #include "termlists.h"
+#include "memory.h"
 #include "runs.h"
 #include "knowledge.h"
 #include "symbols.h"
@@ -316,6 +317,7 @@ void
 commEvent (int event, Tac tc)
 {
   /* Add an event to the roledef, send or read */
+  Claimlist cl;
   Term fromrole = NULL;
   Term torole = NULL;
   Term msg = NULL;
@@ -360,7 +362,7 @@ commEvent (int event, Tac tc)
       /* now parse tuple info */
       if (trip == NULL || trip->next == NULL)
 	{
-          error ("Problem with %i event on line %i.", event, tc->lineno);
+          error ("Problem with claim %i event on line %i.", event, tc->lineno);
 	}
       fromrole = tacTerm (trip);
       claimbig = tacTerm (tacTuple ((trip->next)));
@@ -396,6 +398,31 @@ commEvent (int event, Tac tc)
 	    }
 	}
 
+      /* store claim in claim list */
+      
+      // First check whether label is unique
+      cl = sys->claimlist;
+      while (cl != NULL)
+	{
+	  if (isTermEqual (cl->label, label))
+	    {
+	      /**
+	       *@todo This should not error exit, but automatically generate a fresh claim label.
+	       */
+	      error ("Claim label is not unique at line %i.",tc->lineno);
+	    }
+	  cl = cl->next;
+	}
+      // Assert: label is unique, add claimlist info
+      cl = memAlloc (sizeof (struct claimlist));
+      cl->label = label;
+      cl->rolename = fromrole;
+      cl->count = 0;
+      cl->failed = 0;
+      cl->prec = NULL;
+      cl->next = sys->claimlist;
+      sys->claimlist = cl;
+
       /* handles all claim types differently */
 
       if (claim == CLAIM_Secret)
@@ -719,3 +746,24 @@ tacTermlist (Tac tc)
     }
   return tl;
 }
+
+//! Compute prec() sets for each claim.
+void
+compute_prec_sets (const System sys)
+{
+  Claimlist cl;
+
+  // Process each individual claim
+  cl = sys->claimlist;
+  while (cl != NULL)
+    {
+      //!@todo compute transitive closure
+    }
+}
+
+//! Preprocess after system compilation
+void 
+preprocess (const System sys)
+{
+  compute_prec_sets(sys);
+}
diff --git a/src/compiler.h b/src/compiler.h
index 837aa93..c6e19ca 100644
--- a/src/compiler.h
+++ b/src/compiler.h
@@ -2,5 +2,6 @@
 #define COMPILER
 
 void compile (System sys, Tac tc, int maxruns);
+void preprocess (const System sys);
 
 #endif
diff --git a/src/main.c b/src/main.c
index ffdeeeb..c00a886 100644
--- a/src/main.c
+++ b/src/main.c
@@ -288,6 +288,9 @@ main (int argc, char **argv)
   compile (sys, spdltac, maxruns->ival[0]);
   scanner_cleanup ();
 
+  /* preprocess */
+  preprocess (sys);
+
 #ifdef DEBUG
   if (DEBUGL (1))
     {
diff --git a/src/runs.c b/src/runs.c
index f2088d1..d5d7dfc 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -81,6 +81,8 @@ systemInit ()
   sys->untrusted = NULL;
   sys->secrets = NULL;		// list of claimed secrets
   sys->attack = NULL;
+  /* no protocols => no protocol preprocessed */
+  sys->claimlist = NULL;
 
   /* matching CLP */
   sys->constraints = NULL;	// no initial constraints
@@ -99,12 +101,22 @@ systemInit ()
 void
 systemReset (const System sys)
 {
+  Claimlist cl;
+
   /* some initial counters */
   sys->statesLow = 0;		// number of explored states
   sys->statesHigh = 0;		// this is not as ridiculous as it might seem
   sys->explore = 1;		// do explore the space
   sys->claims = 0;		// number of claims encountered
   sys->failed = 0;		// number of failed claims
+  cl = sys->claimlist;
+  while (cl != NULL)
+    {
+      cl->count = 0;
+      cl->failed = 0;
+      cl = cl->next;
+    }
+  
   sys->knowPhase = 0;		// knowledge transition id
 
   termlistDestroy (sys->secrets);	// remove old secrets list
diff --git a/src/runs.h b/src/runs.h
index 0c7b888..b29a011 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -2,6 +2,7 @@
 #define RUNS
 
 #include "terms.h"
+#include "termmaps.h"
 #include "termlists.h"
 #include "knowledge.h"
 #include "constraints.h"
@@ -154,6 +155,26 @@ struct tracebuf
   Varbuf	variables;
 };
 
+//! The container for the claim info list
+struct claimlist
+{
+  //! The term element for this node.
+  Term label;
+  //! The name of the role in which it occurs.
+  Term rolename;
+  //! Number of occurrences in system exploration.
+  int count;
+  //! Number of occurrences that failed.
+  int failed;
+  //! Preceding label list
+  Termlist prec;
+  //! Next node pointer or NULL for the last element of the function.
+  struct claimlist *next;
+};
+
+//! Shorthand for claimlist pointers.
+typedef struct claimlist *Claimlist;
+
 //! The main state structure.
 struct system
 {
@@ -206,6 +227,9 @@ struct system
   Termlist variables;
   Termlist untrusted;
 
+  /* protocol preprocessing */
+  Claimlist claimlist;
+
   /* constructed trace pointers, static */
   Roledef *traceEvent;		// MaxRuns * maxRoledef
   int *traceRun;		// MaxRuns * maxRoledef