- Present from Cas for Cas' birthday: Not thoroughly tested, but ni-synch seems to be working. Be careful to use the -t1 switch, or attacks will be missed.

src/claims.c

@@ -25,8 +25,10 @@ events_match (const System sys, const int i, const int j)
 
   rdi = sys->traceEvent[i];
   rdj = sys->traceEvent[j];
-  if (rdi->message == rdj->message && rdi->from == rdj->from &&
+  if (isTermEqual (rdi->message, rdj->message) && 
-      rdi->to == rdj->to && rdi->label == rdj->label &&
+      isTermEqual (rdi->from, rdj->from) &&
+      isTermEqual (rdi->to, rdj->to) && 
+      isTermEqual (rdi->label, rdj->label) &&
       !(rdi->internal || rdj->internal))
     {
       if (rdi->type == SEND && rdj->type == READ)
@@ -53,6 +55,7 @@ events_match (const System sys, const int i, const int j)
  * g maps all labels in prec to the event indices for things already found,
  * or to LABEL_TODO for things not found yet but in prec, and LABEL_GOOD for well linked messages (and that have thus defined a runid for the corresponding role).
  * All values not in prec map to -1.
+ *@returns 1 iff the claim is allright, 0 iff it is violated.
  */
 int
 oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g)
@@ -129,19 +132,23 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g)
 	      Term rolename;
 	      Termmap gscan;
 
+	      /*
+	       * Two options: it is either involved or not
+	       */
+	      // 1. Assume that this run is not yet involved 
+	      result = oki_nisynch (sys, i-1, f, g);
+	      // 2. It is involved. Then either already used for this role, or will be now.
 	      rolename = sys->runs[rid].role->nameterm;
 	      rid2 = termmapGet (f, rolename);
-	      result = oki_nisynch (sys, i-1, f, g);
+	      if (rid2 == -1 || rid2 == rid)
-	      // Assume that this run is not yet involved 
+		{
+		  // Was not involved yet in a registerd way, or was the correct rid
 		  gscan = g;
-	      while (gscan != NULL)
+		  while (!result && gscan != NULL)
 		    {
 		      // Ordered match needed
 		      if (gscan->result > -1 && 
 			  events_match (sys, gscan->result, i) == 1)
-		    {
-		      // Events match: but is the run a good candidate?
-		      if (rid2 == -1 || rid2 == rid)
 			{
 			  Termmap fbuf, gbuf;
 
@@ -152,13 +159,13 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g)
 			  fbuf = termmapSet (fbuf, rolename, rid);
 			  gbuf = termmapDuplicate (g);
 			  gbuf = termmapSet (gbuf, rd->label, -3);
-			  result = oki_nisynch (sys, i-1, fbuf, gbuf);
+			  result = oki_nisynch (sys, i-1, fbuf, gbuf) || result;
 			  termmapDelete (gbuf);
 			  termmapDelete (fbuf);
 			}
-		    }
 		      gscan = gscan->next;
 		    }
+		}
 	      return result;
 	    }
 	  /*
@@ -174,20 +181,46 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g)
  */
 
 //! Check validity of ni-synch claim at event i.
+/**
+ *@returns 1 iff claim is true.
+ */
 int
 check_claim_nisynch (const System sys, const int i)
 {
+  Roledef rd;
   int result;
   int rid;
   Termmap f,g;
+  Term label;
+  Claimlist cl;
+  Termlist tl;
 
   rid = sys->traceRun[i];
+  rd = sys->traceEvent[i];
+  cl = rd->claiminfo;
+  cl->count++;
   f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid);
-  /**
+
-   *@todo g should map all labels in prec to LABEL_TODO
+  // map all labels in prec to LABEL_TODO
+  g = NULL;
+  label = rd->label;
+
+  tl = cl->prec;
+  while (tl != NULL)
+    {
+      g = termmapSet (g, tl->term, LABEL_TODO);
+      tl = tl->next;
+    }
+  /*
+   * Check claim
    */
-  result = oki_nisynch(sys, i, f, NULL);
+  result = oki_nisynch(sys, i, f, g);
+  if (!result)
+    {
+      cl->failed++;
+    }
   termmapDelete (f);
+  termmapDelete (g);
   return result;
 }
 

src/compiler.c

