NEW: Added claims: Commit and Running.

There are two new claims:

  claim(X,Commit,t)  : check for agreement on data
  claim(X,Running,t) : signaling claim

The property checked is that each claim Commit needs to be preceded by a Running
with an identical term t.

Cherry-picked from commit 99a6be00e9d3d219ec73665607e8a3a7d65d04d1

src/claim.c

@@ -769,6 +769,54 @@ arachne_claim_weakagree (const System sys, const int claim_run,
     }
   return true;
 }
+
+//! Test commit(X) => running(X)
+int
+arachne_claim_commit (const System sys, const int claim_run,
+		      const int claim_index)
+{
+  /* Check whether preceded by a running with equal parameters */
+
+  int run;
+  Roledef rd_claim;
+
+  rd_claim = roledef_shift (sys->runs[claim_run].start, claim_index);
+  /*
+   * Iterate over all preceding events (include claim run for consistency with formal definition)
+   */
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      int ev;
+      Roledef rd;
+
+      rd = sys->runs[run].start;
+      for (ev = 0; ev < sys->runs[run].step; ev++)
+	{
+	  if (!isDependEvent (run, ev, claim_run, claim_index))
+	    {
+	      break;
+	    }
+	  /* so this event precedes */
+	  if (rd->type == CLAIM)
+	    {
+	      // Check for running signal/claim
+	      // (Check: maybe below can also be rd->to)
+	      if (isTermEqual (rd->claiminfo->type, CLAIM_Running))
+		{
+		  if (isTermEqual (rd->message, rd_claim->message))
+		    {
+		      // Claim holds
+		      return true;
+		    }
+		}
+	    }
+	  /* next */
+	  rd = rd->next;
+	}
+    }
+  return false;
+}
+
 //! Test aliveness
 int
 arachne_claim_alive (const System sys, const int claim_run,
@@ -910,6 +958,21 @@ prune_claim_specifics (const System sys)
 	  return 1;
 	}
     }
+  if (sys->current_claim->type == CLAIM_Commit)
+    {
+      if (arachne_claim_commit (sys, 0, sys->current_claim->ev))
+	{
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: 'commit => running' holds in this part of the proof tree.\n");
+	    }
+	  return 1;
+	}
+    }
   return 0;
 }
 
@@ -1325,5 +1388,9 @@ isClaimSignal (const Claimlist cl)
     {
       return true;
     }
+  if (isTermEqual (cl->type, CLAIM_Running))
+    {
+      return true;
+    }
   return false;
 }

src/specialterm.c

@@ -52,6 +52,8 @@ Term CLAIM_Empty;
 Term CLAIM_Reachable;
 Term CLAIM_SID;
 Term CLAIM_SKR;
+Term CLAIM_Commit;
+Term CLAIM_Running;
 
 Term AGENT_Alice;
 Term AGENT_Bob;
@@ -94,6 +96,9 @@ specialTermInit (const System sys)
   langcons (CLAIM_SID, "SID", TERM_Claim);	// claim specifying session ID
   langcons (CLAIM_SKR, "SKR", TERM_Claim);	// claim specifying session key : doubles as secrecy claim
 
+  langcons (CLAIM_Commit, "Commit", TERM_Claim);	// claim specifying session agreement for a subset of data items
+  langcons (CLAIM_Running, "Running", TERM_Claim);	// claim for signaling data item possession (checked by commit)
+
   /* Define default PKI using PK/SK/K */
   langcons (TERM_PK, "pk", TERM_Function);
   langcons (TERM_SK, "sk", TERM_Function);

src/specialterm.h

@@ -46,6 +46,8 @@ extern Term CLAIM_Empty;
 extern Term CLAIM_Reachable;
 extern Term CLAIM_SID;
 extern Term CLAIM_SKR;
+extern Term CLAIM_Commit;
+extern Term CLAIM_Running;
 
 extern Term AGENT_Alice;
 extern Term AGENT_Bob;