Added support for inequality tests.

There is a new event:

  not match(t1,t2)

where t1,t2 are terms.

They are implemented by using a special claim that simply stores the
intended inequality. The pruning theorems (prune_theorems.c) ensure that
these terms never become equal. If there are equal, the constraint is
violated. As long as they are not equal, there exists a solution using
groung terms such that their instantiation is not equal.

Currently not very efficient implemented and the graph out output is
also ugly for now.

Conflicts:
	gui/Scyther/Trace.py
	src/compiler.c
	src/scanner.l

src/claim.c

@@ -1436,5 +1436,9 @@ isClaimSignal (const Claimlist cl)
     {
       return true;
     }
+  if (isTermEqual (cl->type, CLAIM_Notequal))
+    {
+      return true;
+    }
   return false;
 }

src/compiler.c

@@ -817,6 +817,27 @@ matchEvent (Tac tc)
   markLastRoledef (thisRole->roledef, tc->lineno);
 }
 
+//! Parse a non-match event, and add role definitions for it
+/**
+ * Currently implemented by introducing a special claim.
+ *
+ * Claim(R,NotEqual,(pat,term) );
+ *
+ * This special claim, notequal, is later used for pruning.
+ */
+void
+nonMatchEvent (Tac tc)
+{
+  Term msg;
+  Term mpat;
+  Term mmsg;
+
+  mpat = tacTerm (tc->t1.tac);
+  mmsg = tacTerm (tc->t2.tac);
+  msg = makeTermTuple(mpat,mmsg);
+  claimCreate (sys, thisProtocol, thisRole, CLAIM_Notequal, NULL, msg, tc->lineno);
+}
+
 //! Parse a communication event tc of type event, and add a role definition event for it.
 void
 commEvent (int event, Tac tc)
@@ -1239,7 +1260,14 @@ roleCompile (Term nameterm, Tac tc)
 	    commEvent (SEND, tc);
 	    break;
 	  case TAC_MATCH:
+	    if (tc->t3.value == true)
+	      {
 	        matchEvent (tc);
+	      }
+	    else 
+	      {
+    	        nonMatchEvent (tc);
+	      }
 	    break;
 	  case TAC_CLAIM:
 	    commEvent (CLAIM, tc);

src/parser.y

@@ -58,6 +58,7 @@ int yylex(void);
 %token		KNOWS
 %token		TRUSTED
 %token 		MATCH
+%token 		NOT
 
 %type	<tac>	spdlcomplete
 %type	<tac>	spdlrep
@@ -204,6 +205,17 @@ event		: READT label '(' termlist ')' ';'
 		  	Tac t= tacCreate(TAC_MATCH);
 			t->t1.tac = $3;
 			t->t2.tac = $5;
+			t->t3.value = true;
+			$$ = t;
+		  }
+		| NOT MATCH '(' term ',' term ')' ';'
+		  {
+		  	/* first argument is pattern, second should be
+			 * ground term */
+		  	Tac t= tacCreate(TAC_MATCH);
+			t->t1.tac = $4;
+			t->t2.tac = $6;
+			t->t3.value = false;
 			$$ = t;
 		  }
 		| CLAIMT optlabel '(' termlist ')' ';'

src/prune_theorems.c

@@ -171,6 +171,69 @@ initiatorAgentsType (const System sys)
   return true;			// seems to be okay
 }
 
+//! Handle inequality constraints
+/**
+ * Currently, inequality constraints are encoded using "NotEqual" claims.
+ *
+ * Here we check that their arguments have not become equal. If they are not
+ * equal, there always exists a solution in which the values are different. The
+ * solution generated by the algorithm that grounds the trace (for
+ * visualisation) yields a compatible solution.
+ *
+ * Return true if okay - constraints can be met
+ * Return false if not okay - at least one constraint violated
+ *
+ * Note that this function performs its own proof output if needed.
+ * This allows it to pinpoint the exact constraint that is violated.
+ *
+ * Speed: this is certainly not the most efficient way to solve this. We are
+ * looping over all regular events, even if there are not negative constraints
+ * at all. Instead, we could simply collect a list of all negative constraints,
+ * which would speed up iterating over it.
+ */
+int
+inequalityConstraints (const System sys)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      if (sys->runs[run].protocol != INTRUDER)
+	{
+	  int e;
+	  Roledef rd;
+
+	  rd = sys->runs[run].start;
+          for (e = 0; e < sys->runs[run].step; e++)
+	    {
+	      if (rd->type == CLAIM)
+		{
+		  // It's a claim
+	          if (isTermEqual (rd->claiminfo->type, CLAIM_Notequal))
+		    {
+		      // TODO ASSERT: Message should be a pair for NotEqual claims
+		      if (isTermEqual (TermOp1(rd->message),TermOp2(rd->message)))
+			{
+			  // Inequality violated, no solution exists that makes them inequal anymore.
+			  if (switches.output == PROOF)
+			    {
+			      indentPrint ();
+			      eprintf ("Pruned because the pattern violates an inequality constraint based on the term ");
+			      termPrint (TermOp1(rd->message));
+			      eprintf (".\n");
+			    }
+
+			  return false;
+			}
+		    }
+		}
+	      rd = rd->next;
+	    }
+	}
+    }
+  return true;
+}
+
 //! Prune determination because of theorems
 /**
  * When something is pruned because of this function, the state space is still
@@ -366,6 +429,13 @@ so technically this is a bug. Don't use.
       }
   }
 
+  // Check for violation of inequality constraints
+  if (!inequalityConstraints (sys))
+    {
+      // Prune, because violated
+      return true;
+    }
+
   /*
    * Check for correct orderings involving local constants
    *

src/scanner.l

@@ -161,6 +161,7 @@ read		{ return READT; }
 recv		{ return RECVT; }
 send		{ return SENDT; }
 match		{ return MATCH; }
+not		{ return NOT; }
 var		{ return VAR; }
 const		{ return CONST; }
 fresh		{ return FRESH; }

src/specialterm.c

@@ -61,6 +61,7 @@ Term CLAIM_SID;
 Term CLAIM_SKR;
 Term CLAIM_Commit;
 Term CLAIM_Running;
+Term CLAIM_Notequal;
 
 Term AGENT_Alice;
 Term AGENT_Bob;
@@ -106,6 +107,7 @@ specialTermInit (const System sys)
   langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
   langcons (CLAIM_Empty, "Empty", TERM_Claim);
   langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
+  langcons (CLAIM_Notequal, "NotEqual", TERM_Claim);
 
   langcons (CLAIM_SID, "SID", TERM_Claim);	// claim specifying session ID
   langcons (CLAIM_SKR, "SKR", TERM_Claim);	// claim specifying session key : doubles as secrecy claim

src/specialterm.h

@@ -53,6 +53,7 @@ extern Term CLAIM_SID;
 extern Term CLAIM_SKR;
 extern Term CLAIM_Commit;
 extern Term CLAIM_Running;
+extern Term CLAIM_Notequal;
 
 extern Term AGENT_Alice;
 extern Term AGENT_Bob;