@@ -356,6 +356,7 @@ commEvent (int event, Tac tc)
       fromrole = tacTerm (trip);
       torole = tacTerm (trip->next);
       msg = tacTerm (tacTuple ((trip->next->next)));
+      cl = NULL;
 
       break;
     case CLAIM:
@@ -452,7 +453,7 @@ commEvent (int event, Tac tc)
     }
   /* and make that event */
   thisRole->roledef = roledefAdd (thisRole->roledef, event, label,
-				  fromrole, torole, msg);
+				  fromrole, torole, msg, cl);
 }
 
 int
@@ -1055,7 +1056,13 @@ compute_prec_sets (const System sys)
 void 
 preprocess (const System sys)
 {
+  /*
+   * init some counters
+   */
   sys->rolecount = compute_rolecount(sys);
   sys->roleeventmax = compute_roleeventmax(sys);
+  /*
+   * compute preceding label sets
+   */
   compute_prec_sets(sys);
 }

src/modelchecker.c

@@ -13,6 +13,7 @@
 #include "output.h"
 #include "tracebuf.h"
 #include "attackminimize.h"
+#include "claims.h"
 
 /*
 
@@ -1012,11 +1013,12 @@ claimViolationDetails (const System sys, const int run, const Roledef rd, const
   return NULL;
 }
 
-/* This happens when we violate a claim.
+//! A claim was violated.
+/**
+ * This happens when we violate a claim.
  * Lots of administration.
- * Returns true iff explorify is in order.
+ *@returns True iff explorify is in order.
  */
-
 int
 violateClaim (const System sys, int length, int claimev, Termlist reqt)
 {
@@ -1096,9 +1098,12 @@ executeTry (const System sys, int run)
 	    flag = send_basic (sys, run);
 	  return flag;
 	}
+
+      /*
+       * Execute claim event
+       */
       if (runPoint->type == CLAIM)
 	{
-
 	  /* first we might dynamically determine whether the claim is valid */
 	  if (untrustedAgent (sys, sys->runs[run].agents))
 	    {
@@ -1129,10 +1134,19 @@ executeTry (const System sys, int run)
 	      printf ("#%i\n", run);
 	    }
 #endif
+	  /*
+	   * update claim counters
+	   */
 	  sys->claims++;
 
+	  /*
+	   * distinguish claim types
+	   */
 	  if (runPoint->to == CLAIM_Secret)
 	    {
+	      /*
+	       * SECRECY
+	       */
 	      /* TODO claims now have their own type, test for that */
 	      /* TODO for now it is secrecy of the message */
 
@@ -1141,6 +1155,7 @@ executeTry (const System sys, int run)
 	      sys->secrets =
 		termlistAdd (termlistShallow (oldsecrets), runPoint->message);
 	      flag = claimSecrecy (sys, runPoint->message);
+              runPoint->claiminfo->count++;
 
 	      /* now check whether the claim failed for further actions */
 	      if (!flag)
@@ -1148,6 +1163,7 @@ executeTry (const System sys, int run)
 		  /* violation */
 		  Termlist tl;
 
+                  runPoint->claiminfo->failed++;
 		  tl = claimViolationDetails(sys,run,runPoint,sys->know);
 		  if (violateClaim (sys,sys->step+1, sys->step, tl ))
 		      flag = explorify (sys, run);
@@ -1165,7 +1181,23 @@ executeTry (const System sys, int run)
 	    }
 	  if (runPoint->to == CLAIM_Nisynch)
 	    {
-	      /* TODO nisynch implementation */
+	      /*
+	       * NISYNCH
+	       */
+	      //!@todo TODO nisynch implementation
+
+              flag = check_claim_nisynch (sys, sys->step);
+	      if (!flag)
+		{
+		  /* violation */
+		  if (violateClaim (sys,sys->step+1, sys->step, NULL ))
+		      flag = explorify (sys, run);
+		}
+	      else
+		{
+		  /* no violation */
+		  flag = explorify (sys, run);
+		}
 	    }
 	}
       /* a claim always succeeds */

src/runs.c

@@ -253,40 +253,6 @@ ensureValidRun (System sys, int run)
     }
 }
 
