- Totally untested. Otherwise, niagree should work ;)

src/claim.c

@@ -367,3 +367,63 @@ check_claim_nisynch (const System sys, const int i)
   return result;
 }
 
+//! Check validity of ni-agree claim at event i.
+/**
+ *@returns 1 iff claim is true.
+ *@todo This is now just a copy of ni-synch, should be fixed asap.
+ */
+int
+check_claim_niagree (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 = statesIncrease (cl->count);
+  f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid);
+
+  // 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, g);
+  if (!result)
+    {
+      cl->failed = statesIncrease (cl->failed);
+
+//#ifdef DEBUG 
+      warning ("Claim has failed!");
+      printf ("To be exact, claim label ");
+      termPrint (cl->label);
+      printf (" with prec set ");
+      termlistPrint (cl->prec);
+      printf ("\n");
+      printf ("i: %i\nf: ",i);
+      termmapPrint (f);
+      printf ("\ng: ");
+      termmapPrint (g);
+      printf ("\n");
+//#endif
+
+    }
+  termmapDelete (f);
+  termmapDelete (g);
+  return result;
+}
+

src/claim.h

@@ -2,5 +2,6 @@
 #define CLAIMS
 
 int check_claim_nisynch (const System sys, const int i);
+int check_claim_niagree (const System sys, const int i);
 
 #endif

src/compiler.c

@@ -53,6 +53,7 @@ Term TERM_Agent;
 Term TERM_Claim;
 Term CLAIM_Secret;
 Term CLAIM_Nisynch;
+Term CLAIM_Niagree;
 
 /*
  * Global stuff
@@ -103,6 +104,7 @@ compile (const System mysys, Tac tc, int maxrunsset)
 
   langcons (CLAIM_Secret, "Secret", TERM_Claim);
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
+  langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
 
   /* process the tac */
   tacProcess (tc);
@@ -443,6 +445,14 @@ commEvent (int event, Tac tc)
 	    }
 	  break;
 	}
+      if (claim == CLAIM_Niagree)
+	{
+	  if (n != 0)
+	    {
+	      error ("NIAGREE claim requires no parameters at line %i.", trip->next->lineno);
+	    }
+	  break;
+	}
 
       /* hmm, no handler yet */
 
@@ -985,6 +995,7 @@ compute_prec_sets (const System sys)
       Term t;
       Roledef rd;
       Term label;
+      int claim_index;
 
       label = cl->label;
       // Locate r,lev from label, requires (TODO) unique labeling of claims!
@@ -1017,7 +1028,7 @@ compute_prec_sets (const System sys)
        * Now we compute the preceding label set
        */
       cl->prec = NULL;		// clear first
-      i = index (r1,ev1);
+      claim_index = index (r1,ev1);
       r2 = 0;
       while (r2 < sys->rolecount)
 	{
@@ -1027,7 +1038,7 @@ compute_prec_sets (const System sys)
 	  rd = roledef_re (r2,ev2);
 	  while (rd != NULL)
 	    {
-	      if (prec[index2 (index (r2,ev2),i)] == 1)
+	      if (prec[index2 (index (r2,ev2),claim_index)] == 1)
 		{
 		  // This event precedes the claim
 		  
@@ -1042,6 +1053,12 @@ compute_prec_sets (const System sys)
 	    }
 	  r2++;
 	}
+      /**
+       * ---------------------------
+       * Distinguish types of claims
+       * ---------------------------
+       */
+
       // For ni-synch, the preceding label sets are added to the synchronising_labels sets.
       if (cl->type == CLAIM_Nisynch)
 	{
@@ -1050,13 +1067,57 @@ compute_prec_sets (const System sys)
 	  tl_scan = cl->prec;
 	  while (tl_scan != NULL)
 	    {
-	      if (!inTermlist (sys->synchronising_labels, tl_scan->term))
-		{
-		  sys->synchronising_labels = termlistAdd (sys->synchronising_labels, tl_scan->term);
-		}
+	      sys->synchronising_labels = termlistAddNew (sys->synchronising_labels, tl_scan->term);
 	      tl_scan = tl_scan->next;
 	    }
 	}
+
+      // For ni-agree, the preceding set is also important, but we furthermore need a restricted
+      // synchronising_labels set
+
+      //@todo Fix ni-agree synchronising label sets
+      if (cl->type == CLAIM_Niagree)
+	{
+	  int r_scan;
+
+	  // Scan each role (except the current one) and pick out the last prec events.
+	  r_scan = 0;
+	  while (r_scan < sys->rolecount)
+	    {
+	      // Only other roles
+	      if (r_scan != r1)
+		{
+		  // Scan fully
+		  int ev_scan;
+		  Term t_buf;
+
+		  t_buf = NULL;
+		  ev_scan = 0;
+		  while (ev_scan < sys->roleeventmax)
+		    {
+		      // if this event preceds the claim, replace the label term
+		      if (prec[index2 (index (r_scan, ev_scan), claim_index)] == 1)
+			{
+			  Roledef rd;
+
+	  		  rd = roledef_re (r_scan,ev_scan);
+			  if (rd->label != NULL)
+			    {
+			      t_buf = rd->label;
+			    }
+			}
+		      ev_scan++;
+		    }
+		  // Store only the last label
+		  if (t_buf != NULL)
+		    {
+		      sys->synchronising_labels = termlistAddNew(sys->synchronising_labels, t_buf);
+		    }
+		}
+	      r_scan++;
+	    }
+	}
+
 #ifdef DEBUG
       // Porparam = 100 (weirdness) [x][cc][debug] can turn of the synchronising label sets (override).
       if (sys->porparam == 100)

src/modelchecker.c

@@ -28,6 +28,7 @@
 
 extern Term CLAIM_Secret;
 extern Term CLAIM_Nisynch;
+extern Term CLAIM_Niagree;
 
 /*
    Some forward declarations.
@@ -1258,8 +1259,6 @@ executeTry (const System sys, int run)
 	      /*
 	       * NISYNCH
 	       */
-	      //!@todo TODO nisynch implementation
-
               flag = check_claim_nisynch (sys, sys->step);
 	      if (!flag)
 		{
@@ -1273,6 +1272,24 @@ executeTry (const System sys, int run)
 		  flag = explorify (sys, run);
 		}
 	    }
+	  if (runPoint->to == CLAIM_Niagree)
+	    {
+	      /*
+	       * NIAGREE
+	       */
+              flag = check_claim_niagree (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 */
       flag = 1;

src/termlist.c

@@ -220,7 +220,7 @@ termlistAppend (const Termlist tl, const Term term)
  * Mimics a basic set type behaviour.
  */
 Termlist
-termlistAddNew (const Termlist tl, const term t)
+termlistAddNew (const Termlist tl, const Term t)
 {
   if (inTermlist (tl, t))
       return tl;

src/termlist.h

@@ -32,7 +32,7 @@ __inline__ int inTermlist (Termlist tl, const Term term);
 int isTermlistEqual (Termlist tl1, Termlist tl2);
 Termlist termlistAdd (Termlist tl, Term term);
 Termlist termlistAppend (const Termlist tl, const Term term);
-Termlist termlistAddNew (const Termlist tl, const term t);
+Termlist termlistAddNew (const Termlist tl, const Term t);
 Termlist termlistConcat (Termlist tl1, Termlist tl2);
 Termlist termlistDelTerm (Termlist tl);
 Termlist termlistConjunct (Termlist tl1, Termlist tl2);