Added incompleteness marker for the untyped variables and MGDU set problem.

src/arachne.h

@@ -35,5 +35,6 @@ void arachneOutputAttack ();
 void printSemiState ();
 int countIntruderActions ();
 void role_name_print (const int run);
+void markNoFullProof ();
 
 #endif

src/mgu.c

@@ -26,6 +26,7 @@
 #include "debug.h"
 #include "specialterm.h"
 #include "switches.h"
+#include "arachne.h"
 
 /*
    Most General Unifier
@@ -569,6 +570,27 @@ termMguSubTerm (Term smallterm, Term bigterm,
 	      termDelete (keyneeded);
 	    }
 	}
+      else
+	{
+	  // The big term is a leaf
+	  /**
+	   * In this case we really need to consider the problematic Athena case for untyped variables.
+	   */
+	  if (isTermVariable (bigterm))
+	    {
+	      // Check the type: can it contain tuples, encryptions?
+	      if (isOpenVariable (bigterm))
+		{
+		  // This one needs to be pursued by further constraint adding
+		    /**
+		     * Currently, this is not implemented yet. TODO.
+		     * This is actually the main Athena problem that we haven't solved yet.
+		     */
+		  // Mark that we don't have a full proof.
+		  markNoFullProof ();
+		}
+	    }
+	}
       // simple clause or combined
       tl = termMguTerm (smallterm, bigterm);
       if (tl != MGUFAIL)

src/type.c

@@ -76,6 +76,16 @@ isTypelistGeneric (const Termlist typelist)
     }
 }
 
+//! Say whether this variable can contain tuples and/or encryptions
+/**
+ * Precondition: tvar should be a variable
+ */
+int
+isOpenVariable (const Term tvar)
+{
+  return isTypelistGeneric (tvar->stype);
+}
+
 //! Check whether a single variable term is instantiated correctly.
 /**
  * Check whether a single variable term is instantiated correctly in this

src/type.h

@@ -30,5 +30,6 @@ Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2);
 int checkAllSubstitutions (const System sys);
 int isAgentType (Termlist typelist);
 int goodAgentType (Term agent);
+int isOpenVariable(const Term tvar);
 
 #endif