-//! Add a run event to the system
-/**
- *@param sys A system structure.
- *@param run The run identifier.
- *@param type The type of event.
- *@param label The event label.
- *@param from The sender.
- *@param to The recipient.
- *@param msg The message.
- *\sa READ,SEND,CLAIM
- */
-void
-runAdd (System sys, int run, int type, Term label, Term from, Term to,
-	Term msg)
-{
-  Roledef newEvent;
-  Roledef scan;
-
-  newEvent = roledefInit (type, label, from, to, msg);
-  ensureValidRun (sys, run);
-  if (runPointerGet (sys, run) == NULL)
-    {
-      sys->runs[run].start = newEvent;
-      runPointerSet (sys, run, newEvent);
-    }
-  else
-    {
-      scan = runPointerGet (sys, run);
-      while (scan->next != NULL)
-	scan = scan->next;
-      scan->next = newEvent;
-    }
-}
-
 //! Print a role event list.
 void
 roledefPrint (Roledef rd)
@@ -543,7 +509,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
     {
       Roledef rdnew;
 
-      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm);
+      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
       /* this is an internal action! */
       rdnew->internal = 1;
       rdnew->next = rd;
@@ -603,7 +569,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
  *@return A pointer to a new role event with the given parameters.
  */
 Roledef
-roledefInit (int type, Term label, Term from, Term to, Term msg)
+roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl)
 {
   Roledef newEvent;
 
@@ -616,6 +582,7 @@ roledefInit (int type, Term label, Term from, Term to, Term msg)
   newEvent->message = msg;
   newEvent->forbidden = NULL;	// no forbidden stuff
   newEvent->knowPhase = -1;	// we haven't explored any knowledge yet
+  newEvent->claiminfo = cl;	// only for claims
   newEvent->next = NULL;
   return newEvent;
 }
@@ -625,17 +592,17 @@ roledefInit (int type, Term label, Term from, Term to, Term msg)
  *\sa roledefInit()
  */
 Roledef
-roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg)
+roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl)
 {
   Roledef scan;
 
   if (rd == NULL)
-    return roledefInit (type, label, from, to, msg);
+    return roledefInit (type, label, from, to, msg, cl);
 
   scan = rd;
   while (scan->next != NULL)
     scan = scan->next;
-  scan->next = roledefInit (type, label, from, to, msg);
+  scan->next = roledefInit (type, label, from, to, msg, cl);
   return rd;
 }
 

src/runs.h

@@ -14,6 +14,28 @@
 #define runPointerGet(sys,run)		sys->runs[run].index
 #define runPointerSet(sys,run,newp)	sys->runs[run].index = newp
 
+//! 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;
+  int r;	//!< role number for mapping
+  int ev;	//!< event index in role
+  //! 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;
+
 //! Structure for a role event node or list.
 /**
  *\sa role
@@ -42,11 +64,20 @@ struct roledef
   //! Pointer to next roledef node.
   struct roledef *next;
 
+  /*
+   * Substructure for reads
+   */
   //! Illegal injections for this event.
   Knowledge forbidden;
   //! knowledge transitions counter.
   int knowPhase;
 
+  /*
+   * Substructure for claims
+   */
+  //! Pointer to claim type info
+  Claimlist claiminfo;
+
   /* evt runid for synchronisation, but that is implied in the
      base array */
 };
@@ -155,28 +186,6 @@ 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;
-  int r;	//!< role number for mapping
-  int ev;	//!< event index in role
-  //! 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
 {
@@ -259,8 +268,6 @@ void statesPrintShort (System sys);
 void systemDestroy (System sys);
 void systemDone (System sys);
 void ensureValidRun (System sys, int run);
-void runAdd (System sys, int run, int type, Term label, Term from, Term to,
-	     Term msg);
 void roledefPrint (Roledef rd);
 void runPrint (Roledef rd);
 void runsPrint (System sys);
@@ -272,9 +279,8 @@ void roledefDelete (Roledef rd);
 void roledefDestroy (Roledef rd);
 void roleInstance (const System sys, const Protocol protocol, const Role role,
 		   const Termlist tolist);
-Roledef roledefInit (int type, Term label, Term from, Term to, Term msg);
+Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl);
-Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
+Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl);
-		    Term msg);
 void systemStart (System sys);
 void indentActivate ();
 void indentSet (int i);