diff --git a/src/Makefile b/src/Makefile
new file mode 100644
index 0000000..48ae1d4
--- /dev/null
+++ b/src/Makefile
@@ -0,0 +1,80 @@
+#
+#	Scyther Makefile
+#
+
+#
+#	DEBUG or optimization settings: uncomment a single line:
+#
+CFLAGS = -g3 -D DEBUG		# default usage, for e.g. with valgrind
+#CFLAGS = -g3 -D DEBUG -pg	# for code profiling with gprof
+#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer
+
+#
+#	Compiler and linkage
+#
+CC = gcc
+# Note that these paths must include the path to the argtable library.
+CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall
+LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib
+LOADLIBS = -lfl
+LDLIBS = -largtable2
+OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS}
+
+#
+#	Module set for the modelchecker
+#
+MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \
+report.o debug.o  mgu.o substitutions.o \
+match_basic.o \
+match_clp.o constraints.o \
+output.o latex.o \
+varbuf.o tracebuf.o attackminimize.o \
+tac.o parser.o compiler.o 
+
+#
+#	Dependencies
+#
+MODELCHECKER = ${MODULES} main.o
+
+all:		scyther tags
+
+${Target}.o:	${Target}.c
+		$(CC) $(OPTIONS) ${Target}.c -c
+
+scanner.c:	scanner.lex
+		flex scanner.lex
+		cp lex.yy.c scanner.c
+
+tok.h:		parser.c
+
+parser.c:	parser.y
+		bison -d -v parser.y
+		cp parser.tab.c parser.c
+		cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h
+
+tags:		*.c *.h
+		ctags *.c *.h
+
+modules:	$(MODULES)
+
+scyther:	scanner.o $(MODELCHECKER)
+		$(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS)
+
+ptestmain.o scanner.o	: tok.h
+
+#
+#	Cleanup
+#
+clean:
+		rm -f *.o
+		rm -f scyther
+		rm -f scanner.c
+		rm -f parser.c
+		rm -f tok.h
+#
+#	Clean and rebuild: 'make new'
+#
+new:
+		make clean
+		make all
+
diff --git a/src/README b/src/README
new file mode 100644
index 0000000..bd00924
--- /dev/null
+++ b/src/README
@@ -0,0 +1,33 @@
+==================
+# Scyther README #
+==================
+
+----------------
+1. About Scyther
+----------------
+
+Scyther bla Cas andsoforth, bla Lutger, yada yada yada.
+
+---------------
+2. Requirements
+---------------
+
+Scyther compilation depends on a few external items:
+
+- A C compiler (gcc or anything modern *nixy will do)
+- The Flex and Bison scanner/compiler generation tools.
+- The argtable 2 library.
+
+The first two requirements are usually met by default by any modern *nix
+variant, such as GNU/Linux. 
+
+The argtable2 library is available under the LGPL license from
+http://argtable.sourceforge.net/doc/argtable2.html. Make sure the paths
+in the Makefile include the path to this library.
+
+If you want LaTeX output we need
+
+- LaTeX
+- The MSC macro package msc.sty
+- preamble.tex and postamble.tex
+
diff --git a/src/attackminimize.c b/src/attackminimize.c
new file mode 100644
index 0000000..220dc32
--- /dev/null
+++ b/src/attackminimize.c
@@ -0,0 +1,131 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "runs.h"
+#include "tracebuf.h"
+
+int cUnk = 0;
+int cTod = 0;
+
+void markback(System sys, struct tracebuf *tb, int ev)
+{
+	int run = tb->run[ev];
+
+	while (ev >= 0)
+	{
+		if (tb->run[ev] == run)
+		{
+			switch (tb->event[ev]->type)
+			{
+				case READ:
+					switch (tb->status[ev])
+					{
+						case S_UNK:
+							cUnk--;
+						case S_RED:
+							tb->status[ev] = S_TOD;
+							cTod++;
+							break;
+						case S_TOD:
+						case S_OKE:
+							break;
+					}
+					break;
+				case SEND:
+				case CLAIM:
+					if (tb->status[ev] == S_UNK)
+					{
+					    cUnk--;
+					}
+					tb->status[ev] = S_OKE;
+					break;
+			}
+		}
+		ev--;
+	}
+}
+
+void attackMinimize(System sys, struct tracebuf *tb)
+{
+	int i;
+	int j;
+
+	cUnk = 0;
+	cTod = 0;
+
+	for (i=0; i < tb->length; i++)
+	{
+		switch (tb->status[i])
+		{
+		case S_UNK:
+		    cUnk++;
+		    break;
+		case S_TOD:
+		    cTod++;
+		    break;
+		default:
+		    break;
+		}
+	}
+	
+	markback(sys, tb, tb->violatedclaim);
+
+	while (cUnk + cTod > 0)
+	{
+		while (cTod > 0)
+		{
+			for (i = 0; i < tb->length; i++)
+				// kies een i; laten we de eerste maar pakken
+			{
+				if (tb->status[i] == S_TOD)
+					break;
+			}
+			if (i == tb->length)
+			  {
+			        printf("Some step error.\n");
+				exit(1);
+			  }
+			
+			j = i;
+			while (j >= 0 && inKnowledge(tb->know[j], tb->event[i]->message))
+			{
+			    // zoek waar m in de kennis komt
+			    j--;
+			}
+			tb->status[i] = S_OKE;
+			cTod--;
+			if (j>=0)
+			{
+			    markback(sys,tb,j);
+			}
+		}
+		while (cTod == 0 && cUnk > 0)
+		{
+			for (i = tb->length-1; i>=0; i--)
+				// pak laatste i
+			{
+				if (tb->status[i] == S_UNK)
+					break;
+			}
+			if (i < 0)
+			  {
+			        printf("Some i<0 error.\n");
+				exit(1);
+			  }
+			
+			tb->status[i] = S_RED;
+			cUnk--;
+			tb->reallength--;
+
+			j = tracebufRebuildKnow(tb);
+			if (j>-1)
+			{
+			  	tb->reallength++;
+				markback(sys,tb,i);
+				if (j < tb->length)
+				{
+					tb->link[j] = (tb->link[j] > i ? tb->link[j] : i);
+				}
+			}
+		}
+	}
+}
diff --git a/src/attackminimize.h b/src/attackminimize.h
new file mode 100644
index 0000000..5d0e8f8
--- /dev/null
+++ b/src/attackminimize.h
@@ -0,0 +1 @@
+void attackMinimize(System sys, struct tracebuf *tb);
diff --git a/src/cetest-cm.sh b/src/cetest-cm.sh
new file mode 100755
index 0000000..6ec0a61
--- /dev/null
+++ b/src/cetest-cm.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+#
+# Test conform ce stuff, but our version
+#
+./scyther -r5 $* <spdl/bkepk.spdl
+./scyther -r6 $* <spdl/bkepk.spdl | tail -n 1
diff --git a/src/cetest.sh b/src/cetest.sh
new file mode 100755
index 0000000..e77e43d
--- /dev/null
+++ b/src/cetest.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+#
+# Test conform ce stuff.
+#
+./scyther -r6 $* <spdl/bkepk-ce.spdl
+./scyther -r7 $* <spdl/bkepk-ce.spdl | tail -n 1
+./scyther -r8 $* <spdl/bkepk-ce.spdl | tail -n 1
+./scyther -r7 $* <spdl/bkepk-ce2.spdl | tail -n 1
+./scyther -r8 $* <spdl/bkepk-ce2.spdl | tail -n 1
+./scyther -r9 $* <spdl/bkepk-ce2.spdl | tail -n 1
diff --git a/src/compiler.c b/src/compiler.c
new file mode 100644
index 0000000..b890fdc
--- /dev/null
+++ b/src/compiler.c
@@ -0,0 +1,732 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "tac.h"
+#include "terms.h"
+#include "termlists.h"
+#include "runs.h"
+#include "knowledge.h"
+#include "symbols.h"
+#include "substitutions.h"
+#include "compiler.h"
+
+/*
+   Simple sys pointer as a global. Yields cleaner code although it's against programming standards.
+   It is declared as static to hide it from the outside world, and to indicate its status.
+   Other modules will just see a nicely implemented sys parameter of compile, so we can always change
+   it later if somebody complains. Which they won't.
+*/
+
+static System sys;
+
+/*
+   Forward declarations.
+*/
+
+void tacProcess (Tac tc);
+void levelInit (void);
+void levelDone (void);
+Term symbolDeclare (Symbol s, int isVar);
+void levelTacDeclaration (Tac tc, int isVar);
+Term levelFind (Symbol s, int i);
+Term symbolFind (Symbol s);
+Term tacTerm (Tac tc);
+Termlist tacTermlist (Tac tc);
+
+#define	levelDeclareVar(s)	levelTacDeclaration(s,1)
+#define	levelDeclareConst(s)	levelTacDeclaration(s,0)
+#define	levelVar(s)	symbolDeclare(s,1)
+#define	levelConst(s)	symbolDeclare(s,0)
+
+/* externally used:
+ * TERM_Function in termlists.c for inversekeys
+ * TERM_Type in runs.c for type determination.
+ */
+
+Term TERM_Agent;
+Term TERM_Function;
+Term TERM_Hidden;
+Term TERM_Type;
+Term TERM_Nonce;
+Term TERM_Agent;
+
+Term TERM_Claim;
+Term CLAIM_Secret;
+Term CLAIM_Nisynch;
+
+/*
+ * Global stuff
+ */
+
+#define MAXLEVELS 3
+static Termlist leveltl[MAXLEVELS];
+static int level;
+static int maxruns;
+static Protocol thisProtocol;
+static Role thisRole;
+
+/* ------------------------------------------------------------------- */
+
+/*
+   Compile the tac into the system
+*/
+
+void
+compile (System mysys, Tac tc, int maxrunsset)
+{
+  int i;
+
+  /* Init globals */
+  maxruns = maxrunsset;
+  /* transfer to global static variable */
+  sys = mysys;
+  /* init levels */
+  for (i = 0; i < MAXLEVELS; i++)
+    leveltl[i] = NULL;
+  level = -1;
+  levelInit ();
+
+  /* Init system constants */
+#define langhide(x,y) x = levelConst(symbolSysConst(" _" y "_ "))
+#define langtype(x,y) x->stype = termlistAdd(x->stype,y);
+#define langcons(x,y,z) x = levelConst(symbolSysConst(y)); langtype(x,z)
+
+  langhide (TERM_Type, "Type");
+  langhide (TERM_Hidden, "Hidden");
+  langhide (TERM_Claim, "Claim");
+
+  langcons (TERM_Agent, "Agent", TERM_Type);
+  langcons (TERM_Function, "Function", TERM_Type);
+  langcons (TERM_Nonce, "Nonce", TERM_Type);
+
+  langcons (CLAIM_Secret, "Secret", TERM_Claim);
+  langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
+
+  /* process the tac */
+  tacProcess (tc);
+
+  /* cleanup */
+  levelDone ();
+}
+
+void
+errorTac (int lineno)
+{
+  printf (" on line %i.\n", lineno);
+  exit (1);
+}
+
+void
+levelInit (void)
+{
+  level++;
+  if (level >= MAXLEVELS)
+    {
+      printf ("ERROR: level is increased too much\n");
+      exit (1);
+    }
+  leveltl[level] = NULL;
+}
+
+void
+levelDone (void)
+{
+  if (level < 0)
+    {
+      printf ("ERROR: level is increased too much\n");
+      exit (1);
+    }
+  leveltl[level] = NULL;
+  level--;
+}
+
+Term
+levelDeclare (Symbol s, int isVar, int level)
+{
+  Term t;
+
+  t = levelFind (s, level);
+  if (t == NULL)
+    {
+      /* new! */
+      if (isVar)
+	{
+	  t = makeTermType (VARIABLE, s, -(level + 1));
+	  sys->variables = termlistAdd (sys->variables, t);
+	}
+      else
+	{
+	  t = makeTermType (GLOBAL, s, -(level + 1));
+	}
+      leveltl[level] = termlistAdd (leveltl[level], t);
+
+      /* add to relevant list */
+      switch (level)
+	{
+	case 0:
+	  sys->locals = termlistAdd (sys->locals, t);
+	  break;
+	case 1:
+	  thisProtocol->locals = termlistAdd (thisProtocol->locals, t);
+	  break;
+	case 2:
+	  thisRole->locals = termlistAdd (thisRole->locals, t);
+	  break;
+	}
+    }
+  return t;
+}
+
+Term
+symbolDeclare (Symbol s, int isVar)
+{
+  return levelDeclare (s, isVar, level);
+}
+
+Term
+levelFind (Symbol s, int level)
+{
+  Termlist tl;
+
+  tl = leveltl[level];
+  while (tl != NULL)
+    {
+      if (isTermLeaf (tl->term))
+	{
+	  if (tl->term->symb == s)
+	    {
+	      return tl->term;
+	    }
+	}
+      tl = tl->next;
+    }
+  return NULL;
+}
+
+Term
+symbolFind (Symbol s)
+{
+  int i;
+  Term t;
+
+  i = level;
+  while (i >= 0)
+    {
+      t = levelFind (s, i);
+      if (t != NULL)
+	return t;
+      i--;
+    }
+  return NULL;
+}
+
+void
+defineUsertype (Tac tcdu)
+{
+  Tac tc;
+  Term t;
+  Term tfind;
+
+  tc = tcdu->tac1;
+
+  if (tc == NULL)
+    {
+      printf ("ERROR: empty usertype declaration.\n");
+      errorTac (tcdu->lineno);
+    }
+  while (tc != NULL && tc->op == TAC_STRING)
+    {
+      /* check whether this term is already declared in the same way
+       * (i.e. as a type) */
+
+      tfind = levelFind (tc->sym1, 0);
+      if (tfind == NULL)
+	{
+	  /* this is what we expected: this type is not declared yet */
+	  t = levelDeclare (tc->sym1, 0, 0);
+	  t->stype = termlistAdd (NULL, TERM_Type);
+	}
+      else
+	{
+	  /* oi!, there's already one. Let's hope is is a type too. */
+	  if (inTermlist (tfind->stype, TERM_Type))
+	    {
+	      /* phew. warn anyway */
+	      printf ("WARNING: double declaration of usertype ");
+	      termPrint (tfind);
+	      printf ("\n");
+	    }
+	  else
+	    {
+	      /* that's not right! */
+	      printf ("ERROR: conflicting definitions for ");
+	      termPrint (tfind);
+	      printf (" in usertype definition ");
+	      errorTac (tc->lineno);
+	    }
+	}
+      tc = tc->next;
+    }
+}
+
+void
+levelTacDeclaration (Tac tc, int isVar)
+{
+  Tac tscan;
+  Termlist typetl = NULL;
+  Term t;
+
+  tscan = tc->tac2;
+  if (!isVar && tscan->next != NULL)
+    {
+      printf ("ERROR: Multiple types not allowed for constants ");
+      errorTac (tscan->lineno);
+    }
+  while (tscan != NULL && tscan->op == TAC_STRING)
+    {
+      /* apparently there is type info, termlist? */
+      t = levelFind (tscan->sym1, 0);
+
+      if (t == NULL)
+	{
+	  /* not declared, that is unacceptable. */
+	  printf ("ERROR: type ");
+	  symbolPrint (tscan->sym1);
+	  printf (" was not declared ");
+	  errorTac (tscan->lineno);
+	}
+      else
+	{
+	  if (!inTermlist (t->stype, TERM_Type))
+	    {
+	      printf ("ERROR: non-type constant in type declaration ");
+	      errorTac (tscan->lineno);
+	    }
+	}
+      typetl = termlistAdd (typetl, t);
+      tscan = tscan->next;
+    }
+  /* parse all constants and vars */
+  tscan = tc->tac1;
+  while (tscan != NULL)
+    {
+      t = symbolDeclare (tscan->sym1, isVar);
+      t->stype = typetl;
+      tscan = tscan->next;
+    }
+}
+
+void
+commEvent (int event, Tac tc)
+{
+  /* Add an event to the roledef, send or read */
+  Term fromrole = NULL;
+  Term torole = NULL;
+  Term msg = NULL;
+  Term label = NULL;
+  Term claim = NULL;
+  Term claimbig = NULL;
+  int n = 0;
+  Tac trip;
+
+  /* Construct label, if any */
+  if (tc->sym1 == NULL)
+    {
+      label = NULL;
+    }
+  else
+    {
+      label = levelFind (tc->sym1, level - 1);
+      if (label == NULL)
+	{
+	  /* effectively, labels are bound to the protocol */
+	  level--;
+	  label = levelConst (tc->sym1);
+	  level++;
+	}
+    }
+  trip = tc->tac2;
+  switch (event)
+    {
+    case READ:
+    case SEND:
+      /* now parse triplet info */
+      if (trip == NULL || trip->next == NULL || trip->next->next == NULL)
+	{
+	  printf ("ERROR in %i event ", event);
+	  errorTac (tc->lineno);
+	}
+      fromrole = tacTerm (trip);
+      torole = tacTerm (trip->next);
+      msg = tacTerm (tacTuple ((trip->next->next)));
+
+      break;
+    case CLAIM:
+      /* now parse tuple info */
+      if (trip == NULL || trip->next == NULL)
+	{
+	  printf ("ERROR in %i event ", event);
+	  errorTac (tc->lineno);
+	}
+      fromrole = tacTerm (trip);
+      claimbig = tacTerm (tacTuple ((trip->next)));
+      /* check for several types */
+      claim = tupleProject (claimbig, 0);
+      torole = claim;
+      /* check for obvious flaws */
+      if (claim == NULL)
+	{
+	  printf ("ERROR: invalid claim specification ");
+	  errorTac (trip->next->lineno);
+	}
+      if (!inTermlist (claim->stype, TERM_Claim))
+	{
+	  printf ("ERROR: unknown claim type ");
+	  termPrint (claim);
+	  errorTac (trip->next->lineno);
+	}
+      /* unfold parameters to msg */
+      msg = NULL;
+      n = tupleCount (claimbig) - 1;
+      if (n < 1)
+	{
+	  /* no parameters */
+	  n = 0;
+	}
+      else
+	{
+	  /* n parameters */
+	  msg = deVar (claimbig)->op2;
+	  if (tupleCount (msg) != n)
+	    {
+	      printf
+		("ERROR: something went wrong in the claim tuple parameter unfolding ");
+	      errorTac (trip->next->lineno);
+	    }
+	}
+
+      /* handles all claim types differently */
+
+      if (claim == CLAIM_Secret)
+	{
+	  if (n == 0)
+	    {
+	      printf
+		("ERROR: secrecy claim requires a list of terms to be secret ");
+	      errorTac (trip->next->lineno);
+	    }
+	  break;
+	}
+      if (claim == CLAIM_Nisynch)
+	{
+	  if (n != 0)
+	    {
+	      printf ("ERROR: nisynch claim has no parameters ");
+	      errorTac (trip->next->lineno);
+	    }
+	  break;
+	}
+
+      /* hmm, no handler yet */
+
+      printf ("ERROR: No know handler for this claim type: ");
+      termPrint (claim);
+      printf (" ");
+      errorTac (trip->next->lineno);
+      break;
+    }
+  /* and make that event */
+  thisRole->roledef = roledefAdd (thisRole->roledef, event, label,
+				  fromrole, torole, msg);
+}
+
+int
+normalDeclaration (Tac tc)
+{
+  switch (tc->op)
+    {
+    case TAC_VAR:
+      levelDeclareVar (tc);
+      if (level < 2 && tc->tac3 == NULL)
+	knowledgeAddTermlist (sys->know, tacTermlist (tc->tac1));
+      break;
+    case TAC_CONST:
+      levelDeclareConst (tc);
+      if (level < 2 && tc->tac3 == NULL)
+	knowledgeAddTermlist (sys->know, tacTermlist (tc->tac1));
+      break;
+    case TAC_SECRET:
+      levelDeclareConst (tc);
+      break;
+    case TAC_COMPROMISED:
+      knowledgeAddTermlist (sys->know, tacTermlist (tc->tac1));
+      break;
+    case TAC_INVERSEKEYS:
+      knowledgeAddInverse (sys->know, tacTerm (tc->tac1), tacTerm (tc->tac2));
+      break;
+    default:
+      /* abort with false */
+      return 0;
+    }
+  return 1;
+}
+
+void
+roleCompile (Term nameterm, Tac tc)
+{
+  Role r;
+
+  /* make new (empty) current protocol with name */
+  r = roleCreate (nameterm);
+  thisRole = r;
+  /* add protocol to list */
+  r->next = thisProtocol->roles;
+  thisProtocol->roles = r;
+
+  /* parse the content of the role */
+  levelInit ();
+
+  while (tc != NULL)
+    {
+      switch (tc->op)
+	{
+	case TAC_READ:
+	  commEvent (READ, tc);
+	  break;
+	case TAC_SEND:
+	  commEvent (SEND, tc);
+	  break;
+	case TAC_CLAIM:
+	  commEvent (CLAIM, tc);
+	  break;
+	default:
+	  if (!normalDeclaration (tc))
+	    {
+	      printf ("ERROR: illegal command %i in role ", tc->op);
+	      termPrint (thisRole->nameterm);
+	      printf (" ");
+	      errorTac (tc->lineno);
+	    }
+	  break;
+	}
+      tc = tc->next;
+    }
+  levelDone ();
+}
+
+void
+runInstanceCreate (Tac tc)
+{
+  /* create an instance of an existing role
+   * tac1 is the dot-separated reference to the role.
+   * tac2 is the list of parameters to be filled in.
+   */
+
+  Protocol p;
+  Role r;
+  Symbol psym, rsym;
+  Termlist instParams;
+
+  /* check whether we can still do it */
+  if (sys->maxruns >= maxruns)
+    return;
+
+  /* first, locate the protocol */
+  psym = tc->tac1->sym1;
+  p = sys->protocols;
+  while (p != NULL && p->nameterm->symb != psym)
+    p = p->next;
+  if (p == NULL)
+    {
+      printf ("Trying to create a run of a non-declared protocol ");
+      symbolPrint (psym);
+      printf (" ");
+      errorTac (tc->lineno);
+    }
+
+  /* locate the role */
+  rsym = tc->tac1->sym2;
+  r = p->roles;
+  while (r != NULL && r->nameterm->symb != rsym)
+    r = r->next;
+  if (r == NULL)
+    {
+      printf ("Protocol ");
+      symbolPrint (psym);
+      printf (" has no role called ");
+      symbolPrint (rsym);
+      printf (" ");
+      errorTac (tc->lineno);
+    }
+
+  /* we now know what we are instancing, equal numbers? */
+  instParams = tacTermlist (tc->tac2);
+  if (termlistLength (instParams) != termlistLength (p->rolenames))
+    {
+      printf
+	("Run instance has different number of parameters than protocol ");
+      termPrint (p->nameterm);
+      printf (" ");
+      errorTac (tc->lineno);
+    }
+
+  /* equal numbers, so it seems to be safe */
+  roleInstance (sys, p, r, instParams);
+
+  /* after creation analysis */
+  /* AC1: untrusted agents */
+  /*      first: determine whether the run is untrusted,
+   *      by checking whether one of the untrusted agents occurs
+   *      in the run instance  */
+  if (untrustedAgent (sys, instParams))
+    {
+      /* nothing yet */
+      /* claims handle this themselves */
+
+      /* some reduction might be possible, by cutting of the last few actions
+       * of such an untrusted run */
+
+      /* but most of it might be handled dynamically */
+    }
+
+  /* AC2: originator assumption for CLP ? */
+  /* TODO */
+}
+
+void
+protocolCompile (Symbol prots, Tac tc, Tac tcroles)
+{
+  Protocol pr;
+  Term t;
+
+  if (levelFind (prots, level) != NULL)
+    {
+      printf ("ERROR: Double declaration of protocol ");
+      symbolPrint (prots);
+      printf (" ");
+      errorTac (tc->lineno);
+    }
+  /* make new (empty) current protocol with name */
+  pr = protocolCreate (levelConst (prots));
+  thisProtocol = pr;
+  /* add protocol to list */
+  pr->next = sys->protocols;
+  sys->protocols = pr;
+
+  levelInit ();
+  /* add the role names */
+  pr->rolenames = NULL;
+  while (tcroles != NULL)
+    {
+      pr->rolenames =
+	termlistAppend (pr->rolenames, levelConst (tcroles->sym1));
+      tcroles = tcroles->next;
+    }
+
+  /* parse the content of the protocol */
+  while (tc != NULL)
+    {
+      switch (tc->op)
+	{
+	case TAC_UNTRUSTED:
+	  sys->untrusted =
+	    termlistConcat (sys->untrusted, tacTermlist (tc->tac1));
+	  break;
+	case TAC_ROLE:
+	  t = levelFind (tc->sym1, level);
+	  if (t != NULL)
+	    {
+	      roleCompile (t, tc->tac2);
+	    }
+	  else
+	    {
+	      printf ("ERROR: undeclared role ");
+	      symbolPrint (tc->sym1);
+	      printf (" in protocol ");
+	      termPrint (pr->nameterm);
+	      errorTac (tc->sym1->lineno);
+	    }
+	  break;
+	default:
+	  if (!normalDeclaration (tc))
+	    {
+	      printf ("ERROR: illegal command %i in protocol ", tc->op);
+	      termPrint (thisProtocol->nameterm);
+	      errorTac (tc->lineno);
+	    }
+	  break;
+	}
+      tc = tc->next;
+    }
+  levelDone ();
+}
+
+void
+tacProcess (Tac tc)
+{
+  while (tc != NULL)
+    {
+      switch (tc->op)
+	{
+	case TAC_PROTOCOL:
+	  protocolCompile (tc->sym1, tc->tac2, tc->tac3);
+	  break;
+	case TAC_UNTRUSTED:
+	  sys->untrusted =
+	    termlistConcat (sys->untrusted, tacTermlist (tc->tac1));
+	  break;
+	case TAC_RUN:
+	  runInstanceCreate (tc);
+	  break;
+	case TAC_USERTYPE:
+	  defineUsertype (tc);
+	  break;
+	default:
+	  if (!normalDeclaration (tc))
+	    {
+	      printf ("ERROR: illegal command %i at the global level.\n",
+		      tc->op);
+	      errorTac (tc->lineno);
+	    }
+	  break;
+	}
+      tc = tc->next;
+    }
+}
+
+Term
+tacTerm (Tac tc)
+{
+  switch (tc->op)
+    {
+    case TAC_ENCRYPT:
+      return makeTermEncrypt (tacTerm (tc->tac1), tacTerm (tc->tac2));
+    case TAC_TUPLE:
+      return makeTermTuple (tacTerm (tc->tac1), tacTerm (tc->tac2));
+    case TAC_STRING:
+      {
+	Term t = symbolFind (tc->sym1);
+	if (t == NULL)
+	  {
+	    printf ("Undeclared symbol ");
+	    symbolPrint (tc->sym1);
+	    errorTac (tc->lineno);
+	  }
+	return t;
+      }
+    default:
+      return NULL;
+    }
+}
+
+Termlist
+tacTermlist (Tac tc)
+{
+  Termlist tl = NULL;
+
+  while (tc != NULL)
+    {
+      tl = termlistAppend (tl, tacTerm (tc));
+      tc = tc->next;
+    }
+  return tl;
+}
diff --git a/src/compiler.h b/src/compiler.h
new file mode 100644
index 0000000..837aa93
--- /dev/null
+++ b/src/compiler.h
@@ -0,0 +1,6 @@
+#ifndef COMPILER
+#define COMPILER
+
+void compile (System sys, Tac tc, int maxruns);
+
+#endif
diff --git a/src/constraints.c b/src/constraints.c
new file mode 100644
index 0000000..8066345
--- /dev/null
+++ b/src/constraints.c
@@ -0,0 +1,336 @@
+#include <stdio.h>
+#include "memory.h"
+#include "constraints.h"
+#include "debug.h"
+#include "runs.h"
+
+
+
+/* constraints currently are shallow copies */
+
+Constraint
+makeConstraint (Term term, Knowledge know)
+{
+  /* maybe knowDup can just be a link, but then it needs to be moved from destroy as well */
+  Constraint co = memAlloc (sizeof (struct constraint));
+  co->term = term;
+  //co->know = knowledgeDuplicate(know);
+  co->know = know;
+  return co;
+}
+
+
+Constraint
+constraintDuplicate (Constraint co)
+{
+  return makeConstraint (co->term, co->know);
+}
+
+
+void
+constraintDestroy (Constraint cons)
+{
+  //knowledgeDelete(cons->know);
+  if (cons != NULL)
+    memFree (cons, sizeof (struct constraint));
+}
+
+/* constraints are typically added at the end, to maintain the order in which they were added */
+
+Constraintlist
+constraintlistAdd (Constraintlist cl, Constraint co)
+{
+  Constraintlist clnew = memAlloc (sizeof (struct constraintlist));
+
+  clnew->constraint = co;
+  clnew->next = NULL;
+  if (cl == NULL)
+    {
+      clnew->prev = NULL;
+      return clnew;
+    }
+  else
+    {
+      Constraintlist scan;
+
+      scan = cl;
+      while (scan->next != NULL)
+	scan = scan->next;
+      scan->next = clnew;
+      clnew->prev = scan;
+      return cl;
+    }
+}
+
+Constraintlist
+constraintlistConcat (Constraintlist cl1, Constraintlist cl2)
+{
+  Constraintlist scan;
+
+  if (cl1 == NULL)
+    return cl2;
+  scan = cl1;
+  while (scan->next != NULL)
+    scan = scan->next;
+  scan->next = cl2;
+  return cl1;
+}
+
+Constraintlist
+constraintlistRewind (Constraintlist cl)
+{
+  if (cl == NULL)
+    return NULL;
+  while (cl->prev != NULL)
+    cl = cl->prev;
+  return cl;
+}
+
+
+Constraintlist
+constraintlistInsert (Constraintlist cl, Term term, Knowledge know)
+{
+  Constraintlist clnew = memAlloc (sizeof (struct constraintlist));
+
+  clnew->constraint = makeConstraint (term, know);
+  if (cl != NULL)
+    {
+      if (cl->next != NULL)
+	{
+	  clnew->next = cl->next;
+	  cl->next->prev = cl;
+	}
+      else
+	{
+	  clnew->next = NULL;
+	}
+      clnew->prev = cl;
+      cl->next = clnew;
+      return constraintlistRewind (cl);
+    }
+  else
+    {
+      clnew->next = NULL;
+      clnew->prev = NULL;
+      return clnew;
+    }
+}
+
+/* unlink a single constraint */
+
+Constraintlist
+constraintlistUnlink (Constraintlist cl)
+{
+  Constraintlist clnext, clprev;
+
+  if (cl == NULL)
+    return NULL;
+  clprev = cl->prev;
+  clnext = cl->next;
+
+  if (clnext != NULL)
+    {
+      clnext->prev = clprev;
+      cl->next = NULL;
+    }
+  if (clprev != NULL)
+    {
+      clprev->next = clnext;
+      cl->prev = NULL;
+      return constraintlistRewind (clprev);
+    }
+  else
+    {
+      return clnext;
+    }
+}
+
+
+/* remove a single constraint */
+
+Constraintlist
+constraintlistRemove (Constraintlist cl)
+{
+  Constraintlist clnew;
+
+  clnew = constraintlistUnlink (cl);
+  memFree (cl, sizeof (struct constraintlist));
+  return clnew;
+}
+
+/* remove all constraints from this point onwards */
+
+void
+constraintlistDelete (Constraintlist cl)
+{
+  Constraintlist cldel;
+
+  /* no empty cl */
+  if (cl == NULL)
+    return;
+
+  /* cut off previous */
+  if (cl->prev != NULL)
+    {
+      /* TODO maybe this should cause a warning? */
+      printf ("WARNING: clDelete with non-empty prev\n");
+      cl->prev->next = NULL;
+    }
+  while (cl != NULL)
+    {
+      cldel = cl;
+      cl = cl->next;
+      memFree (cldel, sizeof (struct constraintlist));
+    }
+  return;
+}
+
+void
+constraintlistDestroy (Constraintlist cl)
+{
+  Constraintlist cldel;
+
+  /* no empty cl */
+  if (cl == NULL)
+    return;
+
+  /* cut off previous */
+  if (cl->prev != NULL)
+    {
+      /* TODO maybe this should cause a warning? */
+      printf ("WARNING: clDestroy with non-empty prev\n");
+      cl->prev = NULL;
+    }
+  while (cl != NULL)
+    {
+      cldel = cl;
+      cl = cl->next;
+      constraintDestroy (cldel->constraint);
+      memFree (cldel, sizeof (struct constraintlist));
+    }
+}
+
+
+Constraintlist
+constraintlistDuplicate (Constraintlist oldcl)
+{
+  Constraintlist newcl = NULL;
+
+  while (oldcl != NULL)
+    {
+      newcl =
+	constraintlistAdd (newcl, constraintDuplicate (oldcl->constraint));
+      oldcl = oldcl->next;
+    }
+  return newcl;
+}
+
+Constraintlist
+constraintlistShallow (Constraintlist oldcl)
+{
+  Constraintlist newcl = NULL;
+
+  while (oldcl != NULL)
+    {
+      newcl = constraintlistAdd (newcl, oldcl->constraint);
+      oldcl = oldcl->next;
+    }
+  return newcl;
+}
+
+/* ----------------------------------------------------------
+
+   Print stuff
+
+---------------------------------------------------------- */
+
+void
+constraintPrint (Constraint co)
+{
+  indent ();
+  printf ("Constraint ");
+  if (co == NULL)
+    {
+      printf ("[empty]\n");
+      return;
+    }
+  termPrint (co->term);
+  printf (" :\n");
+  knowledgePrint (co->know);
+}
+
+void
+constraintlistPrint (Constraintlist cl)
+{
+  if (cl == NULL)
+    {
+      indent ();
+      printf ("[empty constraintlist]\n");
+      return;
+    }
+  while (cl != NULL)
+    {
+      constraintPrint (cl->constraint);
+      cl = cl->next;
+    }
+}
+
+
+/* ----------------------------------------------------------
+
+   Now some real logic for the constraints
+
+---------------------------------------------------------- */
+
+/* eliminate all standalone variables */
+
+void
+msElim (Constraint co)
+{
+  Termlist tl;
+
+  /* simple variables can only exist in basic */
+  if (co->know == NULL)
+    {
+#ifdef DEBUG
+      debug (5, "Exiting because co->know is empty.");
+#endif
+    }
+  else
+    {
+      tl = co->know->basic;
+      while (tl != NULL)
+	{
+	  if (isTermVariable (tl->term))
+	    {
+	      tl = termlistDelTerm (tl);
+	      co->know->basic = tl;
+	    }
+	  else
+	    tl = tl->next;
+	}
+    }
+}
+
+
+/* find the first constraint such that m is not a variable */
+/* also, apply standalone elimination to it */
+
+Constraintlist
+firstNonVariable (Constraintlist cl)
+{
+  while (cl != NULL && isTermVariable (cl->constraint->term))
+    {
+      cl = cl->next;
+    }
+  if (cl != NULL)
+    {
+      msElim (cl->constraint);
+      cl->constraint->term = deVar (cl->constraint->term);
+      return cl;
+    }
+  else
+    {
+      return NULL;
+    }
+}
diff --git a/src/constraints.h b/src/constraints.h
new file mode 100644
index 0000000..ff5f541
--- /dev/null
+++ b/src/constraints.h
@@ -0,0 +1,42 @@
+#ifndef CONSTRAINTS
+#define CONSTRAINTS
+#include "terms.h"
+#include "knowledge.h"
+
+struct constraint
+{
+  Term term;
+  Knowledge know;
+};
+
+typedef struct constraint *Constraint;
+
+struct constraintlist
+{
+  Constraint constraint;
+  struct constraintlist *next;
+  struct constraintlist *prev;
+};
+
+typedef struct constraintlist *Constraintlist;
+
+Constraint makeConstraint (Term term, Knowledge know);
+Constraint constraintDuplicate (Constraint co);
+void constraintDestroy (Constraint cons);
+Constraintlist constraintlistAdd (Constraintlist cl, Constraint co);
+Constraintlist constraintlistConcat (Constraintlist cl1, Constraintlist cl2);
+Constraintlist constraintlistRewind (Constraintlist cl);
+Constraintlist constraintlistInsert (Constraintlist cl, Term term,
+				     Knowledge know);
+Constraintlist constraintlistUnlink (Constraintlist cl);
+Constraintlist constraintlistRemove (Constraintlist cl);
+void constraintlistDestroy (Constraintlist cl);
+void constraintlistDelete (Constraintlist cl);
+Constraintlist constraintlistShallow (Constraintlist oldcl);
+Constraintlist constraintlistDuplicate (Constraintlist oldcl);
+void constraintPrint (Constraint co);
+void constraintlistPrint (Constraintlist cl);
+
+Constraintlist firstNonVariable (Constraintlist cl);
+
+#endif
diff --git a/src/debug.c b/src/debug.c
new file mode 100644
index 0000000..401a946
--- /dev/null
+++ b/src/debug.c
@@ -0,0 +1,30 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "debug.h"
+#include "runs.h"
+
+static int debuglevel;
+
+void
+debugSet (int level)
+{
+  debuglevel = level;
+}
+
+int
+debugCond (int level)
+{
+  return (level <= debuglevel);
+}
+
+void
+debug (int level, char *string)
+{
+#ifdef DEBUG
+  if (debugCond (level))
+    {
+      indent ();
+      printf ("DEBUG [%i]: %s\n", level, string);
+    }
+#endif
+}
diff --git a/src/debug.h b/src/debug.h
new file mode 100644
index 0000000..2e3253d
--- /dev/null
+++ b/src/debug.h
@@ -0,0 +1,10 @@
+#ifndef DEBUG_H
+#define DEBUG_H
+
+void debugSet (int level);
+int debugCond (int level);
+void debug (int level, char *string);
+
+#define DEBUGL(a) debugCond(a)
+
+#endif
diff --git a/src/debuglevels.txt b/src/debuglevels.txt
new file mode 100644
index 0000000..873b4e4
--- /dev/null
+++ b/src/debuglevels.txt
@@ -0,0 +1,7 @@
+Conventions for debug levels; ifdef DEBUG
+
+-D1	meta		show compiled code, meta dynamic results
+-D2	claims		show results of claims
+-D3	events		show executed events
+-D4	internalsHigh	interesting internals (traces that were cut off)
+-D5	internalsLow	usually uninteresting stuff
diff --git a/src/design.txt b/src/design.txt
new file mode 100644
index 0000000..97c40bb
--- /dev/null
+++ b/src/design.txt
@@ -0,0 +1,47 @@
+Design Issues for the Model Checker
+-----------------------------------
+
+- For secrecy, we can trigger all sends at once. For synchronisation,
+  this is not the case.
+
+- Modules have to be split up sensibly.
+
+  - Although 'knowledge' and 'term matching' seem to different items,
+    their intertwined workings suggest that they should be implemented
+    in parallel.
+
+  - State generation (as in creating instances) might already allow for
+    a lot of static analysis.
+
+- We should make a list of required operations. Ingmar's work can serve
+  as a starting point.
+
+- For now, there will be no parser, and test cases will be input by
+  hand.
+
+- Synchronisation is more difficult to test, so we focus on secrecy
+  first. I've got some good ideas on Synchronisation testing though
+  (with narrowing sets of possible partners). Synchronisation is very
+  hard to prune, I presume. I have to prove that though ;)
+
+Sketch for secrecy:
+
+SimulateStep(F,M,constraints):
+	if Empty(F):
+		return
+	else:
+		for (s in PossibleSends):
+			add s.message to M
+			if (secrecy violated):
+				halt
+			remove s from F
+		ReadSets = supersetTransitions(F)
+		for (ReadSet in ReadSets):
+			for (s in ReadSet):
+				// dit is vaag
+				if NonMatch goto next ReadSet
+				constraint = F,M,match()
+			SimulateStep(F \ s,M,constraints)
+						
+				
+
diff --git a/src/knowledge.c b/src/knowledge.c
new file mode 100644
index 0000000..1816106
--- /dev/null
+++ b/src/knowledge.c
@@ -0,0 +1,474 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "termlists.h"
+#include "knowledge.h"
+#include "memory.h"
+#include "runs.h"
+#include "debug.h"
+
+/*
+ * Knowledge stuff
+ *
+ * Note that a really weird thing is going on involving unpropagated substitutions.
+ * Idea:
+ *
+ * 1. Substitute terms by filling in ->subst.
+ * Now, either:
+ * 2a. Undo this by knowledgeUndo.
+ * 2b. Propagate it, modifying the knowledge beyond repair by knowledgeSubstDo. Now inKnowledge works again.
+ * 2c. inKnowledge/knowledgeSet if something is in the knowledge: this does not consider the substitutions!, and 
+ *     they now have some overhead.
+ */
+
+void
+knowledgeInit (void)
+{
+  return;
+}
+
+void
+knowledgeDone (void)
+{
+}
+
+Knowledge
+makeKnowledge ()
+{
+  return (Knowledge) memAlloc (sizeof (struct knowledge));
+}
+
+Knowledge
+emptyKnowledge ()
+{
+  Knowledge know;
+
+  know = makeKnowledge ();
+  know->basic = NULL;
+  know->encrypt = NULL;
+  know->inverses = NULL;
+  know->vars = NULL;
+  return know;
+}
+
+Knowledge
+knowledgeDuplicate (Knowledge know)
+{
+  Knowledge newknow;
+
+  if (know == NULL)
+    {
+      printf ("Warning! Trying to copy empty knowledge!\n");
+      return NULL;
+    }
+  newknow = makeKnowledge ();
+  newknow->basic = termlistShallow (know->basic);
+  newknow->encrypt = termlistShallow (know->encrypt);
+  newknow->vars = termlistShallow (know->vars);
+  newknow->inverses = know->inverses;
+  return newknow;
+}
+
+void
+knowledgeDelete (Knowledge know)
+{
+  if (know != NULL)
+    {
+      termlistDelete (know->basic);
+      termlistDelete (know->encrypt);
+      termlistDelete (know->vars);
+      memFree (know, sizeof (struct knowledge));
+    }
+}
+
+void
+knowledgeDestroy (Knowledge know)
+{
+  if (know != NULL)
+    {
+      termlistDestroy (know->basic);
+      termlistDestroy (know->encrypt);
+      termlistDestroy (know->vars);
+      // termlistDestroy(know->inverses);
+      memFree (know, sizeof (struct knowledge));
+    }
+}
+
+/*
+ * knowledgeAddTerm
+ *
+ * returns a boolean:
+ * true iff the term was actually new, and added.
+ */
+
+int
+knowledgeAddTerm (Knowledge know, Term term)
+{
+  if (know == NULL)
+    {
+      printf
+	("Warning: trying to add term to uninitialised (NULL) Know pointer.\n");
+      return 1;
+    }
+  if (term == NULL)
+    return 0;
+
+  term = deVar (term);
+
+  /* test whether we knew it before */
+  if (inKnowledge (know, term))
+    return 0;
+
+  if (isTermTuple (term))
+    {
+      knowledgeAddTerm (know, term->op1);
+      knowledgeAddTerm (know, term->op2);
+    }
+
+  /* adding variables? */
+  know->vars = termlistAddVariables (know->vars, term);
+
+  knowledgeSimplify (know, term);
+  if (isTermLeaf (term))
+    {
+      know->basic = termlistAdd (know->basic, term);
+    }
+  if (term->type == ENCRYPT)
+    {
+      Term invkey = inverseKey (know->inverses, term->key);
+      if (inKnowledge (know, invkey))
+	{
+	  /* we can decrypt it */
+	  knowledgeAddTerm (know, term->op);
+	  if (!inKnowledge (know, term->key))
+	    {
+	      /* we know the op now, but not the key, so add it anyway */
+	      know->encrypt = termlistAdd (know->encrypt, term);
+	    }
+	}
+      else
+	{
+	  /* we cannot decrypt it, and from the initial test we know we could not construct it */
+	  know->encrypt = termlistAdd (know->encrypt, term);
+	}
+      termDelete (invkey);
+    }
+  return 1;
+}
+
+
+/*
+	Note: the input is a key k, i.e. it can decrypt
+	anything that was encrypted with k^{-1}.
+*/
+
+void
+knowledgeSimplify (Knowledge know, Term key)
+{
+  Termlist tldecrypts = NULL;
+  Termlist scan = know->encrypt;
+  Term invkey = inverseKey (know->inverses, key);
+
+  while (scan != NULL)
+    {
+      if (isTermEqual ((scan->term)->key, invkey))
+	{
+	  tldecrypts = termlistAdd (tldecrypts, (scan->term)->op);
+	  know->encrypt = termlistDelTerm (scan);
+	  scan = know->encrypt;
+	}
+      else
+	scan = scan->next;
+    }
+  termDelete (invkey);
+  knowledgeAddTermlist (know, tldecrypts);
+  termlistDelete (tldecrypts);
+}
+
+/*
+ * Add a whole termlist.
+ *
+ * Returns true iff there was at least one new item.
+ */
+
+int
+knowledgeAddTermlist (Knowledge know, Termlist tl)
+{
+  int flag = 0;
+
+  while (tl != NULL)
+    {
+      flag = knowledgeAddTerm (know, tl->term) || flag;
+      tl = tl->next;
+    }
+  return flag;
+}
+
+/*
+
+   add an inverse pair to the knowledge
+
+ */
+
+void
+knowledgeAddInverse (Knowledge know, Term t1, Term t2)
+{
+  know->inverses = termlistAdd (know->inverses, t1);
+  know->inverses = termlistAdd (know->inverses, t2);
+  return;
+}
+
+/*
+   same, but for list. List pointer is simply copied, so don't delete it later!
+*/
+
+void
+knowledgeSetInverses (Knowledge know, Termlist tl)
+{
+  know->inverses = tl;
+}
+
+/*
+
+inKnowledge
+
+Is a term a part of the knowledge?
+
+*/
+
+int
+inKnowledge (const Knowledge know, Term term)
+{
+  /* if there is no term, then it's okay 'fur sure' */
+  if (term == NULL)
+    return 1;
+  /* if there is a term, but no knowledge, we're in trouble */
+  if (know == NULL)
+    return 0;
+
+  mindwipe (know, inKnowledge (know, term));
+
+  term = deVar (term);
+  if (isTermLeaf (term))
+    {
+      return inTermlist (know->basic, term);
+    }
+  if (term->type == ENCRYPT)
+    {
+      return inTermlist (know->encrypt, term) ||
+	(inKnowledge (know, term->key) && inKnowledge (know, term->op));
+    }
+  if (term->type == TUPLE)
+    {
+      return (inTermlist (know->encrypt, term) ||
+	      (inKnowledge (know, term->op1) &&
+	       inKnowledge (know, term->op2)));
+    }
+  return 0;			/* unrecognized term type, weird */
+}
+
+int
+isKnowledgeEqual (Knowledge know1, Knowledge know2)
+{
+  if (know1 == NULL || know2 == NULL)
+    {
+      if (know1 == NULL && know2 == NULL)
+	return 1;
+      else
+	return 0;
+    }
+  if (!isTermlistEqual (know1->encrypt, know2->encrypt))
+    return 0;
+  return isTermlistEqual (know1->basic, know2->basic);
+}
+
+
+void
+knowledgePrint (Knowledge know)
+{
+  indent ();
+  if (know == NULL)
+    {
+      printf ("Empty.\n");
+      return;
+    }
+  printf (" [Basic]: ");
+  termlistPrint (know->basic);
+  printf ("\n");
+  indent ();
+  printf (" [Encrp]: ");
+  termlistPrint (know->encrypt);
+  printf ("\n");
+  indent ();
+  printf (" [Vars]: ");
+  termlistPrint (know->vars);
+  printf ("\n");
+}
+
+/*
+   print inverses
+ */
+
+void
+knowledgeInversesPrint (Knowledge know)
+{
+  Termlist tl;
+  int after = 0;
+
+  if (know == NULL)
+    {
+      printf ("Empty knowledge.");
+      return;
+    }
+
+  tl = knowledgeGetInverses (know);
+  if (tl == NULL)
+    {
+      printf ("None.");
+    }
+  else
+    {
+      while (tl != NULL && tl->next != NULL)
+	{
+	  if (after)
+	    {
+	      printf (",");
+	    }
+	  printf ("(");
+	  termPrint (tl->term);
+	  printf (",");
+	  termPrint (tl->next->term);
+	  printf (")");
+	  after = 1;
+	  tl = tl->next->next;
+	}
+    }
+}
+
+/*
+   give the set of representatives for the knowledge.
+   Note: this is a shallow copy, and needs to be termlistDelete'd.
+ */
+
+Termlist
+knowledgeSet (Knowledge know)
+{
+  Termlist tl1, tl2;
+
+  tl1 = termlistShallow (know->basic);
+  tl2 = termlistShallow (know->encrypt);
+  return termlistConcat (tl1, tl2);
+}
+
+/*
+   get the inverses pointer of the knowledge.
+   Essentially the inverse function of knowledgeSetInverses
+*/
+
+Termlist
+knowledgeGetInverses (Knowledge know)
+{
+  if (know == NULL)
+    return NULL;
+  else
+    return know->inverses;
+}
+
+/*
+ * check whether any substitutions where made at all.
+ */
+
+int
+knowledgeSubstNeeded (const Knowledge know)
+{
+  Termlist tl;
+
+  if (know == NULL)
+    return 0;
+  tl = know->vars;
+  while (tl != NULL)
+    {
+      if (tl->term->subst != NULL)
+	return 1;
+      tl = tl->next;
+    }
+  return 0;
+}
+
+/*
+ * knowledgeReconstruction
+ *
+ * This is useful after e.g. substitutions.
+ * Just rebuilds the knowledge in a new (shallow) copy.
+ */
+
+Knowledge
+knowledgeReconstruction (const Knowledge know)
+{
+  Knowledge newknow = emptyKnowledge ();
+
+  newknow->inverses = know->inverses;
+  knowledgeAddTermlist (newknow, know->basic);
+  knowledgeAddTermlist (newknow, know->encrypt);
+  return newknow;
+}
+
+/*
+ * propagate any substitutions just made.
+ *
+ * This usually involves reconstruction of the complete knowledge, which is
+ * 'cheaper' than a thorough analysis, so we always make a copy.
+ */
+
+Knowledge
+knowledgeSubstDo (const Knowledge know)
+{
+  /* otherwise a copy (for deletion) is returned. */
+  return knowledgeReconstruction (know);
+}
+
+/*
+ * Undo the substitutions just made. Note that this does not work anymore after knowledgeSubstDo!
+ */
+
+void
+knowledgeSubstUndo (const Knowledge know)
+{
+  Termlist tl;
+
+  tl = know->vars;
+  while (tl != NULL)
+    {
+      tl->term->subst = NULL;
+      tl = tl->next;
+    }
+}
+
+/*
+ * knowledgeNew(old,new)
+ *
+ * yield a termlist (or NULL) that represents the reduced items that are
+ * in the new set, but not in the old one.
+ */
+
+Termlist
+knowledgeNew (const Knowledge oldk, const Knowledge newk)
+{
+  Termlist newtl;
+
+  newtl = NULL;
+
+  void addNewStuff (Termlist tl)
+  {
+    while (tl != NULL)
+      {
+	if (!inKnowledge (oldk, tl->term))
+	  {
+	    newtl = termlistAdd (newtl, tl->term);
+	  }
+	tl = tl->next;
+      }
+  }
+  addNewStuff (newk->basic);
+  addNewStuff (newk->encrypt);
+  return newtl;
+}
diff --git a/src/knowledge.h b/src/knowledge.h
new file mode 100644
index 0000000..3005da2
--- /dev/null
+++ b/src/knowledge.h
@@ -0,0 +1,60 @@
+#ifndef KNOWLEDGE
+#define KNOWLEDGE
+
+#include "terms.h"
+#include "termlists.h"
+
+struct knowledge
+{
+  Termlist basic;
+  Termlist encrypt;
+  Termlist inverses;
+  union
+  {
+    Termlist vars;		// special: denotes unsubstituted variables
+    struct knowledge *next;	// use for alternative memory management.
+  };
+};
+
+typedef struct knowledge *Knowledge;
+
+void knowledgeInit (void);
+void knowledgeDone (void);
+Knowledge makeKnowledge ();
+Knowledge emptyKnowledge ();
+Knowledge knowledgeDuplicate (Knowledge know);
+void knowledgeDelete (Knowledge know);
+void knowledgeDestroy (Knowledge know);
+int knowledgeAddTerm (Knowledge know, Term term);
+int knowledgeAddTermlist (Knowledge know, Termlist tl);
+void knowledgeAddInverse (Knowledge know, Term t1, Term t2);
+void knowledgeSetInverses (Knowledge know, Termlist tl);
+void knowledgeSimplify (Knowledge know, Term decryptkey);
+int inKnowledge (const Knowledge know, Term term);
+void knowledgePrint (Knowledge know);
+void knowledgeInversesPrint (Knowledge know);
+int isKnowledgeEqual (Knowledge know1, Knowledge know2);
+Termlist knowledgeSet (Knowledge know);
+Termlist knowledgeGetInverses (Knowledge know);
+int knowledgeSubstNeeded (const Knowledge know);
+Knowledge knowledgeSubstDo (const Knowledge know);
+void knowledgeSubstUndo (const Knowledge know);
+Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
+
+#define mindwipe(k,recurse) \
+	if (k != NULL && k->vars != NULL) { \
+		Termlist tl = k->vars; \
+		while (tl != NULL) { \
+			if (tl->term->subst != NULL) { \
+				Term oldsubst = tl->term->subst; \
+				tl->term->subst = NULL; \
+				int flag = recurse; \
+				tl->term->subst = oldsubst; \
+				return flag; \
+			} \
+			tl = tl->next; \
+		} \
+	} \
+
+
+#endif
diff --git a/src/language.txt b/src/language.txt
new file mode 100644
index 0000000..a3e84ba
--- /dev/null
+++ b/src/language.txt
@@ -0,0 +1,46 @@
+Language
+--------
+
+language	:= (<def>)*
+def		:= (<directive> | <protocol> | <rundef> | <unstrusted>)
+
+//directive	:= <dir_require>
+//dir_require	:= require <filename>;
+
+protocol	:= protocol <protocolname> ( <rolelist> ) { <roledef>* } optsc
+protocolname	:= <id>
+
+intruderknow	:= public <termlist>;
+roledef		:= role <rolename> { <actions> } optsc
+rolename	:= <id> 
+actions		:= (<action>;)+
+action		:= (<read> | <send> | <claim>)
+decl		:= (<const> | <var>)+
+const		:= const <termlist> [ : <typeterm> ];
+var		:= var <termlist> [ : <typelist> ];
+
+read		:= read [_<label>]  (<term>,<term>,<term>);
+send		:= send [_<label>]  (<term>,<term>,<term>);
+claim		:= claim [_<label>] (<term>,<termlist>);
+label		:= <id>;
+
+rundef		:= <protocolname>.<rolename> ( <instancelist> ) ;
+instancelist	:= (<agent>|<typeterm>)*
+
+agent		:= <term>
+typeterm	:= <term>
+typelist	:= <termlist>
+
+untrusted	:= untrusted <termlist>;
+
+termlist	:= <term> [, <termlist>]
+term		:= (<baseterm> | <encterm> | <tupleterm> | <function>)
+encterm		:= { <term> } <term>
+function	:= <term> ( <term> )
+baseterm	:= (<variable> | <const>)
+variable	:= <id>
+const		:= <id>
+
+optsc		:= [ ; ]
+id		:= (<digit>|<uppercase>|<lowercase>)+
+
diff --git a/src/latex.c b/src/latex.c
new file mode 100644
index 0000000..e3a0c44
--- /dev/null
+++ b/src/latex.c
@@ -0,0 +1,797 @@
+/*
+ * LaTeX output component
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+#include <limits.h>
+#include "runs.h"
+#include "memory.h"
+#include "modelchecker.h"
+#include "tracebuf.h"
+#include "varbuf.h"
+#include "output.h"
+
+#define EVENTSPACE 1
+#define LINKTHRESHOLD 0.95
+
+extern const char *progname;
+extern const char *releasetag;
+extern int globalLatex;
+extern Term TERM_Function;
+
+/* struct for additional info */
+
+struct traceinfo {
+    int match;
+    int position;
+};
+
+/* global variables for this module */
+
+struct traceinfo *tinfo;
+int width;
+int landscape = 0;
+int *runPerm;
+
+/* code */
+
+void latexInit(const System sys, int argc, char **argv)
+{
+    int i;
+
+    printf("\\documentclass{article}\n");
+    printf("\\usepackage{msc}\n");
+    printf("%%\n");
+    printf("%% LaTeX output generated by %s\n", progname);
+    printf("%% Input:\n");
+
+    /* print command line */
+    printf("%% $");
+    for (i = 0; i < argc; i++)
+	printf(" %s", argv[i]);
+    printf("\n");
+
+    printf("%%\n");
+    printf("\\begin{document}\n\n");
+
+    /* comment macro (used for debugging) */
+    printf("\\newcommand{\\comment}[1]{}\n");
+
+    /* preamble */
+    printf("\\input{preamble}\n");
+}
+
+void latexDone(const System sys)
+{
+    printf("\\input{postamble}\n");
+    printf("\n\\end{document}\n\n");
+}
+
+void
+latexTermPrint (Term term, Termlist highlight)
+{
+	if (term == NULL)
+	{
+		printf ("Empty term");
+		return;
+	}
+#ifdef DEBUG
+	if (!DEBUGL (1))
+	{
+		term = deVar (term);
+	}
+#else
+	term = deVar (term);
+#endif
+	if (realTermLeaf (term))
+	{
+		if (inTermlist(highlight, term))
+			printf("\\mathbf{");
+		symbolPrint (term->symb);
+		if (realTermVariable (term))
+			printf ("V");
+		if (term->runid >= 0)
+		{
+			printf ("\\sharp%i", term->runid);
+		}
+		if (term->subst != NULL)
+		{
+			printf ("\\rightarrow");
+			latexTermPrint (term->subst, highlight);
+		}
+		if (inTermlist(highlight, term))
+			printf("}");
+	}
+	if (realTermTuple (term))
+	{
+		printf ("(");
+		while (realTermTuple (term))
+		{
+			latexTermPrint (term->op1, highlight);
+			printf (",");
+			term = term->op2;
+			if (!realTermTuple (term))
+				latexTermPrint (term, highlight);
+
+		}
+		printf (")");
+		return;
+	}
+	if (realTermEncrypt (term))
+	{
+		if (isTermLeaf (term->key)
+				&& inTermlist (term->key->stype, TERM_Function))
+		{
+			/* function application */
+			latexTermPrint (term->key, highlight);
+			printf ("(");
+			latexTermPrint (term->op, highlight);
+			printf (")");
+		}
+		else
+		{
+			/* normal encryption */
+			printf ("\\{");
+			latexTermPrint (term->op, highlight);
+			printf ("\\}_{");
+			latexTermPrint (term->key, highlight);
+			printf ("}");
+		}
+	}
+}
+
+void
+latexTermlistPrint (Termlist tl, Termlist highlight)
+{
+  if (tl == NULL)
+    {
+      printf ("[Empty]");
+      return;
+    }
+  printf ("[");
+  while (tl != NULL)
+    {
+      latexTermPrint (tl->term, highlight);
+      tl = tl->next;
+      if (tl != NULL)
+	  printf(", ");
+    }
+  printf ("]");
+}
+
+void latexTimers(const System sys)
+{
+    void endline(void) {
+	printf("\\\\ \\hline\n");
+    }
+
+    printf("\\begin{tabular}{|r|r|c|r|} \\hline\n");
+
+    /* display stats, header first */
+
+    printf("Time & States & Attack & st/sec");
+    endline();
+
+    /* print time */
+
+    double seconds;
+    seconds = (double) clock() / CLOCKS_PER_SEC;
+    printf("$%.3e$ &", seconds);
+
+    /* states traversed */
+
+    printf("$");
+    statesPrintShort(sys);
+    printf("$ &");
+
+    /* flag
+     *
+     * L n          Attack of length <n>
+     * None         failed claim
+     * NoClaim      no claims
+     */
+
+    if (sys->claims == 0) {
+	printf("NoClaim & ");
+    } else {
+	if (sys->failed > 0)
+	    printf("L:%i & ", attackLength(sys->attack));
+	else
+	    printf("None & ");
+    }
+
+    /*
+       printf("%.3e (%li) claims encountered.\n",(double)
+       sys->claims, sys->claims);
+       printf("%.3e (%li) claims failed.\n",(double)
+       sys->failed, sys->failed);
+     */
+
+    /* states per second */
+
+    if (seconds > 0) {
+	printf("$%.3e$ ",
+	       (double) (sys->statesLow +
+			 (sys->statesHigh * ULONG_MAX)) / seconds);
+    } else {
+	printf("$\\infty$ ");
+    }
+    endline();
+
+    printf("\\end{tabular}\n\n");
+}
+
+void latexMSCStart()
+{
+    if (landscape)
+	printf("\\begin{landscape}\n");
+
+    printf("\\begin{msc}{attack}\n");
+}
+
+void latexMSCEnd()
+{
+    printf("\\end{msc}\n");
+
+    if (landscape)
+	printf("\\end{landscape}\n");
+
+}
+
+void latexDeclInst(const System sys, int run)
+{
+	 Term bar = NULL;
+
+	bar = agentOfRun(sys, run);
+	printf("\\declinst{run%d}{$", run);
+	termPrint(bar);
+	printf("\\sharp%i$}{$", run);
+	agentsOfRunPrint(sys, run);
+	printf("$}\n");
+}
+
+void latexEventSpace(int amount)
+{
+    int i;
+	 //printf("%% number of newlines: %d\n",amount);
+    for (i = 0; i < EVENTSPACE * amount; i++)
+	printf("\\nextlevel\n");
+}
+
+
+void latexMessagePrint(struct tracebuf *tb, int from, int to)
+{
+
+	Term sendTerm = NULL;
+	Term readTerm = NULL;
+
+	if (from == -1 && to == -1) {
+		return;
+	}
+	if (from != -1) {
+		sendTerm = tb->event[from]->message;
+	}
+	if (to != -1) {
+		readTerm = tb->event[to]->message;
+	}
+	if (from == -1 && to != -1) {
+		printf("\\found{$");
+		termPrint(readTerm);
+		printf("$}{}{run%d}\n", tb->run[to]);
+	} else if (from != -1 && to == -1) {
+		printf("\\lost{$");
+		termPrint(sendTerm);
+		printf("$}{}{run%d}\n", tb->run[from]);
+	} else if (from != -1 && to != -1) {
+
+		printf("\\mess{$");
+
+		termPrint(sendTerm);
+
+		if (!isTermEqual(sendTerm, readTerm)) {
+			printf("\\rightarrow");
+			termPrint(readTerm);
+		}
+
+		printf("$}{run%d", tb->run[from]);
+		printf("}{run%d}[%d]", tb->run[to],
+				EVENTSPACE * (tinfo[to].position -
+					tinfo[from].position));
+
+		printf("\n");
+	}
+}
+void latexMessagePrintHighlight(struct tracebuf *tb, int from, int to, Termlist highlight)
+{
+
+	Term sendTerm = NULL;
+	Term readTerm = NULL;
+
+	if (from == -1 && to == -1) {
+		return;
+	}
+	if (from != -1) {
+		sendTerm = tb->event[from]->message;
+	}
+	if (to != -1) {
+		readTerm = tb->event[to]->message;
+	}
+	if (from == -1 && to != -1) {
+		printf("\\found{$");
+		latexTermPrint(readTerm, highlight);
+		printf("$}{}{run%d}\n", tb->run[to]);
+	} else if (from != -1 && to == -1) {
+		printf("\\lost{$");
+		latexTermPrint(sendTerm, highlight);
+		printf("$}{}{run%d}\n", tb->run[from]);
+	} else if (from != -1 && to != -1) {
+
+		printf("\\mess{$");
+
+		latexTermPrint(sendTerm, highlight);
+
+		if (!isTermEqual(sendTerm, readTerm)) {
+			printf("\\rightarrow");
+			latexTermPrint(readTerm, highlight);
+		}
+
+		printf("$}{run%d", tb->run[from]);
+		printf("}{run%d}[%d]", tb->run[to],
+				EVENTSPACE * (tinfo[to].position -
+					tinfo[from].position));
+
+		printf("\n");
+	}
+}
+void latexLearnComment(struct tracebuf *tb, int index, Termlist tl)
+{
+
+    printf("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", index + 1,
+	   index);
+    termlistPrint(tl);
+    printf("$}{envright}\n");
+}
+
+void latexAction(struct tracebuf *tb, int te)
+{
+    printf("\\action{$");
+    termPrint(tb->event[te]->message);
+    printf("$}{run%d}\n", tb->run[te]);
+    //printf("\\nextlevel\n");
+}
+
+void latexClaim(struct tracebuf *tb, int run, Termlist tl)
+{
+    printf("\\condition{$");
+    printf("\\neg secret ");
+    termlistPrint(tl);
+    printf("$}{run%d}\n", run);
+}
+
+int latexCorrespondingSend(struct tracebuf *tb, int rd)
+{
+
+    int labelMatch = 0;
+    int toMatch = 0;
+    int fromMatch = 0;
+    int tofromMatch = 0;
+    int messageMatch = 0;
+    int nMatches = 0;
+    int maxNMatches = 0;
+
+    int readEvent = rd;
+    int sendEvent = -1;
+    int bestSendEvent = -1;
+
+    for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) {
+	if (tb->event[sendEvent]->type == SEND) {
+	    /* do all the different kind of matchings first */
+
+	    labelMatch =
+		isTermEqual(tb->event[sendEvent]->label,
+			      tb->event[readEvent]->label);
+	    toMatch =
+		isTermEqual(tb->event[sendEvent]->to,
+			      tb->event[readEvent]->to);
+	    fromMatch =
+		isTermEqual(tb->event[sendEvent]->from,
+			      tb->event[readEvent]->from);
+	    tofromMatch = toMatch || fromMatch;
+	    messageMatch =
+		isTermEqual(tb->event[sendEvent]->message,
+			      tb->event[readEvent]->message);
+
+	    /* calculate the score */
+
+	    nMatches = labelMatch + tofromMatch + messageMatch;
+
+	    if (nMatches == 3) {
+		/* bingo! success on all matches */
+
+		//printf("Found perfect match: %d\n", s);
+		bestSendEvent = sendEvent;
+		break;
+	    }
+	    if (nMatches > maxNMatches) {
+		if (labelMatch && messageMatch) {
+		    /* strongest restriction: message and label should match */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+
+		} else if (messageMatch) {
+		    /* if label AND message don't match: */
+		    /* at least message should match */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+		} else if (labelMatch) {
+		    /* if message doesn't match */
+		    /* the label should matches */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+		}
+	    }
+	}
+    }
+
+    //bestSendEvent = NULL;
+    if (bestSendEvent == -1) {
+
+	int u;
+
+	for (u = 0; u < rd; u++) {
+	    if (tb->event[u]->type == SEND) {
+		//knowledgePrint(sys->traceKnow[u]);
+		if (inKnowledge
+		    (tb->know[u + 1], tb->event[readEvent]->message)) {
+		    bestSendEvent = u;
+		    break;
+		}
+	    }
+	}
+    }
+
+    if (bestSendEvent == -1) {
+	printf("%% Could not find a matching SEND\n");
+    }
+    return bestSendEvent;
+}
+
+
+int
+newInKnowledge (const Knowledge know, Term term)
+{
+  /* if there is no term, then it's okay 'fur sure' */
+  if (term == NULL)
+    return 1;
+  /* if there is a term, but no knowledge, we're in trouble */
+  if (know == NULL)
+    return 0;
+
+  mindwipe (know, inKnowledge (know, term));
+
+  term = deVar (term);
+  if (isTermLeaf (term))
+    {
+      return inTermlist (know->basic, term);
+    }
+  if (term->type == ENCRYPT)
+    {
+      return inTermlist (know->encrypt, term) ||
+	(inKnowledge (know, term->key) || inKnowledge (know, term->op));
+    }
+  if (term->type == TUPLE)
+    {
+      return (inTermlist (know->encrypt, term) ||
+	      (inKnowledge (know, term->op1) || 
+	       inKnowledge (know, term->op2)));
+    }
+  return 0;			/* unrecognized term type, weird */
+}
+
+int latexCorrespondingSend2(struct tracebuf *tb, int readEvent)
+{
+    int u;
+
+	 for (u = tb->length - 1; u>=0 ; u--)
+	 {
+		 if (tb->event[u]->type == SEND)
+		 { 
+			 if (!inKnowledge (tb->know[u], tb->event[readEvent]->message))
+			 {
+				 /*
+					 printf("%% term[");
+					 printf("]#%d is introduced at traceEvent[%d] ",readEvent,u);
+					 printf("\n");
+					 */
+				 return u;
+			 }
+		 }
+	 }
+		
+    return -1;
+
+}
+
+/*
+ * Display knowledge in LaTeX format.
+ */
+
+void knowledgePrintLatex(Knowledge know)
+{
+    Termlist tl;
+
+    if (know == NULL)
+    {
+        printf("\\emptyset");
+    }
+    else
+    {
+        tl = knowledgeSet(know);
+        termlistPrint(tl);
+        termlistDelete(tl);
+    }
+}
+
+void attackDisplayLatex(System sys)
+{
+    int i;
+    struct tracebuf *tb;
+    int *runPosition;
+    int currRun;
+    int position;
+    int eventSize;
+    Termlist tl;
+    Termlist newtl;
+	 Termlist claimDetails;
+	 Termlist highlights = NULL;
+    int cKnowledge;
+    int bestSend;
+
+    tb = sys->attack;
+    if (tb == NULL) {
+	printf("Attack pointer empty: nothing to display.\n");
+	exit(1);
+    }
+    /* set variables */
+    varbufSet (sys, tb->variables);
+
+    /* Rebuild knowledge. Strange, this ought to be good. 
+     * Maybe reconstruct dependencies as well. */
+    tracebufRebuildKnow(tb);
+
+    /* Make a comment in which the trace is displayed, for debugging etc. */
+    printf("\n\\comment{ TRACE\n\n");
+    printf("Length: %i\n",tb->length);
+    printf("Reallength: %i\n",tb->reallength);
+    printf("\n");
+    i = 0;
+    while (i <= tb->length)
+    {
+      printf("Knowledge %i:\n",i);
+		knowledgePrint(tb->know[i]);
+		printf(" [Inverses]: ");
+		knowledgeInversesPrint(tb->know[i]);
+		printf("\n\n");
+		if (i < tb->length)
+		{
+			 printf("Event %i\t[",i);
+			 switch (tb->status[i])
+				{
+				case S_UNK:
+				printf("?");
+				break;
+					case S_RED:
+				printf("redundant");
+				break;
+					case S_TOD:
+				printf("to do");
+				break;
+					case S_OKE:
+				printf("okay");
+					  break;
+					default:
+				printf("illegal status code");
+				break;
+				}
+			 printf("]\t");
+			 termPrint(tb->event[i]->message);
+			 printf("\t#%i",tb->run[i]);
+			 printf("\n");
+			 roledefPrint(tb->event[i]);
+			 printf("\n\n");
+		}
+		i++;
+    }
+    printf("}\n\n");
+
+    /* display initial knowledge */
+    printf("$I_0 = \\emptyset \\oplus ");
+    knowledgePrintLatex(tb->know[0]);
+    printf("$\n\n");
+
+    tinfo =
+	(struct traceinfo *) memAlloc((tb->length+1) *
+				      sizeof(struct traceinfo));
+
+    width = 1;
+    for (i = 0; i < tb->length; i++) {
+	if (tb->run[i] >= width)
+	    width = tb->run[i] + 1;
+    }
+
+    for (i = 0; i < tb->length; i++) {
+		 tb->link[i] = -1;
+	tinfo[i].match = -1;
+	tinfo[i].position = i;
+    }
+    tinfo[i].match = -1;
+    tinfo[i].position = i;
+
+    runPosition = (int *) memAlloc(width * sizeof(int));
+    for (i = 0; i < width; i++) {
+		 runPosition[i] = 0;
+    }
+    for (i = tb->length - 1; i >= 0; i--)
+	 {
+		 if (tb->status[i] != S_RED)
+		 {
+			 if (tb->event[i]->type == READ && !tb->event[i]->internal)
+			 {
+				 bestSend = latexCorrespondingSend2(tb, i);
+				 printf("%% match: %d <-> %d\n",i, bestSend);
+				 if (bestSend == -1)
+					 continue;
+
+				 tb->link[i] = bestSend;
+				 tb->link[bestSend] = i;
+			 }
+			 if (tb->event[i]->type == CLAIM)
+			 {
+				 claimDetails = claimViolationDetails(sys, tb->run[i], tb->event[i], tb->know[i]);
+			 }
+		 }
+	 }
+    printf("\\comment{ claimDetails :\n");
+    termlistPrint(claimDetails);
+    printf("\n}\n");
+
+    // landscape = (width > 4);		// not for the time being
+
+    position = 0;
+    currRun = 0;
+    eventSize = 0;
+    for (i = 0; i < tb->length; i++) 
+	 {
+		 if (tb->status[i] != S_RED)
+		 {
+			 tinfo[i].position = position; 
+			 eventSize = 1;
+			 currRun = tb->run[i];
+
+			 switch (tb->event[i]->type) {
+				 case SEND:
+					 position++;
+					 tinfo[i].position++;
+					 break;
+				 case READ:
+					 if (tb->link[i] != -1) {
+						 if (termDistance(tb->event[i]->message,tb->event[tb->link[i]]->message) < LINKTHRESHOLD)
+						 {
+							 /* disconnect read-send */
+							 tb->link[tb->link[i]] = -1;
+							 tb->link[i] = -1;
+						 } else {
+							 if (runPosition[currRun] <= tinfo[tb->link[i]].position &&
+									 currRun != tb->run[tb->link[i]])
+							 {
+									 printf("\\comment{\n");
+								 termPrint(tb->event[i]->message);
+								 printf("\n");
+								 termPrint(tb->event[tb->link[i]]->message);
+								 printf("\n");
+								 printf("%% termDistance: %f\n", 
+									termDistance(tb->event[i]->message, 
+											  tb->event[tb->link[i]]->message));
+								 printf("}\n");
+								 tinfo[i].position = tinfo[tb->link[i]].position;
+								 eventSize = 0;
+							 }
+						 }
+					 }
+					 if (tb->event[i]->internal) {
+						 eventSize = 0;
+					 }
+					 break;
+				 case CLAIM:
+					 if (claimDetails != NULL && claimDetails != (Termlist) -1) {
+						 eventSize = 2;
+					 } else {
+						 eventSize = 0;
+					 }
+					 break;
+				 default:
+					 break;
+			 }
+			 if (!(tb->event[i]->type == READ && tb->event[i]->internal))
+				 runPosition[currRun] = tinfo[i].position + eventSize;
+			 /* printf("%% Event %d at %d\n", i, position); */
+			 position += eventSize;
+		 }
+	 }
+
+    latexMSCStart();
+    for (i = 0; i < width; i++) {
+		 if (runPosition[i] > 0)
+			 latexDeclInst(sys, i);
+    }
+
+    //for (j=-1; j<=sys->step; j++)
+    position = 0;
+    cKnowledge = 0;
+    for (i = 0; i < tb->length; i++) 
+	 {
+		 if (tb->status[i] != S_RED) 
+		 {
+			 latexEventSpace(tinfo[i].position - position);
+			 if (tinfo[i].position >= position)
+			 {
+				 position = tinfo[i].position;
+			 }
+			 switch (tb->event[i]->type) {
+				 case SEND:
+					 newtl = knowledgeNew(tb->know[i], tb->know[i + 1]);
+					 highlights = NULL;
+					 /* Build a Termlist of terms that from the claimViolationDetails,
+						 that appear in the knowledge */
+					 if (newtl != NULL)
+					 {
+						 tl = claimDetails;
+						 while (tl != NULL)
+						 {
+							 if (inTermlist(newtl, tl->term))
+							 {
+								 highlights = termlistAdd(highlights, tl->term);
+							 }
+							 tl = tl->next;
+						 }
+						 printf("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", cKnowledge + 1,
+								 cKnowledge);
+						 cKnowledge++;
+						 latexTermlistPrint(newtl, highlights);
+						 printf("$}{envright}\n");
+					 }
+
+					 if (tb->link[i] != -1 && i < tb->length) {
+						 latexMessagePrintHighlight(tb, i, tb->link[i], highlights);
+					 } else {
+						 latexMessagePrintHighlight(tb, i, -1, highlights);	//lost message
+					 }
+					 termlistDelete(highlights);
+
+					 break;
+				 case READ:
+					 if (tb->event[i]->internal) {
+						} else if (tb->link[i] == -1) {
+							latexMessagePrint(tb, -1, i);	//found message
+						}
+					 break;
+				 case CLAIM:
+					 if (claimDetails != NULL && claimDetails != (Termlist) -1) {
+						 latexClaim(tb, tb->run[i], claimDetails);
+					 }
+					 break;
+				 default:
+					 break;		//kannie!
+			 }
+		 }
+    }
+	 latexEventSpace(2);
+    latexMSCEnd();
+    memFree(runPosition, width * sizeof(int));
+    memFree(tinfo, (tb->length+1) * sizeof(struct traceinfo));
+}
diff --git a/src/latex.h b/src/latex.h
new file mode 100644
index 0000000..ef9efac
--- /dev/null
+++ b/src/latex.h
@@ -0,0 +1,21 @@
+/*
+ * LaTeX output component header
+ */
+
+#ifndef LATEX
+#define LATEX
+
+#include "runs.h"
+
+void latexInit(const System sys, int argc, char **argv);
+void latexDone(const System sys);
+void latexTimers(const System sys);
+void latexMSCStart();
+void latexMSCEnd();
+void latexDeclInst(const System sys);
+void latexMessagePrint(const System sys, int from, int to);
+void latexLearnComment(const System sys, Termlist tl);
+void latexTracePrint(System sys);
+void attackDisplayLatex(System sys);
+
+#endif
diff --git a/src/license.txt b/src/license.txt
new file mode 100644
index 0000000..4a5bed6
--- /dev/null
+++ b/src/license.txt
@@ -0,0 +1,4 @@
+- GNU getopt
+- GNU bison/flex
+- ARGTABLE	http://argtable.sourceforge.net/
+- de rest (c) Cas
diff --git a/src/lutger-todo.txt b/src/lutger-todo.txt
new file mode 100644
index 0000000..c38849e
--- /dev/null
+++ b/src/lutger-todo.txt
@@ -0,0 +1 @@
+- TODO vullen
diff --git a/src/main.c b/src/main.c
new file mode 100644
index 0000000..31472de
--- /dev/null
+++ b/src/main.c
@@ -0,0 +1,548 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <time.h>
+#include <limits.h>
+#include "runs.h"
+#include "debug.h"
+#include "modelchecker.h"
+#include "memory.h"
+#include "symbols.h"
+#include "pheading.h"
+#include "symbols.h"
+#include "tok.h"
+#include "tac.h"
+#include "compiler.h"
+#include "latex.h"
+#include "output.h"
+
+#include "argtable2.h"
+
+extern struct tacnode *spdltac;
+void scanner_cleanup (void);
+void strings_cleanup (void);
+int yyparse (void);
+
+void MC_incRuns (const System sys);
+void MC_incTraces (const System sys);
+void MC_single (const System sys);
+int modelCheck (const System sys);
+
+const char *progname = "scyther";
+const char *releasetag = "alpha2-devel";
+
+int
+main (int argc, char **argv)
+{
+  System sys;
+
+  struct arg_int *traversal = arg_int0 ("t", "traverse", NULL,
+					"set traversal method, partial order reduction (default is 8)");
+  struct arg_rem *trav1 = arg_rem (NULL, "1 : nondeterministic.");
+  struct arg_rem *trav2 = arg_rem (NULL, "2 : nonreads first.");
+  struct arg_rem *trav3 = arg_rem (NULL, "3 : nonreads; supertransition.");
+  struct arg_rem *trav4 =
+    arg_rem (NULL, "4 : nonreads; supertransition; forbidden");
+  struct arg_rem *trav5 = arg_rem (NULL,
+				   "5 : nonreads; supertransition; forbidden; remove hopeless");
+  struct arg_rem *trav6 =
+    arg_rem (NULL, "6 : secrecy p.o. reduction, new style");
+  struct arg_rem *trav7 = arg_rem (NULL,
+				   "7 : nonreads; supertransition; forbidden; remove hopeless V2");
+  struct arg_rem *trav8 =
+    arg_rem (NULL, "8 : nondeterministic knowledge brancher");
+  struct arg_int *match =
+    arg_int0 ("m", "match", NULL, "matching method (default is 0)");
+  struct arg_rem *match0 = arg_rem (NULL, "0 : typed.");
+  struct arg_rem *match1 = arg_rem (NULL, "1 : basic typeflaws.");
+  struct arg_rem *match2 = arg_rem (NULL, "2 : full typeflaws");
+  struct arg_lit *clp =
+    arg_lit0 ("c", "cl", "use constraint logic, non-associative.");
+  struct arg_int *prune = arg_int0 ("p", "prune", NULL,
+				    "pruning method (default is 2)");
+  struct arg_rem *prune0 =
+    arg_rem (NULL, "0 : search all traces, no pruning.");
+  struct arg_rem *prune1 = arg_rem (NULL,
+				    "1 : search traces of any length until a violation occurs.");
+  struct arg_rem *prune2 = arg_rem (NULL,
+				    "2 : search progessively shorter traces after a violated claim.");
+  struct arg_rem *prune3 = arg_rem (NULL, "3 : quit after a violated claim.");
+  struct arg_int *maxlength = arg_int0 ("l", "max-length", NULL,
+					"prune traces longer than <int> events.");
+  struct arg_lit *incTraces = arg_lit0 (NULL, "increment-traces",
+					"incremental search using the length of the traces.");
+  struct arg_int *maxruns =
+    arg_int0 ("r", "max-runs", NULL, "create at most <int> runs.");
+  struct arg_lit *incRuns = arg_lit0 (NULL, "increment-runs",
+				      "incremental search using the number of runs.");
+  struct arg_lit *latex = arg_lit0 (NULL, "latex", "output in LaTeX format.");
+  struct arg_lit *noreport =
+    arg_lit0 ("d", "disable-report", "don't report violations.");
+  struct arg_int *switchS = arg_int0 ("s", "states", NULL,
+				      "report total number of states and claims traversed.");
+  struct arg_rem *switchS0 =
+    arg_rem (NULL, "if <int> is not 0, report progress after <int> states.");
+  // struct arg_file *outfile = arg_file0("o",NULL,"<output>",            "output file (default is \"-\")");
+#ifdef DEBUG
+  struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
+  struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
+				      "indent the debug output using trace length.");
+  struct arg_int *debugl =
+    arg_int0 ("D", "debug", NULL, "set debug level (default is 0)");
+#endif
+  struct arg_lit *help = arg_lit0 (NULL, "help", "print this help and exit");
+  struct arg_lit *version =
+    arg_lit0 (NULL, "version", "print version information and exit");
+  //struct arg_file *infiles = arg_filen(NULL,NULL,"FILE",0,argc+2,               "input file(s)");
+  struct arg_end *end = arg_end (30);
+  void *argtable[] = {
+    traversal, trav1, trav2, trav3, trav4, trav5, trav6, trav7, trav8,
+    match, match0, match1, match2,
+    clp,
+    prune, prune0, prune1, prune2, prune3,
+    maxlength, incTraces,
+    maxruns, incRuns,
+    latex,
+    noreport,
+    switchS, switchS0,
+#ifdef DEBUG
+    porparam,
+    switchI,
+    debugl,
+#endif
+    help, version,
+    // infiles,
+    end
+  };
+  int nerrors;
+  int exitcode = 0;
+
+  /* verify the argtable[] entries were allocated sucessfully */
+  if (arg_nullcheck (argtable) != 0)
+    {
+      /* NULL entries were detected, some allocations must have failed */
+      printf ("%s: insufficient memory\n", progname);
+      exitcode = 1;
+      goto exit;
+    }
+
+  /* defaults
+   * set any command line default values prior to parsing */
+#ifdef DEBUG
+  debugl->ival[0] = 0;
+  porparam->ival[0] = 0;
+#endif
+  traversal->ival[0] = 8;
+  match->ival[0] = 0;
+  maxlength->ival[0] = -1;
+  maxruns->ival[0] = INT_MAX;
+  prune->ival[0] = 2;
+  switchS->ival[0] = 0;
+
+  /* Parse the command line as defined by argtable[] */
+  nerrors = arg_parse (argc, argv, argtable);
+
+  /* special case: '--help' takes precedence over error reporting */
+  if (help->count > 0)
+    {
+      printf ("Usage: %s ", progname);
+      arg_print_syntax (stdout, argtable, "\n");
+      printf
+	("This program can model check security protocols for various\n");
+      printf ("properties, given a finite scenario.\n\n");
+      arg_print_glossary (stdout, argtable, "  %-25s %s\n");
+      exitcode = 0;
+      goto exit;
+    }
+
+  /* special case: '--version' takes precedence error reporting */
+  if (version->count > 0)
+    {
+      printf ("'%s' model checker for security protocols.\n", progname);
+      printf ("%s release.\n", releasetag);
+#ifdef DEBUG
+      printf ("Compiled with debugging support.\n");
+#endif
+      printf ("December 2003--, Cas Cremers\n");
+      exitcode = 0;
+      goto exit;
+    }
+
+  /* If the parser returned any errors then display them and exit */
+  if (nerrors > 0)
+    {
+      /* Display the error details contained in the arg_end struct. */
+      arg_print_errors (stdout, end, progname);
+      printf ("Try '%s --help' for more information.\n", progname);
+      exitcode = 1;
+      goto exit;
+    }
+
+  /* special case: uname with no command line options induces brief help */
+  /*
+     if (argc==1)
+     {
+     printf("Try '%s --help' for more information.\n",progname);
+     exitcode=0;
+     goto exit;
+     }
+   */
+
+  /*
+   * Arguments have been parsed by argtable,
+   * continue with main code.
+   */
+
+  /* Lutger-tries-to-test-with-broken-methods detector */
+  if (clp->count > 0)
+    {
+      printf ("For the time being, this method is not supported, \n");
+      printf ("as too many changes have been made to the normal \n");
+      printf ("matching logic, and CL simply isn't reliable in \nmany ");
+      printf ("ways. Try again in a few weeks.\n");
+      exit(0);
+    }
+
+  /* handle debug level */
+#ifdef DEBUG
+  debugSet (debugl->ival[0]);
+  if (DEBUGL (1))
+    {
+      /* print command line */
+      int i;
+      printf ("$");
+      for (i = 0; i < argc; i++)
+	printf (" %s", argv[i]);
+      printf ("\n");
+    }
+#else
+  debugSet (0);
+#endif
+  /* Initialize memory routines */
+  memInit ();
+
+  /* initialize symbols */
+  termsInit ();
+  termlistsInit ();
+  knowledgeInit ();
+  symbolsInit ();
+  tacInit ();
+
+  /* generate system */
+  sys = systemInit ();
+#ifdef DEBUG
+  sys->porparam = porparam->ival[0];
+#endif
+  sys->latex = latex->count;
+  sys->know = emptyKnowledge ();
+
+  /* parse input */
+
+  yyparse ();
+#ifdef DEBUG
+  if (DEBUGL (1))
+    tacPrint (spdltac);
+#endif
+
+  /* compile */
+
+  compile (sys, spdltac, maxruns->ival[0]);
+  scanner_cleanup ();
+
+#ifdef DEBUG
+  if (DEBUGL (1))
+    {
+      printf ("\nCompilation yields:\n\n");
+      printf ("untrusted agents: ");
+      termlistPrint (sys->untrusted);
+      printf ("\n");
+      knowledgePrint (sys->know);
+      printf ("inverses: ");
+      knowledgeInversesPrint (sys->know);
+      printf ("\n");
+      locVarPrint (sys->locals);
+      protocolsPrint (sys->protocols);
+
+      printf ("\nInstantiated runs:\n\n");
+      runsPrint (sys);
+    }
+#endif
+
+  /* allocate memory for traces, based on runs */
+  systemStart (sys);
+  sys->traceKnow[0] = sys->know;	// store initial knowledge
+
+  /* add parameters to system */
+
+  sys->clp = (clp->count > 0 ? 1 : 0);
+
+  sys->traverse = traversal->ival[0];
+  sys->match = match->ival[0];
+  sys->prune = prune->ival[0];
+  sys->switchS = switchS->ival[0];
+
+  /* TODO for now, warning for -m2 and non-clp */
+  if (sys->match == 2 && !sys->clp)
+    {
+      printf
+	("Warning: -m2 is only supported for constraint logic programming.\n");
+    }
+#ifdef DEBUG
+  /* in debugging mode, some extra switches */
+  if (switchI->count > 0)
+    indentActivate ();
+  if (DEBUGL (1))
+    printf ("Using traversal method %i.\n", sys->traverse);
+#else
+  /* non-debug defaults */
+  sys->switchM = 0;
+#endif
+  if (noreport->count > 0)
+    sys->report = 0;
+  if (maxlength->ival[0] >= 0)
+    sys->switch_maxtracelength = maxlength->ival[0];
+
+  /* latex header? */
+  if (sys->latex)
+    latexInit (sys, argc, argv);
+
+  /* model check system */
+#ifdef DEBUG
+  if (DEBUGL (1))
+    printf ("Start modelchecking system.\n");
+#endif
+  if (incRuns->count > 0)
+    {
+      MC_incRuns (sys);
+    }
+  else
+    {
+      if (incTraces->count > 0)
+	{
+	  MC_incTraces (sys);
+	}
+      else
+	{
+	  MC_single (sys);
+	}
+    }
+  
+  /* Display shortest attack, if any */
+
+  if (sys->attack != NULL && sys->attack->length != 0)
+    {
+      attackDisplay(sys);
+    }
+
+  /* latex closeup */
+  if (sys->latex)
+    latexDone (sys);
+
+  /*
+   * Now we clean up any memory that was allocated.
+   */
+
+  knowledgeDestroy (sys->know);
+  systemDone (sys);
+
+  /* done symbols */
+  tacDone ();
+  symbolsDone ();
+  knowledgeDone ();
+  termlistsDone ();
+  termsDone ();
+
+  /* memory clean up? */
+  strings_cleanup ();
+  memDone ();
+
+exit:
+  /* deallocate each non-null entry in argtable[] */
+  arg_free (argtable);
+
+  return exitcode;
+}
+
+void
+timersPrint (const System sys)
+{
+  /* display stats, header first */
+
+  printf ("Time\t\tStates\t\tAttack\t\tst/sec\n");
+
+  /* print time */
+
+  double seconds;
+  seconds = (double) clock () / CLOCKS_PER_SEC;
+  printf ("%.3e\t", seconds);
+
+  /* states traversed */
+
+  statesPrintShort (sys);
+  printf ("\t");
+
+  /* flag
+   *
+   * L n          Attack of length <n>
+   * None         failed claim
+   * NoClaim      no claims
+   */
+
+  if (sys->claims == 0)
+    {
+      printf ("NoClaim\t\t");
+    }
+  else
+    {
+      if (sys->failed > 0)
+	printf ("L:%i\t\t", attackLength(sys->attack));
+      else
+	printf ("None\t\t");
+    }
+
+  /*
+     printf("%.3e (%li) claims encountered.\n",(double)
+     sys->claims, sys->claims);
+     printf("%.3e (%li) claims failed.\n",(double)
+     sys->failed, sys->failed);
+   */
+
+  /* states per second */
+
+  if (seconds > 0)
+    {
+      printf ("%.3e\t",
+	      (double) (sys->statesLow +
+			(sys->statesHigh * ULONG_MAX)) / seconds);
+    }
+  else
+    {
+      printf ("<inf>\t\t");
+    }
+
+  printf ("\n");
+}
+
+/*
+ * Analyse the model.
+ *
+ * This procedure considers mainly incremental searches, and settings
+ * parameters for that. The real work is handled by modelCheck.
+ */
+
+void
+MC_incRuns (const System sys)
+{
+  /*
+   * incremental runs check
+   *
+   * note: we assume that at least one run needs to be checked.
+   */
+  int maxruns = sys->maxruns;
+  int runs = 1;
+  int flag = 1;
+  int res;
+
+  do
+    {
+      systemReset (sys);
+      sys->maxruns = runs;
+      printf ("%i of %i runs in incremental runs search.\n", runs, maxruns);
+      res = modelCheck (sys);
+      printf ("\n");
+      if (res)
+	{
+	  /* Apparently a violation occurred. If we are searching
+	   * the whole space, then we just continue.  However, if
+	   * we're looking to prune, ``the buck stops here''. */
+
+	  if (sys->prune != 0)
+	    {
+	      flag = 0;
+	    }
+	}
+      runs++;
+    }
+  while (flag && runs <= maxruns);
+}
+
+void
+MC_incTraces (const System sys)
+{
+  /*
+   * incremental traces check
+   *
+   * note: we assume that at least one run needs to be checked.
+   */
+  int maxtracelen;
+  int tracelen;
+  int tracestep;
+
+  tracestep = 3;		/* what is a sensible stepping size? */
+  maxtracelen = getMaxTraceLength (sys);
+  tracelen = maxtracelen - tracestep;
+  while (tracelen > 6)		/* what is a reasonable minimum? */
+    tracelen -= tracestep;
+
+  int flag = 1;
+  int res;
+
+  do
+    {
+      systemReset (sys);
+      sys->maxtracelength = tracelen;
+      printf ("%i of %i trace length in incremental trace length search.\n",
+	      tracelen, maxtracelen);
+      res = modelCheck (sys);
+      printf ("\n");
+      if (res)
+	{
+	  /* Apparently a violation occurred. If we are searching
+	   * the whole space, then we just continue.  However, if
+	   * we're looking to prune, ``the buck stops here''. */
+
+	  if (sys->prune != 0)
+	    {
+	      flag = 0;
+	    }
+	}
+      tracelen += tracestep;
+    }
+  while (flag && tracelen <= maxtracelen);
+}
+
+/*
+ * Traditional handywork
+ */
+
+void
+MC_single (const System sys)
+{
+  /*
+   * simple one-time check
+   */
+
+  systemReset (sys);		// reset any globals
+  modelCheck (sys);
+}
+
+/*
+ * Model check the system, given all parameters.
+ * 
+ * Precondition: the system was reset with the corresponding parameters.
+ * This also reports on time and states traversed.
+ */
+
+int
+modelCheck (const System sys)
+{
+  traverse (sys);		// start model checking
+  if (sys->latex)
+    {
+      latexTimers (sys);
+    }
+  else
+    {
+      timersPrint (sys);
+    }
+  return (sys->failed);
+}
diff --git a/src/match_basic.c b/src/match_basic.c
new file mode 100644
index 0000000..c55e2bd
--- /dev/null
+++ b/src/match_basic.c
@@ -0,0 +1,298 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "memory.h"
+#include "substitutions.h"
+#include "runs.h"
+#include "modelchecker.h"
+#include "match_basic.h"
+
+Termlist
+candidates (const Knowledge know)
+{
+  Termlist knowset;
+  Termlist candlist;
+
+  /* candidates for typeless basic stuff */
+  knowset = knowledgeSet (know);
+  candlist = termlistAddBasics (NULL, knowset);
+  termlistDelete (knowset);
+  return candlist;
+}
+
+
+struct fvpass
+{
+  int (*solution) (struct fvpass, Knowledge);
+
+  System sys;
+  int run;
+  Roledef roledef;
+  int (*proceed) (System, int);
+};
+
+/*
+ * fix variables in a message, and check whether it can be accepted.
+ *
+ * fp.sys is only accessed for the matching type.
+ */
+
+
+int
+fixVariablelist (const struct fvpass fp, const Knowledge know,
+		 Termlist varlist, const Term message)
+{
+  int flag = 0;
+
+  Termlist tlscan;
+  Termlist candlist;
+
+  if (varlist != NULL)
+    {
+      if (!isTermVariable (varlist->term))
+	{
+	  while (varlist != NULL && !isTermVariable (varlist->term))
+	    {
+	      varlist = varlist->next;
+	    }
+	}
+    }
+
+  /* cond: varlist == NULL || isTermvariable(varlist->term) */
+
+  if (varlist == NULL)
+    {
+      /* there are no (more) variables to be fixed. */
+      /* actually trigger it if possible */
+
+      int copied;
+      Knowledge tempknow;
+
+      /* first we propagate the substitutions in the knowledge */
+      /* TODO this must also be done for all agent knowledge!! */
+
+      if (knowledgeSubstNeeded (know))
+	{
+	  copied = 1;
+	  tempknow = knowledgeSubstDo (know);
+	}
+      else
+	{
+	  copied = 0;
+	  tempknow = know;
+	}
+
+      if (inKnowledge (tempknow, message))
+	{
+	  if (fp.solution != NULL)
+	    {
+	      flag = fp.solution (fp, tempknow);
+	    }
+	  else
+	    {
+	      flag = 1;
+	    }
+	}
+      else
+	flag = 0;
+
+      /* restore state */
+      if (copied)
+	{
+	  knowledgeDelete (tempknow);
+	  knowledgeSubstUndo (know);
+	}
+      return flag;
+    }
+
+  /* cond: isTermvariable(varlist->term) */
+  varlist->term = deVar (varlist->term);
+  /* cond: realTermvariable(varlist->term) */
+  candlist = candidates (know);
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      indent ();
+      printf ("Set ");
+      termPrint (varlist->term);
+      printf (" with type ");
+      termlistPrint (varlist->term->stype);
+      printf (" from candidates ");
+      termlistPrint (candlist);
+      printf ("\n");
+    }
+#endif
+
+  /* Now check all candidates. Do they work as candidates? */
+  tlscan = candlist;
+  while (tlscan != NULL && !(flag && fp.solution == NULL))
+    {
+      if (!isTermEqual (varlist->term, tlscan->term))
+	{
+	  /* substitute */
+	  varlist->term->subst = tlscan->term;
+	  if (validSubst (fp.sys->match, varlist->term))
+	    {
+#ifdef DEBUG
+	      if (DEBUGL (5))
+		{
+		  indent ();
+		  printf ("Substituting ");
+		  termPrint (varlist->term);
+		  printf ("\n");
+		}
+#endif
+	      /* now we may need to substitute more */
+	      flag = fixVariablelist (fp, know, varlist->next, message)
+		|| flag;
+	    }
+	}
+      tlscan = tlscan->next;
+    }
+  /* restore state: variable is not instantiated. */
+  varlist->term->subst = NULL;
+
+  /* garbage collect */
+  termlistDelete (candlist);
+
+  return flag;
+}
+
+/*
+ * check whether a roledef, given some newer knowledge substitutions, can survive
+ */
+
+#define enabled_basic(sys,know,newterm) !inKnowledge(know,newterm)
+
+/*
+ * matchRead
+ *
+ * try to execute a read event. It must be able to be construct it from the
+ * current intruder knowledge (Inject), but not from the forbidden knowledge
+ * set, which we tried earlier.
+ *
+ * returns 0 if it is not enabled, 1 if it was enabled (and routes explored)
+ */
+
+int
+matchRead_basic (const System sys, const int run,
+		 int (*proceed) (System, int))
+{
+  Roledef rd;
+  int flag = 0;
+  struct fvpass fp;
+
+  int solution (struct fvpass fp, Knowledge know)
+  {
+    Knowledge oldknow;
+    Term newterm;
+
+    /* remove variable linkages */
+    newterm = termDuplicateUV (fp.roledef->message);
+    /* a candidate, but if this is a t4 traversal, is it also an old one? */
+    if (fp.sys->traverse < 4 ||
+	fp.roledef->forbidden == NULL ||
+	enabled_basic (fp.sys, fp.roledef->forbidden, newterm))
+      {
+	/* it is enabled, i.e. not forbidden */
+	oldknow = fp.sys->know;
+	fp.sys->know = know;
+#ifdef DEBUG
+	if (DEBUGL (5))
+	  {
+	    printf ("+");
+	  }
+#endif
+	fp.proceed (fp.sys, fp.run);
+	fp.sys->know = oldknow;
+	termDelete (newterm);
+	return 1;
+      }
+    else
+      {
+	/* blocked */
+#ifdef DEBUG
+	if (DEBUGL (5))
+	  {
+	    printf ("-");
+	  }
+#endif
+	termDelete (newterm);
+	return 0;
+      }
+  }
+
+  rd = runPointerGet (sys, run);
+  Termlist varlist = termlistAddVariables (NULL, rd->message);
+
+  fp.sys = sys;
+  fp.run = run;
+  fp.roledef = rd;
+  fp.proceed = proceed;
+  fp.solution = solution;
+
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      indent ();
+      printf ("{\n");
+    }
+#endif
+  flag = fixVariablelist (fp, sys->know, varlist, rd->message);
+  termlistDelete (varlist);
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      indent ();
+      printf ("} with flag %i\n", flag);
+    }
+#endif
+  return flag;
+}
+
+/* 
+ * block
+ *
+ * Skips over an event. Because the intruder knowledge is incremental, we can
+ * just overwrite the old value of forbidden.
+ */
+
+int
+block_basic (const System sys, const int run)
+{
+  Knowledge pushKnow;
+  Roledef rd;
+
+  rd = runPointerGet (sys, run);
+  pushKnow = rd->forbidden;
+  rd->forbidden = sys->know;
+  traverse (sys);
+  rd->forbidden = pushKnow;
+  return 1;
+}
+
+int
+send_basic (const System sys, const int run)
+{
+  Roledef rd = runPointerGet (sys, run);
+  /* execute send, push knowledge? */
+  if (inKnowledge (sys->know, rd->message))
+    {
+      /* no new knowledge, so this remains */
+      explorify (sys, run);
+    }
+  else
+    {
+      /* new knowledge, must store old state */
+      Knowledge oldknow = sys->know;
+      sys->know = knowledgeDuplicate (sys->know);
+
+      sys->knowPhase++;
+      knowledgeAddTerm (sys->know, rd->message);
+      explorify (sys, run);
+      sys->knowPhase--;
+
+      knowledgeDelete (sys->know);
+      sys->know = oldknow;
+    }
+  return 1;
+}
diff --git a/src/match_basic.h b/src/match_basic.h
new file mode 100644
index 0000000..88b5d58
--- /dev/null
+++ b/src/match_basic.h
@@ -0,0 +1,11 @@
+#ifndef MATCHBASIC
+#define MATCHBASIC
+
+int matchRead_basic (const System sys, const int run,
+		     int (*proceed) (System, int));
+int enabled_basic (const System sys, const Knowledge know,
+		   const Term newterm);
+int block_basic (const System sys, const int run);
+int send_basic (const System sys, const int run);
+
+#endif
diff --git a/src/match_clp.c b/src/match_clp.c
new file mode 100644
index 0000000..e6eab42
--- /dev/null
+++ b/src/match_clp.c
@@ -0,0 +1,502 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "match_clp.h"
+#include "runs.h"
+#include "memory.h"
+#include "constraints.h"
+#include "mgu.h"
+#include "memory.h"
+#include "debug.h"
+#include "match_clp.h"
+#include "modelchecker.h"
+
+struct solvepass
+{
+  int (*solution) (struct solvepass, Constraintlist);
+
+  System sys;
+  int run;
+  int (*proceed) (System, int);
+};
+
+int
+solve (const struct solvepass sp, Constraintlist solvecons)
+{
+  Constraintlist activecl, cl, beforecl;
+  Constraint activeco;
+  int flag;
+
+  flag = 0;
+
+  /* locate first non-variable constraint */
+  activecl = firstNonVariable (solvecons);
+
+  if (activecl == NULL)
+    {
+      /* no such thing, so that's nice */
+      if (sp.solution != NULL)
+	sp.solution (sp, solvecons);
+      return 1;
+    }
+
+  /* there is an active constraint */
+  /* detach it from the list, but retain */
+  beforecl = activecl->prev;
+  solvecons = constraintlistUnlink (activecl);
+  activeco = activecl->constraint;
+  if (isTermTuple (activeco->term))
+    {
+      /* it's a tuple, so we unfold it first */
+      Constraintlist oldcl = solvecons;
+      cl = constraintlistDuplicate (solvecons);
+      cl =
+	constraintlistAdd (cl,
+			   makeConstraint (deVar (activeco->term)->op1,
+					   activeco->know));
+      cl =
+	constraintlistAdd (cl,
+			   makeConstraint (deVar (activeco->term)->op2,
+					   activeco->know));
+      solvecons = cl;
+      flag = solve (sp, solvecons) || flag;
+      constraintlistDestroy (solvecons);
+      solvecons = oldcl;
+      if (flag && sp.solution == NULL)
+	return 1;
+    }
+  else
+    {
+      /* not a tuple. does it unify? */
+
+      //TODO or remove: termNormalize(activeco->term);
+      void examine (Termlist tl)
+      {
+	Termlist tlres, tlscan;
+	int goodsubst;
+
+	while (tl != NULL)
+	  {
+	    //TODO or remove: termNormalize(tl->term);
+	    tlres = termMguTerm (activeco->term, tl->term);
+
+	    /* check whether this is a valid
+	     * substitution */
+	    goodsubst = 1;
+	    tlscan = tlres;
+	    while (tlscan != NULL && tlres != MGUFAIL)
+	      {
+		if (validSubst (sp.sys->match, tlscan->term))
+		  {
+		    tlscan = tlscan->next;
+		  }
+		else
+		  {
+		    goodsubst = 0;
+		    tlscan = NULL;
+		  }
+	      }
+	    if (tlres != MGUFAIL && goodsubst)
+	      {
+		/* maybe this has modified current and previous knowledge! */
+		/* modify and copy _all_ knowledge instances, if needed, that is
+		   all constraints as well as all agent knowledge! */
+		Constraintlist oldcl = NULL;
+		int copied = 0;
+
+		if (tlres != NULL)
+		  {
+		    copied = 1;
+		    /* sometimes not needed, when no substitutions took place */
+		    oldcl = solvecons;
+		    solvecons = constraintlistDuplicate (solvecons);
+		    Constraintlist cl = solvecons;
+		    while (cl != NULL)
+		      {
+			cl->constraint->know =
+			  knowledgeSubstDo (cl->constraint->know);
+			cl = cl->next;
+		      }
+		  }
+
+		/* explore this new state */
+		flag = solve (sp, solvecons) || flag;
+
+		/* undo changes */
+		if (copied)
+		  {
+		    Constraintlist cl;
+		    cl = solvecons;
+		    while (cl != NULL)
+		      {
+			knowledgeDelete (cl->constraint->know);
+			cl = cl->next;
+		      }
+		    constraintlistDestroy (solvecons);
+		    solvecons = oldcl;
+		    cl = solvecons;
+		    while (cl != NULL)
+		      {
+			knowledgeSubstUndo (cl->constraint->know);
+			cl = cl->next;
+		      }
+		  }
+
+	      }
+	    else
+	      {
+		/* unification failed */
+	      }
+
+	    if (tlres != MGUFAIL)
+	      {
+		tlscan = tlres;
+		while (tlscan != NULL)
+		  {
+		    tlscan->term->subst = NULL;
+		    tlscan = tlscan->next;
+		  }
+		termlistDelete (tlres);
+	      }
+
+	    /* abort if necessary */
+	    if (flag && sp.solution == NULL)
+	      return;
+
+	    tl = tl->next;
+	  }
+      }
+
+      examine (activeco->know->basic);
+      if (flag && sp.solution == NULL)
+	return 1;
+      examine (activeco->know->encrypt);
+      if (flag && sp.solution == NULL)
+	return 1;
+
+      if (isTermEncrypt (activecl->constraint->term))
+	{
+	  /* shouldn't this be a branch? TODO */
+
+	  Constraintlist oldcl = solvecons;
+	  cl = constraintlistDuplicate (oldcl);
+	  cl =
+	    constraintlistAdd (cl,
+			       makeConstraint (activeco->term->op,
+					       activeco->know));
+	  cl =
+	    constraintlistAdd (cl,
+			       makeConstraint (activeco->term->key,
+					       activeco->know));
+	  solvecons = cl;
+	  flag = solve (sp, solvecons) || flag;
+	  constraintlistDestroy (solvecons);
+	  solvecons = oldcl;
+	  if (flag && sp.solution == NULL)
+	    return 1;
+	}
+    }
+
+  /* relink detached link */
+  if (beforecl == NULL)
+    {
+      solvecons = constraintlistConcat (activecl, solvecons);
+    }
+  else
+    {
+      activecl->prev = beforecl;
+      activecl->next = beforecl->next;
+      beforecl->next = activecl;
+      if (activecl->next != NULL)
+	activecl->next->prev = activecl;
+    }
+  return flag;
+}
+
+
+int
+matchRead_clp (const System sys, const int run, int (*proceed) (System, int))
+{
+  Constraintlist oldcl, newcl;
+  Constraint co;
+  Roledef runPoint;
+  int flag;
+
+
+  /* save old state */
+  oldcl = sys->constraints;
+  newcl = constraintlistShallow (oldcl);
+
+  /* creat new state */
+  runPoint = runPointerGet (sys, run);
+
+  /* we know this is a read */
+  co = makeConstraint (runPoint->message, sys->know);
+  newcl = constraintlistAdd (newcl, co);
+  sys->constraints = newcl;
+
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      constraintlistPrint (newcl);
+    }
+#endif
+
+  /* check solvability */
+  int solution (const struct solvepass sp, const Constraintlist cl)
+  {
+    Knowledge oldknow = NULL;
+    Constraintlist oldcl = sys->constraints;
+    int flag = 0;
+    int copied = 0;
+
+    sys->constraints = cl;
+    if (knowledgeSubstNeeded (sys->know))
+      {
+	copied = 1;
+	oldknow = sys->know;
+	sys->know = knowledgeSubstDo (sys->know);
+      }
+    flag = sp.proceed (sys, run);
+    if (copied)
+      {
+	knowledgeDelete (sys->know);
+	sys->know = oldknow;
+	knowledgeSubstUndo (sys->know);
+      }
+    sys->constraints = oldcl;
+    return flag;
+  }
+
+  struct solvepass sp;
+  sp.solution = solution;
+  sp.sys = sys;
+  sp.run = run;
+  sp.proceed = proceed;
+  flag = solve (sp, sys->constraints);
+
+  /* restore memory allocation */
+  constraintDestroy (co);
+  constraintlistDelete (newcl);
+  sys->constraints = oldcl;
+
+  return flag;
+}
+
+int
+enabled_clp (const System sys, const int run)
+{
+  return 1;
+}
+
+int
+block_clp (const System sys, const int run)
+{
+  return 1;
+}
+
+int
+secret_clp (const System sys, const Term t)
+{
+  Constraintlist oldcl, newcl;
+  Constraint co;
+  int flag;
+
+  /* save old state */
+  oldcl = sys->constraints;
+  newcl = constraintlistShallow (oldcl);
+
+  /* we know this is a read */
+  co = makeConstraint (t, sys->know);
+  newcl = constraintlistAdd (newcl, co);
+  sys->constraints = newcl;
+
+  /* check solvability */
+
+  struct solvepass sp;
+  sp.solution = NULL;
+  sp.sys = sys;
+  flag = !solve (sp, sys->constraints);
+
+  /* restore memory allocation */
+  constraintDestroy (co);
+  constraintlistDelete (newcl);
+  sys->constraints = oldcl;
+
+  return flag;
+}
+
+void
+sendAdd_clp (const System sys, const int run, const Termlist tl)
+{
+  Term t;
+  Termlist tl2;
+
+  if (tl == NULL)
+    {
+      /* TODO because the constraints might have changed, we can try to solve them again... */
+      explorify (sys, run);
+      return;
+    }
+  t = deVar (tl->term);
+  if (realTermLeaf (t))
+    {
+      /* leaf: simply add it */
+      knowledgeAddTerm (sys->know, t);
+      sendAdd_clp (sys, run, tl->next);
+      return;
+    }
+  else
+    {
+      /* node */
+      if (realTermTuple (t))
+	{
+	  /* tuple */
+	  tl2 = termlistShallow (tl->next);
+	  tl2 = termlistAdd (tl2, t->op1);
+	  tl2 = termlistAdd (tl2, t->op2);
+	  sendAdd_clp (sys, run, tl2);
+	  termlistDelete (tl2);
+	}
+      else
+	{
+	  /* encrypt */
+	  Term invkey;
+
+	  invkey = inverseKey (sys->know->inverses, t->key);
+	  if (!hasTermVariable (invkey))
+	    {
+	      /* simple case: no variable inside */
+	      knowledgeAddTerm (sys->know, t);
+	      tl2 = termlistShallow (tl->next);
+	      if (inKnowledge (sys->know, invkey) && hasTermVariable (t->op))
+		tl2 = termlistAdd (tl2, t->op);
+	      sendAdd_clp (sys, run, tl2);
+	      termlistDelete (tl2);
+	    }
+	  else
+	    {
+	      /* difficult case: variable in inverse
+	       * key. We have to branch. */
+
+	      /* branch 1 : invkey not in knowledge */
+	      /* TODO this yields a negative constraint, which we omit for the time being */
+	      Knowledge oldknow = knowledgeDuplicate (sys->know);
+
+	      knowledgeAddTerm (sys->know, t);
+	      sendAdd_clp (sys, run, tl->next);
+
+	      knowledgeDelete (sys->know);
+	      sys->know = oldknow;
+
+	      /* branch 2 : invkey in knowledge */
+	      oldknow = knowledgeDuplicate (sys->know);
+	      Constraintlist clold = sys->constraints;
+	      Constraintlist clbuf = constraintlistShallow (clold);
+	      tl2 = termlistShallow (tl->next);
+
+	      Constraint co = makeConstraint (invkey, sys->know);
+	      sys->constraints = constraintlistAdd (clbuf, co);
+	      /* we _could_ explore first if this is solveable */
+	      knowledgeAddTerm (sys->know, t);
+	      tl2 = termlistAdd (tl2, t->op);
+	      sendAdd_clp (sys, run, tl2);
+
+	      termlistDelete (tl2);
+	      constraintDestroy (co);
+	      constraintlistDelete (clbuf);
+	      sys->constraints = clold;
+	      knowledgeDelete (sys->know);
+	      sys->know = oldknow;
+	    }
+	}
+    }
+}
+
+int
+send_clp (const System sys, const int run)
+{
+  Roledef rd = runPointerGet (sys, run);
+  /* execute send, push knowledge? */
+  if (inKnowledge (sys->know, rd->message))
+    {
+      /* no new knowledge, so this remains */
+      explorify (sys, run);
+    }
+  else
+    {
+      /* new knowledge, must store old state */
+      Knowledge oldknow;
+      oldknow = sys->know;
+      sys->know = knowledgeDuplicate (sys->know);
+
+      Termlist tl = termlistAdd (NULL, rd->message);
+      sendAdd_clp (sys, run, tl);
+      termlistDelete (tl);
+
+      knowledgeDelete (sys->know);
+      sys->know = oldknow;
+    }
+  return 1;
+}
+
+int
+isPossible_clp (const System sys, const int run, int
+		(*proceed) (System, int), const Term t, const Knowledge k)
+{
+  Constraintlist oldcl, newcl;
+  Constraint co;
+  Roledef runPoint;
+  int flag;
+
+  /* save old state */
+  oldcl = sys->constraints;
+  newcl = constraintlistShallow (oldcl);
+
+  /* creat new state */
+  runPoint = runPointerGet (sys, run);
+
+  /* add the new constraint */
+  co = makeConstraint (t, k);
+  newcl = constraintlistAdd (newcl, co);
+  sys->constraints = newcl;
+
+  /* check solvability */
+  int solution (const struct solvepass sp, const Constraintlist cl)
+  {
+    Knowledge oldknow = NULL;
+    Constraintlist oldcl = sys->constraints;
+    int flag = 0;
+    int copied = 0;
+
+    sys->constraints = cl;
+    if (knowledgeSubstNeeded (sys->know))
+      {
+	copied = 1;
+	oldknow = sys->know;
+	sys->know = knowledgeSubstDo (sys->know);
+      }
+    flag = sp.proceed (sys, run);
+    if (copied)
+      {
+	knowledgeDelete (sys->know);
+	sys->know = oldknow;
+	knowledgeSubstUndo (sys->know);
+      }
+    sys->constraints = oldcl;
+    return flag;
+  }
+
+  struct solvepass sp;
+  sp.solution = solution;
+  sp.sys = sys;
+  sp.run = run;
+  sp.proceed = proceed;
+  flag = solve (sp, sys->constraints);
+
+  /* restore memory allocation */
+  constraintDestroy (co);
+  constraintlistDelete (newcl);
+  sys->constraints = oldcl;
+
+  return flag;
+}
diff --git a/src/match_clp.h b/src/match_clp.h
new file mode 100644
index 0000000..dae1660
--- /dev/null
+++ b/src/match_clp.h
@@ -0,0 +1,13 @@
+#ifndef MATCHCLP
+#define MATCHCLP
+
+#include "runs.h"
+
+int matchRead_clp (const System sys, const int run,
+		   int (*proceed) (System, int));
+int enabled_clp (const System sys, const int run);
+int block_clp (const System sys, const int run);
+int secret_clp (const System sys, const Term t);
+int send_clp (const System sys, const int run);
+
+#endif
diff --git a/src/memory.c b/src/memory.c
new file mode 100644
index 0000000..9a8881d
--- /dev/null
+++ b/src/memory.c
@@ -0,0 +1,48 @@
+/* my own memory functions (not yet) */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <malloc.h>
+#include <mcheck.h>
+#include "memory.h"
+#include "debug.h"
+
+/* for displaying the sizes */
+
+#include "terms.h"
+#include "termlists.h"
+#include "knowledge.h"
+#include "substitutions.h"
+#include "runs.h"
+
+void
+memInit ()
+{
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      void sp (char *txt, int size)
+      {
+	printf ("Size of %s : %i\n", txt, size);
+      }
+      printf ("Data structure size.\n\n");
+      sp ("pointer", sizeof (Term));
+      sp ("term node", sizeof (struct term));
+      sp ("termlist node", sizeof (struct termlist));
+      sp ("knowledge node", sizeof (struct knowledge));
+      sp ("substituition node", sizeof (struct substitution));
+      sp ("substlist node", sizeof (struct substitutionlist));
+      sp ("roledef node", sizeof (struct roledef));
+      sp ("system node", sizeof (struct system));
+      printf ("\n");
+    }
+  mtrace ();
+#endif
+  return;
+}
+
+void
+memDone (int sw)
+{
+  return;
+}
diff --git a/src/memory.h b/src/memory.h
new file mode 100644
index 0000000..e8aa199
--- /dev/null
+++ b/src/memory.h
@@ -0,0 +1,14 @@
+#ifndef MEMORY
+#define MEMORY
+
+#include "string.h"
+#include "debug.h"
+#include <malloc.h>
+
+void memInit ();
+void memDone ();
+#define memAlloc(t) malloc(t)
+#define memFree(p,t) free(p)
+#define memRealloc(p,t) realloc(p,t);
+
+#endif
diff --git a/src/mgu.c b/src/mgu.c
new file mode 100644
index 0000000..b7b67f4
--- /dev/null
+++ b/src/mgu.c
@@ -0,0 +1,151 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "terms.h"
+#include "termlists.h"
+#include "substitutions.h"
+#include "mgu.h"
+#include "memory.h"
+
+/*
+   Most General Unifier
+
+   Unification etc.
+
+   New version yields a termlist with substituted variables, which can later be reset to NULL.
+*/
+
+void
+termlistSubstReset (Termlist tl)
+{
+  while (tl != NULL)
+    {
+      tl->term->subst = NULL;
+      tl = tl->next;
+    }
+}
+
+Termlist
+termMguTerm (Term t1, Term t2)
+{
+  /* added for speed */
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+  if (t1 == t2)
+    return NULL;
+
+#ifdef DEBUG
+  void showSubst (Term t)
+  {
+    if (!DEBUGL (5))
+      return;
+
+    indent ();
+    printf ("Substituting ");
+    termPrint (t);
+    printf (", typed ");
+    termlistPrint (t->stype);
+    printf ("->");
+    termlistPrint (t->subst->stype);
+    printf ("\n");
+  }
+#endif
+
+  if (!(hasTermVariable (t1) || hasTermVariable (t2)))
+    {
+      if (isTermEqual (t1, t2))
+	{
+	  return NULL;
+	}
+      else
+	{
+	  return MGUFAIL;
+	}
+    }
+
+  /* symmetrical tests for single variable */
+  if (isTermVariable (t1))
+    {
+      if (termOccurs (t2, t1))
+	return MGUFAIL;
+      else
+	{
+	  t1->subst = t2;
+#ifdef DEBUG
+	  showSubst (t1);
+#endif
+	  return termlistAdd (NULL, t1);
+	}
+    }
+  if (isTermVariable (t2))
+    {
+      if (termOccurs (t1, t2))
+	return MGUFAIL;
+      else
+	{
+	  t2->subst = t1;
+#ifdef DEBUG
+	  showSubst (t2);
+#endif
+	  return termlistAdd (NULL, t2);
+	}
+    }
+
+  /* left & right are compounds with variables */
+  if (t1->type != t2->type)
+    return MGUFAIL;
+
+  /* identical compounds */
+  /* encryption first */
+  if (isTermEncrypt (t1))
+    {
+      Termlist tl1, tl2;
+
+      tl1 = termMguTerm (t1->key, t2->key);
+      if (tl1 == MGUFAIL)
+	{
+	  return MGUFAIL;
+	}
+      else
+	{
+	  tl2 = termMguTerm (t1->op, t2->op);
+	  if (tl2 == MGUFAIL)
+	    {
+	      termlistSubstReset (tl1);
+	      termlistDelete (tl1);
+	      return MGUFAIL;
+	    }
+	  else
+	    {
+	      return termlistConcat (tl1, tl2);
+	    }
+	}
+    }
+
+  /* tupling second
+     non-associative version ! TODO other version */
+  if (isTermTuple (t1))
+    {
+      Termlist tl1, tl2;
+
+      tl1 = termMguTerm (t1->op1, t2->op1);
+      if (tl1 == MGUFAIL)
+	{
+	  return MGUFAIL;
+	}
+      else
+	{
+	  tl2 = termMguTerm (t1->op2, t2->op2);
+	  if (tl2 == MGUFAIL)
+	    {
+	      termlistSubstReset (tl1);
+	      termlistDelete (tl1);
+	      return MGUFAIL;
+	    }
+	  else
+	    {
+	      return termlistConcat (tl1, tl2);
+	    }
+	}
+    }
+  return MGUFAIL;
+}
diff --git a/src/mgu.h b/src/mgu.h
new file mode 100644
index 0000000..e278723
--- /dev/null
+++ b/src/mgu.h
@@ -0,0 +1,12 @@
+#ifndef MGU
+#define MGU
+
+#include "terms.h"
+#include "termlists.h"
+#include "substitutions.h"
+
+#define MGUFAIL (Termlist) -1
+
+Termlist termMguTerm (Term t1, Term t2);
+
+#endif
diff --git a/src/modelchecker.c b/src/modelchecker.c
new file mode 100644
index 0000000..4f8c5e1
--- /dev/null
+++ b/src/modelchecker.c
@@ -0,0 +1,1171 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <limits.h>
+#include "substitutions.h"
+#include "knowledge.h"
+#include "runs.h"
+#include "debug.h"
+#include "modelchecker.h"
+#include "report.h"
+#include "memory.h"
+#include "match_basic.h"
+#include "match_clp.h"
+#include "output.h"
+#include "tracebuf.h"
+#include "attackminimize.h"
+
+/*
+
+	A model checker. Really.
+*/
+
+extern Term CLAIM_Secret;
+extern Term CLAIM_Nisynch;
+
+/*
+   Some forward declarations.
+*/
+
+int traverseSimple (const System oldsys);
+int traverseNonReads (const System oldsys);
+int traversePOR (const System oldsys);
+int traversePOR2 (const System oldsys);
+int traversePOR2b (const System oldsys);
+int traversePOR3 (const System oldsys);
+int traversePOR4 (const System oldsys);
+int propertyCheck (const System sys);
+int executeTry (const System sys, int run);
+int claimSecrecy (const System sys, const Term t);
+int violateClaim (const System sys, int length, int claimev, Termlist reqt);
+Termlist secrecyUnfolding (Term t, const Knowledge know);
+
+/*
+   Main code.
+*/
+
+void
+statePrint (const System sys)
+{
+  int i, s;
+  Roledef rd;
+
+  indent ();
+  printf ("state %i: ", sys->step);
+  for (i = 0; i < sys->maxruns; i++)
+    {
+      s = 0;
+      rd = runPointerGet (sys, i);
+      while (rd != NULL)
+	{
+	  rd = rd->next;
+	  s++;
+	}
+      printf ("%i ", s);
+    }
+  printf (" - phase %i, done %i", sys->PORphase, sys->PORdone);
+  printf ("\n");
+}
+
+int
+traverse (const System sys)
+{
+  /* branch for traversal methods */
+  switch (sys->traverse)
+    {
+    case 1:
+      return traverseSimple (sys);
+    case 2:
+      return traverseNonReads (sys);
+    case 3:
+    case 4:
+      return traversePOR (sys);
+    case 5:
+      return traversePOR2 (sys);
+    case 6:
+      return traversePOR3 (sys);
+    case 7:
+      return traversePOR2b (sys);
+    case 8:
+      return traversePOR4 (sys);
+    default:
+      debug (2, "This is NOT an existing traversal method !");
+      exit (1);
+    }
+}
+
+/*
+ * executeStep
+ *
+ * Does not really execute anything, it's just bookkeeping, progressing
+ * counters and such.
+ *
+ * If it returns TRUE, explore. If false, don't traverse.
+ */
+
+int
+executeStep (const System sys, const int run)
+{
+  Roledef runPoint;
+  runPoint = runPointerGet (sys, run);
+#ifdef DEBUG
+  if (DEBUGL (3))
+    {
+      indent ();
+      printf ("exec: ");
+      roledefPrint (runPoint);
+      printf ("#%i\n", run);
+    }
+#endif
+  runPointerSet (sys, run, runPoint->next);
+
+
+  /* store knowledge for this step */
+  (sys->step)++;
+  sys->traceKnow[sys->step] = sys->know;
+
+  /* check for properties */
+  propertyCheck (sys);
+
+  /* set indent for printing */
+  indentSet (sys->step);
+  /* hmmm, but what should it return if not exploring? */
+  if (!sys->explore)
+    return 0;
+
+  /* we want to explore it, but are we allowed by pruning? */
+  if (sys->step >= sys->maxtracelength)
+    {
+      /* cut off traces that are too long */
+#ifdef DEBUG
+      if (DEBUGL (4))
+	{
+	  indent ();
+	  printf ("trace cut off.\n");
+	  if (DEBUGL (5))
+	    {
+	      (sys->step)--;
+	      tracePrint (sys);
+	      (sys->step)++;
+	    }
+	}
+#endif
+      return 0;
+    }
+
+  /* we will explore this state, so count it. */
+  /* ulong was _not_ enough... */
+  if (++sys->statesLow == ULONG_MAX)
+    {
+      sys->statesLow = 0;
+      sys->statesHigh++;
+      /* No test for overflow statesHigh. If stuff gets that fast, then 
+       * I surely hope the max of ulong is set higher in the language def */
+    }
+
+  /* show progression */
+  if (sys->switchS > 0)
+    {
+      if (sys->statesLow % (long int) sys->switchS == 0)
+	{
+	  indent ();
+	  statesPrint (sys);
+	}
+    }
+  return 1;
+}
+
+/*
+ * explorify
+ *
+ * grandiose naming scheme (c) sjors dubya.
+ * explores the system state given by the next step of a run.
+ */
+
+int
+explorify (const System sys, const int run)
+{
+  Roledef rd;
+  int flag;
+
+  rd = runPointerGet (sys, run);
+  if (rd == NULL)
+    {
+      printf ("ERROR: trying to progress completed run!\n");
+      exit (1);
+    }
+
+  if (executeStep (sys, run))
+    {
+      flag = traverse (sys);
+    }
+  else
+    {
+      flag = 0;
+    }
+  runPointerSet (sys, run, rd);
+  sys->step--;
+  indentSet (sys->step);
+  return flag;
+}
+
+int
+traverseSimple (const System sys)
+{
+  /* simple nondeterministic traversal */
+
+  int run;
+  int flag = 0;
+
+  for (run = 0; run < (sys->maxruns); run++)
+    {
+      if (runPointerGet (sys, run) != NULL)
+	{
+	  flag = 1;
+	  executeTry (sys, run);
+	}
+    }
+  if (!flag)
+    {
+      /* trace was not succesful */
+    }
+  return flag;
+}
+
+/*
+ * nonReads
+ *
+ * Do a certain type of action first, i.e. that which satisfies nonRead(System,
+ * Roledef). Use the inverse of this predicate to detect the other type of
+ * event.
+ */
+
+#define predRead(sys,rd)	( rd->type == READ && !rd->internal )
+#define isRead(sys,rd)		( rd != NULL && predRead(sys,rd) )
+#define nonRead(sys,rd)		( rd != NULL && !predRead(sys,rd) )
+
+int
+nonReads (const System sys)
+{
+  /* all sends first, then simple nondeterministic traversal */
+
+  int run;
+  Roledef rd;
+
+  /* check for existence of executable sends */
+  for (run = 0; run < (sys->maxruns); run++)
+    {
+      rd = runPointerGet (sys, run);
+      if (nonRead (sys, rd))
+	{
+	  executeTry (sys, run);
+	  return 1;
+	}
+    }
+  return 0;
+}
+
+int
+traverseNonReads (const System sys)
+{
+  if (nonReads (sys))
+    return 1;
+  else
+    return traverseSimple (sys);
+}
+
+int
+traversePOR (const System sys)
+{
+  int flag = 0;
+  int phase = sys->PORphase;
+  int done = sys->PORdone;
+  Roledef rd;
+
+  if (phase == -1)
+    {
+      /* if we did nothing in the previous scan, this does not
+         add anything new, and we exit. */
+      if (done == 0)
+	return 0;
+
+      if (nonReads (sys))
+	{
+	  return 1;
+	}
+      else
+	{
+	  sys->PORphase = 0;
+	  sys->PORdone = 0;
+	  flag = traversePOR (sys);
+	  sys->PORphase = phase;
+	  sys->PORdone = done;
+          return flag;
+	}
+    }
+  else
+    {
+      /* other phase: branch the reads */
+
+      if (phase == 0)
+	{
+	  /* phase 0: init the relevant counters */
+	  sys->PORdone = 0;
+	  flag = 0;
+	}
+
+      (sys->PORphase)++;
+      if (sys->PORphase == sys->maxruns)
+	{
+	  sys->PORphase = -1;
+	}
+
+      rd = runPointerGet (sys, phase);
+      if (isRead (sys, rd))
+	{
+	  /* consider both possibilities */
+
+	  /* empty branch test */
+	  if (sys->PORphase != -1 || sys->PORdone == 1)
+	    {
+	      /* apparently we have already done something,
+	       * so we can consider _not_ doing this read */
+
+	      /* option 1: we do not execute the event */
+
+#ifdef DEBUG
+	      if (DEBUGL (5))
+		{
+		  indent ();
+		  printf
+		    ("We are not executing a non-send event in phase %i\n",
+		     phase);
+		}
+#endif
+	      switch (sys->clp)
+		{
+		case 0:
+		  flag = block_basic (sys, phase);
+		  break;
+		case 1:
+		  flag = block_clp (sys, phase);
+		  break;
+		default:
+		  printf ("Non existing clp switch.\n");
+		  exit (1);
+		}
+	    }
+
+	  /* option 2: we do execute the event */
+
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      indent ();
+	      printf
+		("We are actually executing a non-send event in phase %i\n",
+		 phase);
+	    }
+#endif
+	  sys->PORdone = 1;	// mark that we did (try) stuff
+	  flag = executeTry (sys, phase);
+	}
+      else
+	{
+	  /* empty branch test */
+	  if (sys->PORphase != -1 || sys->PORdone == 1)
+	    {
+	      /* something else or null, proceed with scan */
+	      flag = traverse (sys);
+	    }
+	}
+      sys->PORdone = done;
+      sys->PORphase = phase;
+      return flag;
+    }
+}
+
+/*
+ * POR2b
+ *
+ * currently -t7
+ *
+ * New partial order reduction, which ought to be much more intuitive.
+ */
+
+int
+traversePOR2b (const System sys)
+{
+  Roledef runPoint;
+  int flag = 0;
+  int phase = sys->PORphase;
+  int done = sys->PORdone;
+
+  if (phase == -1)
+    {
+      /* if we did nothing in the previous scan, this does not
+         add anything new, and we exit. */
+      if (done == 0)
+	{
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      indent ();
+	      printf
+		("Read branch had no executed reads in phase %i, pruning tree.\n",
+		 phase);
+	    }
+#endif
+	  return 0;
+	}
+
+      /* nonReads first, as long as they exist */
+
+      if (nonReads (sys))
+	{
+	  /* there was a nonread executed, branches itself */
+	  return 1;
+	}
+      else
+	{
+	  /* no more nonreads, go to next phase */
+
+	  sys->PORphase = 0;
+	  sys->PORdone = 0;
+	  flag = traverse (sys);
+	  sys->PORdone = done;
+	  sys->PORphase = phase;
+	  return flag;
+	}
+    }
+  else
+    {
+      /* other phase: branch the reads */
+
+      (sys->PORphase)++;
+      if (sys->PORphase == sys->maxruns)
+	{
+	  sys->PORphase = -1;
+	}
+
+      runPoint = runPointerGet (sys, phase);
+      if (isRead (sys, runPoint))
+	{
+
+	  /* A read, we were looking for one of those.  Consider
+	   * both possibilities */
+
+	  /* option A. Try to execute the event */
+
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      indent ();
+	      printf ("We are actually executing a read event in phase %i\n",
+		      phase);
+	    }
+#endif
+	  sys->PORdone++;
+	  flag = executeTry (sys, phase);
+	  sys->PORdone--;
+
+	  /* option B. Not execute now */
+
+	  if (!flag)
+	    {
+	      /* It did not work now, so we try it later */
+#ifdef DEBUG
+	      if (DEBUGL (5))
+		{
+		  indent ();
+		  printf ("Postponing a failed read in phase %i\n", phase);
+		}
+#endif
+
+	      flag = traverse (sys);
+	    }
+	  else
+	    {
+	      /* It worked. Will the situation change later
+	       * however?  Surely only if there was a
+	       * variable involved, we might try it later */
+
+	      if (hasTermVariable (runPoint->message))
+		{
+		  /* It has a variable, so we might try
+		   * it later, but _only_ with different
+		   * knowledge */
+
+#ifdef DEBUG
+		  if (DEBUGL (5))
+		    {
+		      indent ();
+		      printf
+			("Postponing a read for later ideas in phase %i\n",
+			 phase);
+		    }
+#endif
+		  if (!sys->clp)
+		    {
+		      /* non-clp */
+		      flag = block_basic (sys, phase);
+		    }
+		  else
+		    {
+		      /* clp */
+		      flag = block_clp (sys, phase);
+		    }
+		}
+	      else
+		{
+		  /* no more hope */
+#ifdef DEBUG
+		  if (DEBUGL (5))
+		    {
+		      indent ();
+		      printf ("No more hope in phase %i.\n", phase);
+		    }
+#endif
+		}
+	    }
+
+	}
+      else
+	{
+	  /* it is not a read. this actually should mean the role is empty */
+
+	  /* something else or null, proceed with scan */
+	  flag = traverse (sys);
+	}
+
+      /* reset phase counter */
+      sys->PORphase = phase;
+      return flag;
+    }
+}
+
+int
+traversePOR2 (const System sys)
+{
+  Roledef runPoint;
+  int flag = 0;
+  int phase = sys->PORphase;
+  int done = sys->PORdone;
+
+  if (phase == -1)
+    {
+      /* if we did nothing in the previous scan, this does not
+         add anything new, and we exit. */
+      if (sys->PORdone == 0)
+	return 0;
+
+      if (nonReads (sys))
+	{
+	  return 1;
+	}
+      else
+	{
+	  sys->PORphase = 0;
+	  sys->PORdone = 0;
+	  flag = traversePOR2 (sys);
+	  sys->PORphase = phase;
+	  sys->PORdone = done;
+	  return flag;
+	}
+    }
+  else
+    {
+      /* other phase: branch the reads */
+
+      if (phase == 0)
+	{
+	  /* phase 0: init the relevant counters */
+	  sys->PORdone = 0;
+	  flag = 0;
+	}
+
+      (sys->PORphase)++;
+      if (sys->PORphase == sys->maxruns)
+	{
+	  sys->PORphase = -1;
+	}
+
+      runPoint = runPointerGet (sys, phase);
+
+      if (isRead (sys, runPoint))
+	{
+	  /* empty branch test */
+	  if (sys->PORphase != -1 || sys->PORdone == 1)
+	    {
+	      /* option 1: we do not execute the event */
+
+#ifdef DEBUG
+	      if (DEBUGL (5))
+		{
+		  indent ();
+		  printf
+		    ("We are not executing a non-send event in phase %i\n",
+		     phase);
+		}
+#endif
+	      switch (sys->clp)
+		{
+		case 0:
+
+		  /* the idea is, that if the
+		   * read has no variables, and
+		   * is enabled already, it makes
+		   * no sense to delay it any
+		   * longer. */
+
+		  if (hasTermVariable (runPoint->message))
+		    {
+		      /* original case */
+		      flag = block_basic (sys, phase);
+		    }
+		  else
+		    {
+		      /* check whether it was enabled already */
+		      /* HACK this is a custom 'enabled' test. */
+		      /* TODO rewrite this, we don't want such a test. */
+		      if (!inKnowledge (sys->know, runPoint->message))
+			{
+			  /* not enabled yet, so we might want to do so later */
+			  flag = block_basic (sys, phase);
+			}
+		      else
+			{
+			  /* enabled, skipping */
+			}
+		    }
+		  break;
+		case 1:
+		  flag = block_clp (sys, phase);
+		  break;
+		default:
+		  printf ("Non existing clp switch.\n");
+		  exit (1);
+		}
+	    }
+
+	  /* option 2: we do execute the event */
+
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      indent ();
+	      printf
+		("We are actually executing a non-send event in phase %i\n",
+		 phase);
+	    }
+#endif
+	  sys->PORdone = 1;	// mark that we did (try) stuff
+	  flag = executeTry (sys, phase);
+	}
+      else
+	{
+	  /* empty branch test */
+	  if (sys->PORphase != -1 || sys->PORdone == 1)
+	    {
+	      /* something else or null, proceed with scan */
+	      flag = traverse (sys);
+	    }
+	}
+      sys->PORdone = done;
+      sys->PORphase = phase;
+      return flag;
+    }
+}
+
+int
+traversePOR3 (const System sys)
+{
+  Roledef rd;
+  int flag;
+  int run;
+
+  if (nonReads (sys))
+    {
+      return 1;
+    }
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      rd = runPointerGet (sys, run);
+      if (rd != NULL)
+	{
+	  /* option 1: just execute it */
+
+	  flag = executeTry (sys, run);
+
+	  /* option 2: if it worked, and its a read... */
+
+	  if (flag)
+	    {
+	      if (rd->type == READ &&
+		  !(rd->internal) && hasTermVariable (rd->message))
+		{
+
+		  /* option 2a: worked, but also execute
+		   * it later if we thinks that's
+		   * different actually only relevant for
+		   * non internal reads */
+
+		  /* TODO consider option for global
+		   * 'sendsTodo' counter, because if
+		   * there are zero left, this is not
+		   * required. */
+
+#ifdef DEBUG
+		  if (DEBUGL (5))
+		    {
+		      indent ();
+		      printf ("Blocking read for run #%i.\n", run);
+		    }
+#endif
+		  block_basic (sys, run);
+		}
+	      return 1;
+	    }
+	}
+    }
+  return 0;
+}
+
+/*
+ * POR4
+ *
+ * This is the simplified version of the algorithm, to be compared with
+ * the -t7 version.
+ *
+ * Based on some new considerations.
+ */
+
+int
+traversePOR4 (const System sys)
+{
+  Roledef rd;
+  int flag = 0;
+  int run;
+  int i;
+  int offset;
+
+  /* Previously we did the sends first. This does not always improve things,
+   * depending on the protocol.
+   */
+  // if (nonReads (sys)) return 1;
+
+  /* a choice for choose */
+
+  /* The 'choose' implemented here is the following:
+   *
+   * choose ev#rid
+   * where rid = min(r: ev#r in enabled(sys): (r-lastrun) mod maxruns)
+   * and where lastrun is the runid of the previous event 
+   * in the trace, or 0 if there was none.
+   */
+  if (sys->step == 0)
+    {
+      /* first step, start at 0 */
+      offset = 0;
+    }
+  else
+    {
+      /* there was a previous action, start scan from there */
+      offset = sys->traceRun[sys->step - 1] + sys->porparam;
+    }
+
+  /* Try all events (implicitly we only handle enabled ones) starting with our
+   * first choice.  If one was chosen, flag is set, and the loop aborts. */
+  for (i = 0; i < sys->maxruns && !flag; i++)
+    {
+      run = (i + offset) % sys->maxruns;
+      rd = runPointerGet (sys, run);
+
+      if (rd != NULL)
+	{
+	  switch (rd->type)
+	    {
+	    case CLAIM:
+	    case SEND:
+	      executeTry (sys, run);
+	      flag = 1;
+	      break;
+
+	    case READ:
+	      /* the sendsdone check only prevent
+	       * some unneccessary inKnowledge tests,
+	       * and branch tests, still improves
+	       * about 15% */
+	      if (sys->knowPhase > rd->knowPhase)
+		{
+		  /* apparently there has been a new knowledge item since the
+		   * previous check */
+
+		  /* implicit check for enabledness */
+		  flag = executeTry (sys, run);
+
+		  /* if it was enabled (flag) we postpone it if it makes sense
+		   * to do so (hasVariable, non internal) */
+		  if (flag && hasTermVariable (rd->message) && !rd->internal)
+		    {
+		      int stackKnowPhase = rd->knowPhase;
+
+		      rd->knowPhase = sys->knowPhase;
+		      if (sys->clp)
+			{
+			  block_clp (sys, run);
+			}
+		      else
+			{
+			  block_basic (sys, run);
+			}
+		      rd->knowPhase = stackKnowPhase;
+		    }
+		}
+	      break;
+
+	    default:
+	      printf ("Encountered unknown event type %i.\n", rd->type);
+	      exit (1);
+	    }
+	}
+    }
+  return flag;
+}
+
+
+int
+propertyCheck (const System sys)
+{
+  int flag = 1;	// default: properties are true, no attack 
+
+  /* for now, we only check secrecy */
+  if (sys->secrets != NULL)
+    {
+      Termlist scan;
+      scan = sys->secrets;
+      while (scan != NULL)
+	{
+	  if (!claimSecrecy (sys, scan->term))
+	    {
+	      /* apparently, secrecy of this term was violated */
+	      /* find the violated claim event */
+
+	      Termlist tl = NULL;
+	      int claimev = -1;
+	      int i = 0;
+
+	      while (claimev == -1 && i <= sys->step)
+		{
+		  if (sys->traceEvent[i]->type == CLAIM &&
+		      sys->traceEvent[i]->to == CLAIM_Secret)
+	 	    {
+		      Termlist tl = secrecyUnfolding(scan->term, sys->know);
+		      if (tl != NULL)
+		        {
+		          /* This was indeed a violated claim */
+			  claimev = i;
+		        }
+		    }
+		  i++;
+		}
+	      /* do we have it? */
+	      if (claimev == -1)
+		{
+		  /* weird, should not occur */
+		  printf("A secrecy claim was supposed to be violated on term ");
+		  termPrint(scan->term);
+		  printf(" but we couldn't find the corresponding claim.\n");
+		  exit(1);
+		}
+	      else
+		{
+		  /* fine. so it's violated */
+		  violateClaim(sys, sys->step, claimev, tl);
+		  termlistDelete(tl);
+		  flag = 0;
+		}
+	    }
+	  scan = scan->next;
+	}
+
+    }
+  return flag;
+}
+
+/*	true iff the term is secret */
+
+int
+isTermSecret (const System sys, const Term t)
+{
+  switch (sys->clp)
+    {
+    case 0:
+      /* test for simple inclusion */
+      if (inKnowledge (sys->know, t))
+	return 0;
+      if (isTermVariable (t))
+	{
+	  /* it's a variable! */
+
+	  /* TODO that does not necessarily mean we can choose it, does
+	   * it?  NO: the rule should be: there is at least one message
+	   * in knowledge. We don't check it currently.*/
+
+	  return 0;
+	}
+      return 1;
+    case 1:
+      /* CLP stuff */
+      return secret_clp (sys, t);
+    default:
+      return 0;
+    }
+}
+
+/*	true iff the claim is valid */
+
+int
+claimSecrecy (const System sys, const Term t)
+{
+  int csScan (Term t)
+  {
+    t = deVar (t);
+    if (isTermTuple (t))
+      return csScan (t->op1) && csScan (t->op2);
+    else
+      return isTermSecret (sys, t);
+  }
+
+  if (csScan (t))
+    return 1;
+  else
+    {
+      /* Not reported anymore here, but only at the end */
+      // reportSecrecy (sys, t);
+      return 0;
+    }
+}
+
+/*
+ * Unfold the secrecy tuple and construct a list of terms that violate it.
+ */
+
+Termlist
+secrecyUnfolding (Term t, const Knowledge know)
+{
+  t = deVar (t);
+  if (isTermTuple (t))
+    return termlistConcat (secrecyUnfolding(t->op1,know),
+			   secrecyUnfolding(t->op2,know)
+			  );
+  else
+    {
+      if (inKnowledge(know, t))
+	  return termlistAdd(NULL, t);
+      else
+	  return NULL;
+    }
+}
+
+/*
+ * for reporting we need a more detailed output of the claims.
+ * Output is a termlist pointer, or -1.
+ *
+ * in: claim roledef, knowledge for which it is violated
+ *
+ * -1	: claim was ignored
+ * NULL : claim is fulfilled (true)
+ * Termlist: claim was violated, termlist terms are know to the intruder.
+ */
+
+Termlist
+claimViolationDetails (const System sys, const int run, const Roledef rd, const Knowledge know)
+{
+  if (rd->type != CLAIM)
+    {
+      printf("Trying to determine details of something other than a claim!\n");
+      exit(-1);
+    }
+
+  /* cases */
+  if (rd->to == CLAIM_Secret)
+    {
+      /* secrecy claim */
+      
+      if (untrustedAgent (sys, sys->runs[run].agents))
+	{
+	  /* claim was skipped */
+	  return (Termlist) -1;
+	}
+      else
+	{
+	  /* construct violating subterms list */
+          return secrecyUnfolding(rd->message, know);
+	}
+    }
+  return NULL;
+}
+
+/* This happens when we violate a claim.
+ * Lots of administration.
+ * Returns true iff explorify is in order.
+ */
+
+int
+violateClaim (const System sys, int length, int claimev, Termlist reqt)
+{
+  int flag;
+
+  /* default = no adaption of pruning, continue search */
+  flag = 1;
+
+  /* Count the violations */
+  sys->failed++;
+
+  /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */
+  if (sys->attack == NULL || length < sys->attack->reallength)
+    {
+      tracebufDone(sys->attack);
+      sys->attack = tracebufSet(sys, length, claimev);
+      attackMinimize (sys, sys->attack);
+      sys->shortestattack = sys->attack->reallength;
+
+      /* maybe there is some new pruning going on */
+      flag = 0;
+      switch (sys->prune)
+	{
+	case 0:
+	  flag = 1;
+	  break;
+	case 1:
+	  break;
+	case 2:
+	  sys->maxtracelength = sys->shortestattack - 1;
+	  break;
+	} 
+    }
+  return flag;
+}
+
+int
+executeTry (const System sys, int run)
+{
+  Roledef runPoint;
+  int flag = 0;
+
+  runPoint = runPointerGet (sys, run);
+  sys->traceEvent[sys->step] = runPoint;	// store for later usage, problem: variables are substituted later...
+  sys->traceRun[sys->step] = run;	// same
+
+  if (runPoint == NULL)
+    {
+#ifdef DEBUG
+      /* warning, ought not to occur */
+      debug (2, "Trying to activate completed run");
+#endif
+    }
+  else
+    {
+#ifdef DEBUG
+      if (DEBUGL (4))
+	{
+	  indent ();
+	  printf ("try: ");
+	  roledefPrint (runPoint);
+	  printf ("#%i\n", run);
+	}
+#endif
+      if (runPoint->type == READ)
+	{
+	  if (sys->clp)
+	    return matchRead_clp (sys, run, explorify);
+	  else
+	    return matchRead_basic (sys, run, explorify);
+	}
+      if (runPoint->type == SEND)
+	{
+	  if (sys->clp)
+	    flag = send_clp (sys, run);
+	  else
+	    flag = send_basic (sys, run);
+	  return flag;
+	}
+      if (runPoint->type == CLAIM)
+	{
+
+	  /* first we might dynamically determine whether the claim is valid */
+	  if (untrustedAgent (sys, sys->runs[run].agents))
+	    {
+	      /* for untrusted agents we check no claim violations at all
+	       * so: we know it's okay. */
+	      /* TODO for CLP this doesn't work and call for branching, if the
+	       * agent is a variable */
+#ifdef DEBUG
+	      if (DEBUGL (3))
+		{
+		  indent ();
+		  printf ("Skipped claim in untrusted run with agents ");
+		  termlistPrint (sys->runs[run].agents);
+		  printf ("\n");
+		}
+#endif
+	      explorify (sys, run);
+	      return 1;
+	    }
+
+	  /* determine type of claim, and parameters */
+#ifdef DEBUG
+	  if (DEBUGL (2))
+	    {
+	      indent ();
+	      printf ("claim: ");
+	      roledefPrint (runPoint);
+	      printf ("#%i\n", run);
+	    }
+#endif
+	  sys->claims++;
+
+	  if (runPoint->to == CLAIM_Secret)
+	    {
+	      /* TODO claims now have their own type, test for that */
+	      /* TODO for now it is secrecy of the message */
+
+	      Termlist oldsecrets = sys->secrets;
+	      /* TODO this can be more efficient, by filtering out double occurrences */
+	      sys->secrets =
+		termlistAdd (termlistShallow (oldsecrets), runPoint->message);
+	      flag = claimSecrecy (sys, runPoint->message);
+
+	      /* now check whether the claim failed for further actions */
+	      if (!flag)
+		{
+		  /* violation */
+		  Termlist tl;
+
+		  tl = claimViolationDetails(sys,run,runPoint,sys->know);
+		  if (violateClaim (sys,sys->step+1, sys->step, tl ))
+		      flag = explorify (sys, run);
+		  termlistDelete(tl);
+		}
+	      else
+		{
+		  /* no violation */
+		  flag = explorify (sys, run);
+		}
+
+	      /* reset secrets list */
+	      termlistDelete (sys->secrets);
+	      sys->secrets = oldsecrets;
+	    }
+	  if (runPoint->to == CLAIM_Nisynch)
+	    {
+	      /* TODO nisynch implementation */
+	    }
+	}
+      /* a claim always succeeds */
+      flag = 1;
+    }
+  return flag;
+}
+
diff --git a/src/modelchecker.h b/src/modelchecker.h
new file mode 100644
index 0000000..0579b55
--- /dev/null
+++ b/src/modelchecker.h
@@ -0,0 +1,6 @@
+int traverse (const System oldsys);
+int explorify (const System sys, const int run);
+int executeStep (const System sys, const int run);
+int propertyCheck (const System sys);
+Termlist claimViolationDetails (const System sys, const int run, const Roledef
+		rd, const Knowledge know);
diff --git a/src/notes.txt b/src/notes.txt
new file mode 100644
index 0000000..8fe408a
--- /dev/null
+++ b/src/notes.txt
@@ -0,0 +1,76 @@
+- best heuristic currently for -t8: ignore sendsfirst, just look at the
+  previous event and continue at that run.
+- termPrint must currently be encapsulated in a math environment to work in
+  latex output, I wil change this later to some ensure mathmode construct,
+  probably with something like latexTermPrint.
+- Repository to apache2 webdav.
+- The trace incremental search should start at something like 'distance of
+  first claim + SOMECONST * runs'. SOMECONST relates to the partial-order
+  induced trace prolonings.
+- For now, CLP is non-working and not checked. Reconsider this later.
+- Because the properties checked are related to the partial order reductions,
+  it makes sense to check 'all secrecy claims' or 'all synchronisation claims'
+  at once.
+- Once an attack is generated, we know the actual scenario and the trace
+  length. We might re-use this information to generate the shortest attack
+  using no partial order reduction.  Note that choosing a wise method of
+  finding that is a mathematical issue: searching -t1 is exponential, so how
+  do we step trough these traces in order to find the shortest trace in the
+  quickest way? This can be determined under some (statistical) assumptions.
+- The incremental check can be done much easier, by just retrying the main
+  loop explore with different parameters. It keeps everything nicely intact.
+  We must check for fails however, and how pruning is affected.
+- Incremental check can at least be done in two ways: either by limiting the
+  number of runs (big axe method) or by limiting the trace length (nice).
+  There is a drawback to trace length only: the superfluous sends of the
+  algorithm in a scenario with many runs might interfere with the usefulness
+  of short traces. Maybe some heuristic that reduces the runs automatically is
+  required. (e.g. 'number of runs is at most MaxTraceLength/MaxRoleLength' or
+  something like that). Do analysis.
+- If synch checking is expensive, introduce a limit (for -p0 stuff).
+  Basically, after the limit (if -p0 is set), we stop checking synch claims.
+  This then is default behaviour, to be overridden or changed by a switch.
+- clp does not yet consider the matching for variables that have not been
+  instantiated. This *might* lead to some improvement, e.g. when there is only
+  one candidate for the variable. In general, I don't think it will help.
+- match_clp.c 1.25 introduced the variable_in_invkey brancher, which hasn't
+  been thoroughly tested yet. Please do test.
+- Brutus is slower than -t4. CLP is much, much faster however than both.
+- It is very important to have variables in the run agent list, because it
+  dramatically decreases the complexity of the system, as opposed to just
+  creating runs for all possibilities. However, this explicitly introduces the
+  clp problem of var encryptions (see above).
+- Given originator assumptions and such, we might want to implement the
+  compiler, that for non-typed matching, it will ignore all type definitions
+  in the code (as in, putting them in stype, but still considering Function).
+  Then, for 'any agent' we can use stype silently. The modelchecker should
+  then always consider the types with -m0 and -m1.
+- In a paper concerning the CASRUL compiler, they mention associativity for
+  the equality relations.  Note that CASRUL restricts the intruder actions,
+  and sometimes uses approximations.
+- MS and CE never mention associativity as a restriction.
+- For now, clp stuff will use pairing and simple mgu. Maybe a -m3 switch will
+  add the associative variant later.
+- MALLOC_TRACE is the environment variable that triggers mtrace() output.
+- Several memory leak detectors are still in place, they can all be located by
+  searching for "lead" or "diff" and destroying the code.
+- knowledgeAddTerm might be improved by scanning through key list only with
+  things that are newly added.
+- Associativity and unification don't play together well; consider other
+  algorithms. Maybe a simple explore (x,y),z and explore x,(y,z) will do, e.g.
+  take any split point for both sequences.
+- POR (-t3) is actually worse than -t2: sends first. After some pondering I
+  now know why. It's because simultaneous reads yield traces in which there
+  are attacks that are also in the ones where we have R0S0S0;R1 (i.e. is thus
+  equivalent with R0;R1;S0S0)
+- Knowledge is monotonous. So, if we say 'R#0' cannot be triggered by some
+  knowledge, we can just use a pointer for it. If we do want to trigger it, we
+  need to compare two knowledge pointers. As they don't have a unique
+  representation, it is more difficult. For now, I will just forbid specific
+  branches of the read when a message is in some previous knowledge, which is
+  more precise.
+- Comparisons with Casper are in order.
+- It is a good idea to have any number of input files, and parse them all, to
+  combine scenarios. A command should be "require <file>", because that would
+  enable scenarios to load the required role definitions. It's require instead
+  of include, because of possible multiple occurrences.
diff --git a/src/output.c b/src/output.c
new file mode 100644
index 0000000..e6e1d8a
--- /dev/null
+++ b/src/output.c
@@ -0,0 +1,443 @@
+/*
+ * output.c
+ *
+ * Outputs an attack.
+ * Currently, every attack is printed.
+ * TODO move attacks to a buffer, and print _only_ the shortest one.
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include "runs.h"
+#include "latex.h"
+
+
+void linePrint(int i)
+{
+    indent();
+    while (i > 0) {
+	printf("--------");
+	i--;
+    }
+    printf("\n");
+}
+
+int correspondingSend(System sys, int rd)
+{
+
+    int labelMatch = 0;
+    int toMatch = 0;
+    int fromMatch = 0;
+    int tofromMatch = 0;
+    int messageMatch = 0;
+    int nMatches = 0;
+    int maxNMatches = 0;
+
+    int readEvent = rd;
+    int sendEvent = -1;
+    int bestSendEvent = -1;
+
+    for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) {
+	if (sys->traceEvent[sendEvent]->type == SEND) {
+	    /* do all the different kind of matchings first */
+
+	    labelMatch =
+		isTermEqualFn(sys->traceEvent[sendEvent]->label,
+			      sys->traceEvent[readEvent]->label);
+	    toMatch =
+		isTermEqualFn(sys->traceEvent[sendEvent]->to,
+			      sys->traceEvent[readEvent]->to);
+	    fromMatch =
+		isTermEqualFn(sys->traceEvent[sendEvent]->from,
+			      sys->traceEvent[readEvent]->from);
+	    tofromMatch = toMatch || fromMatch;
+	    messageMatch =
+		isTermEqualFn(sys->traceEvent[sendEvent]->message,
+			      sys->traceEvent[readEvent]->message);
+
+	    /* calculate the score */
+
+	    nMatches = labelMatch + tofromMatch + messageMatch;
+
+	    if (nMatches == 3) {
+		/* bingo! success on all matches */
+
+		//printf("Found perfect match: %d\n", s);
+		bestSendEvent = sendEvent;
+		break;
+	    }
+	    if (nMatches > maxNMatches) {
+		/* if we found a better candidate than we already had, we'll update */
+
+		//printf("Comparing SEND #%d: ",s);
+		//if (labelMatch) printf("label ");
+		//if (toMatch) printf("to ");
+		//if (fromMatch) printf("from ");
+		//if (messageMatch) printf("message ");
+		//printf("\n");
+
+		/* however, we first want to be sure that at least some matches are successful */
+
+		if (labelMatch && messageMatch) {
+		    /* strongest restriction: message and label should match */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+
+		} else if (messageMatch) {
+		    /* if label AND message don't match: */
+		    /* at least message should match */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+		} else if (labelMatch) {
+		    /* if message doesn't match */
+		    /* the label should matches */
+
+		    maxNMatches = nMatches;
+		    bestSendEvent = sendEvent;
+		}
+		//printf("Best match: %d  maxNMatches: %d\n", s, maxNMatches);
+	    }
+	}
+    }
+
+    //bestSendEvent = NULL;
+    if (bestSendEvent == -1) {
+	/*Termlist tl;
+	   Term t;
+
+	   //newtl = knowledgeNew(sys->traceKnow[i],sys->traceKnow[i+1]);
+
+	   for (tl = sys->traceKnow[rd]->basic; tl != NULL; tl = tl->next)
+	   {
+	   t = tl->term;
+	   termPrint(t);
+	   printf(" - ");
+	   }
+	   printf("\n");
+	   for (tl = sys->traceKnow[rd]->encrypt; tl != NULL; tl = tl->next)
+	   {
+	   t = tl->term;
+	   termPrint(t);
+	   printf(" - ");
+	   }
+	   printf("\n");
+	   for (tl = sys->traceKnow[rd]->inverses; tl != NULL; tl = tl->next)
+	   {
+	   t = tl->term;
+	   termPrint(t);
+	   printf(" - ");
+	   }
+	   printf("\n"); */
+
+	int u;
+
+	for (u = 0; u < rd; u++) {
+	    if (sys->traceEvent[u]->type == SEND) {
+
+
+		//termPrint(readEvent->message);
+		//printf("\n");
+		knowledgePrint(sys->traceKnow[u]);
+		//printf("Is received message in knowledge after SEND %d? %d\n", u, inKnowledge(sys->traceKnow[u+1],readEvent->message));
+		if (inKnowledge
+		    (sys->traceKnow[u + 1],
+		     sys->traceEvent[readEvent]->message)) {
+		    bestSendEvent = u;
+		    break;
+		}
+	    }
+	}
+    }
+
+    if (bestSendEvent == -1) {
+	printf("!! Could not find a matching SEND\n");
+    } else {
+	//latexMessagePrint(sys, bestSendEvent, readEvent);
+	//printf("Latex: ");
+	//termPrint(bestSendEvent->from);
+	//printf(" -> ");
+	if (!isTermEqualFn
+	    (sys->traceEvent[bestSendEvent]->to,
+	     sys->traceEvent[readEvent]->to)) {
+	    //termPrint(bestSendEvent->to);
+	    //printf(" -> ");
+	}
+	if (!isTermEqualFn
+	    (sys->traceEvent[bestSendEvent]->from,
+	     sys->traceEvent[readEvent]->from)) {
+	    //termPrint(readEvent->from);
+	    //printf(" -> ");
+	}
+	//termPrint(readEvent->to);
+	//printf("\n");
+    }
+    return bestSendEvent;
+}
+
+void tracePrint(System sys)
+{
+    if (sys->latex) {
+	//latexTracePrint(sys);
+	return;
+    }
+
+    int i, j;
+    int lastrid;
+    int width;
+    Termlist newtl;
+
+    /* fix the 'next' knowledge, this is required because sometimes
+     * when calling this function, the next knowledge is not stored
+     * yet, but required for the general form of the output . */
+
+    sys->traceKnow[sys->step + 1] = sys->know;
+
+
+    /* how wide is the trace? */
+    width = 0;
+    for (i = 0; i <= sys->step; i++) {
+	if (sys->traceRun[i] >= width)
+	    width = sys->traceRun[i] + 1;
+    }
+
+    linePrint(width);
+    indent();
+    printf("Dumping trace:\n");
+    linePrint(width);
+
+    /* first some parameter issues */
+
+    knowledgePrint(sys->traceKnow[0]);
+    /* also print inverses */
+    indent();
+    printf("Inverses: ");
+    knowledgeInversesPrint(sys->traceKnow[0]);
+    printf("\n");
+
+    /* Trace columns header.  First the run identifier and role.  On the
+     * second line we have the perceived agents for each partner role.
+     * These are printed in the same order as the role specification in the
+     * protocol. */
+
+    linePrint(width);
+    indent();
+
+    for (i = 0; i < width; i++) {
+	termPrint(sys->runs[i].role->nameterm);
+	printf("#%i\t", i);
+    }
+    printf("\n");
+    for (i = 0; i < width; i++) {
+	termPrint(agentOfRun(sys, i));
+	printf("\t");
+    }
+    printf("\n");
+
+    for (i = 0; i < width; i++) {
+	agentsOfRunPrint(sys, i);
+	printf("\t");
+    }
+    printf("\n");
+
+    /* now we print the actual trace */
+
+    void sticks(int i) {
+	while (i > 0) {
+	    printf("|\t");
+	    i--;
+	}
+    }
+
+    void sticksLine(void) {
+	sticks(width);
+	printf("\n");
+    }
+
+    linePrint(width);
+    lastrid = -1;
+    for (i = 0; i <= sys->step; i++) {
+	/* yields extra newlines between switching of runs */
+
+	j = sys->traceRun[i];
+	if (j != lastrid) {
+	    sticksLine();
+	    lastrid = j;
+	}
+
+	/* print the actual event */
+
+	indent();
+	sticks(j);
+	roledefPrint(sys->traceEvent[i]);
+
+	//if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal)
+	//{
+	/* calls routine to find the best SEND-candidate */
+	/* the result is not yet being used */
+
+	//      printf("\n");
+	//      correspondingSend(sys, i);
+	//}
+
+	/* have we learnt anything new? */
+	newtl = knowledgeNew(sys->traceKnow[i], sys->traceKnow[i + 1]);
+	if (newtl != NULL) {
+	    printf("\n");
+	    sticksLine();
+	    sticks(width);
+	    printf("/* Intruder learns ");
+	    termlistPrint(newtl);
+	    termlistDelete(newtl);
+	    printf(" */");
+	    lastrid = -1;
+	}
+
+	/* new line */
+	printf("\n");
+    }
+
+    switch (sys->clp) {
+    case 1:
+	indent();
+	printf("---[ constraints ]-----\n");
+	constraintlistPrint(sys->constraints);
+	break;
+    default:
+	break;
+    }
+    linePrint(width);
+}
+
+
+
+void attackDisplayAscii(System sys)
+{
+    int i, j;
+    int length;
+    int lastrid;
+    int width;
+    Termlist newtl;
+    struct tracebuf *tb;
+
+    /* attack trace buffer */
+    tb = sys->attack;
+    length = sys->attack->length;
+
+    /* set variables */
+    varbufSet (sys, tb->variables);
+
+    /* how wide is the trace? */
+    width = 0;
+    for (i = 0; i < length; i++) {
+	if (tb->run[i] >= width)
+	    width = tb->run[i] + 1;
+    }
+
+    linePrint(width);
+    indent();
+    printf("Dumping trace:\n");
+    linePrint(width);
+
+    /* first some parameter issues */
+
+    knowledgePrint(tb->know[0]);
+    printf ("Variables: ");
+    termlistPrint (sys->variables);
+    printf ("\n");
+
+    /* Trace columns header.  First the run identifier and role.  On the
+     * second line we have the perceived agents for each partner role.
+     * These are printed in the same order as the role specification in the
+     * protocol. */
+
+    linePrint(width);
+    indent();
+
+    for (i = 0; i < width; i++) {
+	termPrint(sys->runs[i].role->nameterm);
+	printf("#%i\t", i);
+    }
+    printf("\n");
+    for (i = 0; i < width; i++) {
+	termPrint(agentOfRun(sys, i));
+	printf("\t");
+    }
+    printf("\n");
+
+    for (i = 0; i < width; i++) {
+	agentsOfRunPrint(sys, i);
+	printf("\t");
+    }
+    printf("\n");
+
+    /* now we print the actual trace */
+
+    void sticks(int i) {
+	while (i > 0) {
+	    printf("|\t");
+	    i--;
+	}
+    }
+
+    void sticksLine(void) {
+	sticks(width);
+	printf("\n");
+    }
+
+    linePrint(width);
+    lastrid = -1;
+    for (i = 0; i < length; i++) {
+	/* yields extra newlines between switching of runs */
+
+	j = tb->run[i];
+	if (j != lastrid) {
+	    sticksLine();
+	    lastrid = j;
+	}
+
+	/* print the actual event */
+
+	indent();
+	sticks(j);
+	roledefPrint(tb->event[i]);
+
+	//if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal)
+	//{
+	/* calls routine to find the best SEND-candidate */
+	/* the result is not yet being used */
+
+	//      printf("\n");
+	//      correspondingSend(sys, i);
+	//}
+
+	/* have we learnt anything new? */
+	newtl = knowledgeNew(tb->know[i], tb->know[i + 1]);
+	if (newtl != NULL) {
+	    printf("\n");
+	    sticksLine();
+	    sticks(width);
+	    printf("/* Intruder learns ");
+	    termlistPrint(newtl);
+	    termlistDelete(newtl);
+	    printf(" */");
+	    lastrid = -1;
+	}
+
+	/* new line */
+	printf("\n");
+    }
+
+    linePrint(width);
+}
+
+
+void attackDisplay(System sys)
+{
+    if (sys->latex) {
+	attackDisplayLatex(sys);
+    } else {
+	attackDisplayAscii(sys);
+    }
+}
diff --git a/src/output.h b/src/output.h
new file mode 100644
index 0000000..ef69124
--- /dev/null
+++ b/src/output.h
@@ -0,0 +1,9 @@
+#ifndef OUTPUT
+#define OUTPUT
+
+#include "runs.h"
+
+void tracePrint(System sys);
+void attackDisplay(System sys);
+
+#endif
diff --git a/src/parser.y b/src/parser.y
new file mode 100644
index 0000000..75b0b4b
--- /dev/null
+++ b/src/parser.y
@@ -0,0 +1,281 @@
+%{
+#include "pheading.h"
+#include "scanner.c"
+#include "tac.h"
+
+struct tacnode*	spdltac;
+
+int yyerror(char *s);
+int yylex(void);
+
+%}
+
+%union{
+	char*  		str;
+	struct tacnode*	tac;
+	Symbol		symb;
+}
+
+%token 	<symb>	ID
+%token 		PROTOCOL
+%token 		ROLE
+%token 		READT
+%token 		SENDT
+%token 		CLAIMT
+%token 		VAR
+%token 		CONST
+%token 		RUN
+%token 		SECRET
+%token 		COMPROMISED
+%token 		INVERSEKEYS
+%token 		UNTRUSTED
+%token 		USERTYPE
+
+%type	<tac>	spdlcomplete
+%type	<tac>	spdlrep
+%type	<tac>	spdl
+%type	<tac>	roles
+%type	<tac>	role
+%type	<tac>	roledef
+%type	<tac>	event
+%type	<tac>	declaration
+%type	<tac>	secretpref
+%type	<tac>	typeinfo1
+%type	<tac>	typeinfoN
+%type	<tac>	term
+%type	<tac>	termlist
+%type	<tac>	key
+%type	<tac>	roleref
+
+%type	<symb>	label
+
+%start spdlcomplete
+
+
+%%
+
+spdlcomplete	: spdlrep
+		  {	spdltac = $1; }
+		;
+
+spdlrep		: /* empty */
+		  {	$$ = NULL; }
+		| spdl spdlrep
+		  {	$$ = tacCat($1,$2); }
+		;
+
+spdl		: UNTRUSTED termlist ';'
+		  {	
+		  	Tac t = tacCreate(TAC_UNTRUSTED);
+		  	t->tac1 = $2;
+			$$ = t;
+		  }
+		| RUN roleref '(' termlist ')' ';'
+		  {	
+		  	Tac t = tacCreate(TAC_RUN);
+		  	t->tac1 = $2;
+			t->tac2 = $4;
+			$$ = t;
+		  }
+		| PROTOCOL ID '(' termlist ')' '{' roles '}' optclosing
+	 	  {
+		  	Tac t = tacCreate(TAC_PROTOCOL);
+			t->sym1 = $2;
+			t->tac2 = $7;
+			t->tac3 = $4;
+			$$ = t;
+		  }
+		| USERTYPE termlist ';'
+		  {
+			Tac t = tacCreate(TAC_USERTYPE);
+			t->tac1 = $2;
+			$$ = t;
+		  }
+		| declaration
+		  {
+		  	$$ = $1;
+		  }
+		;
+
+roles		: /* empty */
+       		  {	$$ = NULL; }
+       		| role roles
+		  {	$$ = tacCat($1,$2); }
+		| declaration roles
+		  {	$$ = tacCat($1,$2); }
+		;
+
+role		: ROLE ID '{' roledef '}' optclosing
+      		  { 
+		  	Tac t = tacCreate(TAC_ROLE);
+			t->sym1 = $2;
+			t->tac2 = $4;
+			$$ = t;
+		  }
+		;
+
+optclosing	: /* empty */
+		  { }
+		| ';'
+		  { }
+		;
+
+roledef		: /* empty */
+		  {	$$ = NULL; }
+		| event roledef
+		  {	$$ = tacCat($1,$2); }
+		| declaration roledef
+		  {	$$ = tacCat($1,$2); }
+		;
+
+event		: READT label '(' termlist ')' ';'
+		  {	Tac t = tacCreate(TAC_READ);
+		  	t->sym1 = $2;
+			/* TODO test here: tac2 should have at least 3 elements */
+			t->tac2 = $4;
+			$$ = t;
+		  }
+		| SENDT label '(' termlist ')' ';'
+		  {	Tac t = tacCreate(TAC_SEND);
+		  	t->sym1 = $2;
+			/* TODO test here: tac2 should have at least 3 elements */
+			t->tac2 = $4;
+			$$ = t;
+		  }
+		| CLAIMT label '(' termlist ')' ';'
+		/* TODO maybe claims should be in the syntax */
+		  {	Tac t = tacCreate(TAC_CLAIM);
+		  	t->sym1 = $2;
+			t->tac2 = $4;
+			$$ = t;
+		  }
+		;
+
+roleref		: ID '.' ID
+		  {	Tac t = tacCreate(TAC_ROLEREF);
+		  	t->sym1 = $1;
+			t->sym2 = $3;
+			$$ = t;
+		  }
+		;
+
+declaration	: secretpref CONST termlist typeinfo1 ';'
+		  {	Tac t = tacCreate(TAC_CONST);
+		  	t->tac1 = $3;
+			t->tac2 = $4;
+			t->tac3 = $1;
+			$$ = t;
+		  }
+		| secretpref VAR termlist typeinfoN ';'
+		  {	Tac t = tacCreate(TAC_VAR);
+		  	t->tac1 = $3;
+			t->tac2 = $4;
+			t->tac3 = $1;
+			$$ = t;
+		  }
+		| SECRET termlist typeinfo1 ';'
+		  {	Tac t = tacCreate(TAC_SECRET);
+		  	t->tac1 = $2;
+			t->tac2 = $3;
+			$$ = t;
+		  }
+		| INVERSEKEYS '(' term ',' term ')' ';'
+		  {	Tac t = tacCreate(TAC_INVERSEKEYS);
+			t->tac1 = $3;
+			t->tac2 = $5;
+			$$ = t;
+		  }
+		| COMPROMISED termlist ';'
+		  {	Tac t = tacCreate(TAC_COMPROMISED);
+		  	t->tac1= $2;
+			$$ = t;
+		  }
+		;
+
+secretpref	: /* empty */
+		  {	
+			$$ = NULL;
+		  }
+		| SECRET
+		  {
+			Tac t = tacCreate(TAC_SECRET);
+			$$ = t;
+		  }
+		;
+
+typeinfo1	: /* empty */
+		  {
+		  	Tac t = tacCreate(TAC_UNDEF);
+			$$ = t;
+		  }
+		| ':' ID
+		  {	Tac t = tacCreate(TAC_STRING);
+		  	t->sym1 = $2;
+			$$ = t;
+		  }
+		;
+
+typeinfoN	: /* empty */
+		  {
+		  	Tac t = tacCreate(TAC_UNDEF);
+			$$ = t;
+		  }
+		| ':' termlist
+		  {	
+		  	$$ = $2;
+		  }
+		;
+
+label		: /* empty */
+		  { $$ = NULL; }
+		| '_' ID
+		  { $$ = $2; }
+		;
+
+term  		: ID
+		  {
+		  	Tac t = tacCreate(TAC_STRING);
+			t->sym1 = $1;
+			$$ = t;
+		  }
+		| ID '(' termlist ')'
+		  {
+		  	Tac t = tacCreate(TAC_STRING);
+			t->sym1 = $1;
+			$$ = tacJoin(TAC_ENCRYPT,tacTuple($3),t,NULL);
+		  }
+		| '{' termlist '}' key
+		  {
+		  	$$ = tacJoin(TAC_ENCRYPT,tacTuple($2),$4,NULL);
+		  }
+		| '(' termlist ')'
+		  { 
+		  	$$ = tacTuple($2);
+		  }
+		;
+
+termlist	: term
+		  { }
+		| term ',' termlist
+		  {	$$ = tacCat($1,$3); }
+		;
+
+key		: term
+		  { }
+		;
+
+
+
+%%
+
+// error handler routing
+int yyerror(char *s)
+{
+	extern int yylineno;	// defined and maintained in lex.c
+	extern char *yytext;	// defined and maintained in lex.c
+  
+	printf("\nERROR %s at symbol %s on line %i.\n", s, yytext, yylineno);
+	exit(1);
+}
+
+
diff --git a/src/pheading.h b/src/pheading.h
new file mode 100644
index 0000000..61a084a
--- /dev/null
+++ b/src/pheading.h
@@ -0,0 +1,13 @@
+#ifndef PHEADING
+#define PHEADING
+
+#define YY_NO_UNPUT
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "terms.h"
+#include "termlists.h"
+#include "symbols.h"
+#include "runs.h"
+#include "tac.h"
+#endif
diff --git a/src/releases.txt b/src/releases.txt
new file mode 100644
index 0000000..0b33cf6
--- /dev/null
+++ b/src/releases.txt
@@ -0,0 +1,33 @@
+?		bonk
+	- New partial order reduction method.
+	Maybe CLP/t4
+	maybe MSC stuff
+
+2004-02-19	billionaire
+	- replace substitutions with implicit substitutions.
+	- many syntax updates.
+	- many speed improvements.
+
+2004-01-20	alpha1
+	teehee_valley with a couple of minor bugfixes.
+	- Shows error line correctly on parse.
+	- Allows for multi-line comments.
+
+2004-01-20	teehee_valley
+	Nicely working role-based release, can test stdin scenario files.
+	- Preliminary untrusted support.
+	- Public, inversekeys are working.
+	- No tickets yet.
+
+2004-01-19	amoxicillin	
+	Preliminary compiler test release.
+	- Compiler works in ptest, now we can integrate it into the main
+	  part, and throw out the scenarios.
+	  
+2003		dead_ringers
+	A first working release.
+	- -t0 through -t2 implemented.
+	- Typed matching matches all basic terms.
+	- CLP matching works (-m2), but is not compatible with -t2.
+	- Hard coded protocols, inclusion through Makefile.
+
diff --git a/src/report.c b/src/report.c
new file mode 100644
index 0000000..0ca4a83
--- /dev/null
+++ b/src/report.c
@@ -0,0 +1,75 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "terms.h"
+#include "runs.h"
+#include "debug.h"
+#include "output.h"
+
+extern int globalLatex;
+
+/* reportQuit is called after each violation, because it might need to abort the process */
+void
+reportQuit (System sys)
+{
+  /* determine quit or not */
+  if (sys->prune >= 3)
+    {
+      indent ();
+      printf ("Quitting after %li claims, at the first violated claim.\n",
+	      sys->claims);
+      sys->maxtracelength = 0;
+    }
+}
+
+void
+reportStart (System sys)
+{
+  if (!sys->latex)
+    {
+      indent ();
+      printf ("<REPORT>\n");
+      indent ();
+    }
+  statesPrint (sys);
+}
+
+void
+reportMid (System sys)
+{
+  indent ();
+  printf ("Trace length %i.\n", 1 + sys->step);
+  if (globalLatex)
+      printf("\n");
+  tracePrint (sys);
+}
+
+
+void
+reportEnd (System sys)
+{
+  if (!sys->latex)
+    {
+      indent ();
+      printf ("<REPORT>\n");
+    }
+  reportQuit (sys);
+}
+
+void
+reportSecrecy (System sys, Term t)
+{
+  if (!sys->report)
+    {
+      reportQuit (sys);
+      return;
+    }
+  reportStart (sys);
+  indent ();
+  printf ("Secrecy violation of $");
+  termPrint (t);
+  printf ("$\n");
+  if (globalLatex)
+      printf("\n");
+  reportMid (sys);
+  reportEnd (sys);
+}
diff --git a/src/report.h b/src/report.h
new file mode 100644
index 0000000..27b0e8d
--- /dev/null
+++ b/src/report.h
@@ -0,0 +1,6 @@
+#ifndef REPORT
+#define REPORT
+
+void reportSecrecy (System sys, Term t);
+
+#endif
diff --git a/src/runs.c b/src/runs.c
new file mode 100644
index 0000000..b042ca8
--- /dev/null
+++ b/src/runs.c
@@ -0,0 +1,844 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <limits.h>
+#include "terms.h"
+#include "termlists.h"
+#include "knowledge.h"
+#include "runs.h"
+#include "memory.h"
+#include "constraints.h"
+#include "debug.h"
+#include "output.h"
+#include "tracebuf.h"
+
+/* from compiler.o */
+extern Term TERM_Type;
+
+/* for e.g. termprinting */
+int globalLatex;
+
+static int indentState = 0;
+static int indentDepth = 0;
+
+Run
+makeRun ()
+{
+  return (Run) memAlloc (sizeof (struct run));
+}
+
+Roledef
+makeRoledef ()
+{
+  return (Roledef) memAlloc (sizeof (struct roledef));
+}
+
+System
+systemInit ()
+{
+  System sys = (System) memAlloc (sizeof (struct system));
+
+  /* initially, no trace ofcourse */
+  sys->step = 0;
+  sys->shortestattack = INT_MAX;
+  sys->attack = tracebufInit();
+
+  /* switches */
+  sys->porparam = 0;		// multi-purpose parameter
+  sys->latex = 0;		// latex output?
+
+  /* set illegal traversal by default, to make sure it is set
+     later */
+  sys->traverse = 0;
+  sys->report = 1;
+  sys->switch_maxtracelength = INT_MAX;
+  sys->maxtracelength = INT_MAX;
+
+  /* init rundefs */
+  sys->maxruns = 0;
+  sys->runs = NULL;
+  /* no protocols yet */
+  sys->protocols = NULL;
+  sys->locals = NULL;
+  sys->variables = NULL;
+  sys->untrusted = NULL;
+  sys->secrets = NULL;		// list of claimed secrets
+  sys->attack = NULL;
+
+  /* matching CLP */
+  sys->constraints = NULL;	// no initial constraints
+
+  /* reset global counters */
+  systemReset (sys);
+
+  return sys;
+}
+
+void
+systemReset (const System sys)
+{
+  /* some initial counters */
+  sys->statesLow = 0;		// number of explored states
+  sys->statesHigh = 0;		// this is not as ridiculous as it might seem
+  sys->explore = 1;		// do explore the space
+  sys->claims = 0;		// number of claims encountered
+  sys->failed = 0;		// number of failed claims
+  sys->knowPhase = 0;		// knowledge transition id
+
+  termlistDestroy (sys->secrets);	// remove old secrets list
+  sys->secrets = NULL;		// list of claimed secrets
+
+  /* transfer switches */
+  sys->maxtracelength = sys->switch_maxtracelength;
+
+  /* POR init */
+  sys->PORphase = -1;
+  sys->PORdone = 1;		// mark as 'something done' with previous reads
+
+  /* global latex switch: ugly, but otherwise I must carry it into every
+   * single subprocedure such as termPrint */
+
+  globalLatex = sys->latex;
+}
+
+void
+systemDone (System sys)
+{
+  int run;
+  int s;
+
+  /* clear globals, which were defined in systemStart */
+
+  s = sys->maxtracelength + 1;
+  memFree (sys->traceEvent, s * sizeof (Roledef));
+  memFree (sys->traceRun, s * sizeof (int));
+  memFree (sys->traceKnow, s * sizeof (Knowledge));
+
+  /* clear roledefs */
+  for (run = 0; run < sys->maxruns; run++)
+    roledefDestroy (runPointerGet (sys, run));
+
+  /* clear substructures */
+  termlistDestroy (sys->secrets);
+
+  /* clear main system */
+  systemDestroy (sys);
+}
+
+double
+statesApproximation (System sys)
+{
+  if (sys->statesHigh == 0)
+    return (double) sys->statesLow;
+  else
+    return (double) (sys->statesLow + (sys->statesHigh * ULONG_MAX));
+}
+
+void
+statesPrintShort (System sys)
+{
+  printf ("%.3e", statesApproximation (sys));
+}
+
+void
+statesPrint (System sys)
+{
+  if (sys->statesHigh == 0)
+    {
+      printf ("%g", (double) sys->statesLow);
+    }
+  else
+    {
+      double dstates;
+
+      dstates = sys->statesLow + (sys->statesHigh * ULONG_MAX);
+      printf ("%.3e (...)", dstates);
+    }
+  printf (" states traversed.\n");
+  if (globalLatex)
+      printf("\n");
+}
+
+void
+systemDestroy (System sys)
+{
+  memFree (sys->runs, sys->maxruns * sizeof (struct run));
+  memFree (sys, sizeof (struct system));
+}
+
+/* ensureValidRun
+
+   Makes sure memory is allocated for instantiating this run.
+   Note: This is meant to be used BEFORE using runPointerSet.
+*/
+
+void
+ensureValidRun (System sys, int run)
+{
+  int i, oldsize;
+
+  if (run < sys->maxruns)
+    return;
+
+  /* this amount of memory was not allocated yet */
+  /* (re)allocate  space */
+  /* Note, this is never explicitly freed, because it is never
+     copied */
+
+  sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (run + 1));
+
+  /* update size parameter */
+  oldsize = sys->maxruns;
+  sys->maxruns = run + 1;
+
+  /* create runs, set the new pointer(s) to NULL */
+  for (i = oldsize; i < sys->maxruns; i++)
+    {
+      /* init run */
+      struct run myrun = sys->runs[i];
+      myrun.role = NULL;
+      myrun.agents = NULL;
+      myrun.index = NULL;
+      myrun.start = NULL;
+      myrun.know = knowledgeDuplicate (sys->know);
+    }
+}
+
+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;
+    }
+}
+
+void
+roledefPrint (Roledef rd)
+{
+  if (rd == NULL)
+    {
+      printf ("[Empty roledef]\n");
+      return;
+    }
+  if (rd->type == READ && rd->internal)
+    {
+      /* special case: internal read == choose ! */
+      printf ("CHOOSE(");
+      termPrint (rd->message);
+      printf (")");
+      return;
+    }
+  if (rd->type == READ)
+    printf ("READ");
+  if (rd->type == SEND)
+    printf ("SEND");
+  if (rd->type == CLAIM)
+    printf ("CLAIM");
+  if (rd->label != NULL)
+    {
+      if (globalLatex)
+	{
+	  printf ("$_{");
+	  termPrint (rd->label);
+	  printf ("}$");
+	}
+      else
+	{
+	  printf ("_");
+	  termPrint (rd->label);
+	}
+    }
+  if (globalLatex)
+    printf ("$");
+  printf ("\t(");
+  termPrint (rd->from);
+  printf (",");
+  if (rd->type == CLAIM)
+    printf (" ");
+  termPrint (rd->to);
+  printf (", ");
+  termPrint (rd->message);
+  printf (" )");
+  if (globalLatex)
+    printf ("$");
+}
+
+void
+runPrint (Roledef rd)
+{
+  int i;
+
+  indent ();
+  i = 0;
+  while (rd != NULL)
+    {
+      printf ("%i: ", i);
+      roledefPrint (rd);
+      printf ("\n");
+      i++;
+      rd = rd->next;
+    }
+}
+
+void
+runsPrint (System sys)
+{
+  int i;
+
+  indent ();
+  printf ("[ Run definitions ]\n");
+  for (i = 0; i < (sys->maxruns); i++)
+    {
+      indent ();
+      printf ("Run definition %i:\n", i);
+      runPrint (runPointerGet (sys, i));
+      printf ("\n");
+    }
+}
+
+/*
+ * returns a pointer to the agent name term
+ */
+
+Term
+agentOfRunRole (const System sys, const int run, const Term role)
+{
+  Termlist roles = sys->runs[run].protocol->rolenames;
+  Termlist agents= sys->runs[run].agents;
+
+  /* TODO stupid reversed order, lose that soon */
+  agents = termlistForward(agents);
+  while (agents != NULL && roles != NULL)
+    {
+      if (isTermEqual(roles->term, role))
+	{
+	  return agents->term;
+	}
+      agents = agents->prev;
+      roles = roles->next;
+    }
+  return NULL;
+}
+
+/*
+ * returns a pointer to the agent name term
+ */
+
+Term
+agentOfRun (const System sys, const int run)
+{
+  return agentOfRunRole(sys,run,sys->runs[run].role->nameterm);
+}
+
+Roledef
+roledefDuplicate1 (const Roledef rd)
+{
+  if (rd == NULL)
+    return NULL;
+  Roledef newrd = makeRoledef ();
+  memcpy (newrd, rd, sizeof (struct roledef));
+  newrd->next = NULL;
+  return newrd;
+}
+    
+Roledef
+roledefDuplicate (Roledef rd)
+{
+  if (rd == NULL)
+    return NULL;
+  Roledef newrd = roledefDuplicate1 (rd);
+  newrd->next = roledefDuplicate (rd->next);
+  return newrd;
+}
+
+void
+roledefDelete (Roledef rd)
+{
+  if (rd == NULL)
+    return;
+  roledefDelete (rd->next);
+  memFree (rd, sizeof (struct roledef));
+  return;
+}
+
+void
+roledefDestroy (Roledef rd)
+{
+  if (rd == NULL)
+    return;
+  roledefDestroy (rd->next);
+  termDelete (rd->from);
+  termDelete (rd->to);
+  termDelete (rd->message);
+  memFree (rd, sizeof (struct roledef));
+  return;
+}
+
+/*
+   Instantiate a role by making a new run.
+
+   This involves creation of a new run(id).
+   Copy & subst of Roledef, Agent knowledge.
+   Tolist might contain type constants.
+*/
+
+void
+roleInstance (const System sys, const Protocol protocol, const Role role,
+	      const Termlist paramlist)
+{
+  int rid;
+  Run runs;
+  Roledef rd;
+  Termlist scanfrom, scanto;
+  Termlist fromlist = NULL;
+  Termlist tolist = NULL;
+  Term extterm = NULL;
+
+  /* claim runid, allocate space */
+  rid = sys->maxruns;
+  ensureValidRun (sys, rid);
+  runs = sys->runs;
+
+  /* duplicate roledef in buffer rd */
+  rd = roledefDuplicate (role->roledef);
+
+  /* scan for types in agent list */
+  /* scanners */
+  scanfrom = protocol->rolenames;
+  scanto = paramlist;
+  while (scanfrom != NULL && scanto != NULL)
+    {
+      fromlist = termlistAdd (fromlist, scanfrom->term);
+      if (scanto->term->stype != NULL &&
+	  inTermlist (scanto->term->stype, TERM_Type))
+	{
+	  /* There is a TYPE constant in the parameter list.
+	   * Generate a new local variable for this run, with this type */
+	  Term newvar = makeTermType (VARIABLE, scanfrom->term->symb, rid);
+	  sys->variables = termlistAdd (sys->variables, newvar);
+	  newvar->stype = termlistAdd (NULL, scanto->term);
+	  tolist = termlistAdd (tolist, newvar);
+	  /* newvar is apparently new, but it might occur
+	   * in the first event if it's a read, in which
+	   * case we forget it */
+	  if (!(rd->type == READ && termOccurs (rd->message, scanfrom->term)))
+	    {
+	      /* but this is already set in the first
+	       * read... */
+	      /* TODO scan might be more complex, but
+	       * this will do for now. I.e. occurring
+	       * first in a read will do */
+	      extterm = makeTermTuple (newvar, extterm);
+	    }
+	}
+      else
+	{
+	  /* not a type constant, add to list */
+	  tolist = termlistAdd (tolist, scanto->term);
+	}
+      scanfrom = scanfrom->next;
+      scanto = scanto->next;
+    }
+
+  /* prefix a read for such reads. TODO: this should also cover any external stuff */
+  if (extterm != NULL)
+    {
+      Roledef rdnew;
+
+      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm);
+      /* this is an internal action! */
+      rdnew->internal = 1;
+      rdnew->next = rd;
+      rd = rdnew;
+    }
+
+  /* set parameters */
+  runs[rid].protocol = protocol;
+  runs[rid].role = role;
+  runs[rid].agents = termlistDuplicate (tolist);
+  runs[rid].start = rd;
+  runs[rid].index = rd;
+
+  /* duplicate all locals form this run */
+  scanto = role->locals;
+  while (scanto != NULL)
+    {
+      Term t = scanto->term;
+      if (!inTermlist (fromlist, t))
+	{
+	  if (realTermLeaf (t))
+	    {
+	      Term newt = makeTermType (t->type, t->symb, rid);
+	      if (realTermVariable (newt))
+		{
+	          sys->variables = termlistAdd (sys->variables, newt);
+		}
+	      newt->stype = t->stype;
+	      fromlist = termlistAdd (fromlist, t);
+	      tolist = termlistAdd (tolist, newt);
+	    }
+	}
+      scanto = scanto->next;
+    }
+
+  /* TODO this is not what we want yet, also local knowledge. The local
+   * knowledge (list?) also needs to be substituted on invocation. */
+  runs[rid].know = knowledgeDuplicate (sys->know);
+
+  /* now adjust the local run copy */
+
+  rd = runs[rid].start;
+  while (rd != NULL)
+    {
+      rd->from = termLocal (rd->from, fromlist, tolist, role->locals, rid);
+      rd->to = termLocal (rd->to, fromlist, tolist, role->locals, rid);
+      rd->message =
+	termLocal (rd->message, fromlist, tolist, role->locals, rid);
+      rd = rd->next;
+    }
+  termlistDelete (fromlist);
+  termlistDelete (tolist);
+}
+
+Roledef
+roledefInit (int type, Term label, Term from, Term to, Term msg)
+{
+  Roledef newEvent;
+
+  newEvent = makeRoledef ();
+  newEvent->internal = 0;
+  newEvent->type = type;
+  newEvent->label = label;
+  newEvent->from = from;
+  newEvent->to = to;
+  newEvent->message = msg;
+  newEvent->forbidden = NULL;	// no forbidden stuff
+  newEvent->knowPhase = -1;	// we haven't explored any knowledge yet
+  newEvent->next = NULL;
+  return newEvent;
+}
+
+Roledef
+roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg)
+{
+  Roledef scan;
+
+  if (rd == NULL)
+    return roledefInit (type, label, from, to, msg);
+
+  scan = rd;
+  while (scan->next != NULL)
+    scan = scan->next;
+  scan->next = roledefInit (type, label, from, to, msg);
+  return rd;
+}
+
+
+/* allocate memory for traces, runs have to be known for that */
+
+void
+systemStart (System sys)
+{
+  int i, s;
+  Roledef rd;
+
+  s = 0;
+  for (i = 0; i < sys->maxruns; i++)
+    {
+      rd = runPointerGet (sys, i);
+      while (rd != NULL)
+	{
+	  s++;
+	  rd = rd->next;
+	}
+    }
+
+  /* this is the maximum trace length */
+  if (sys->maxtracelength > s)
+    sys->maxtracelength = s;
+
+  /* trace gets one added entry for buffer */
+  s = sys->maxtracelength + 1;
+
+  /* freed in systemDone */
+  sys->traceEvent = memAlloc (s * sizeof (Roledef));
+  sys->traceRun = memAlloc (s * sizeof (int));
+  sys->traceKnow = memAlloc (s * sizeof (Knowledge));
+
+  /* clear, for niceties */
+  for (i = 0; i < s; i++)
+    {
+      sys->traceEvent[i] = NULL;
+      sys->traceRun[i] = 0;
+      sys->traceKnow[i] = NULL;
+    }
+}
+
+void
+indentActivate ()
+{
+  indentState = 1;
+}
+
+void
+indentSet (int i)
+{
+  if (indentState)
+    indentDepth = i;
+}
+
+void
+indent ()
+{
+  int i = indentDepth;
+  int j = 0;
+  while (i > 0)
+    {
+      printf ("%i  ", j);
+      i--;
+      j++;
+    }
+}
+
+Protocol
+protocolCreate (Term name)
+{
+  Protocol p;
+
+  p = memAlloc (sizeof (struct protocol));
+  p->nameterm = name;
+  p->rolenames = NULL;
+  p->next = NULL;
+  p->roles = NULL;
+  p->locals = NULL;
+  return p;
+}
+
+Role
+roleCreate (Term name)
+{
+  Role r;
+
+  r = memAlloc (sizeof (struct role));
+  r->nameterm = name;
+  r->next = NULL;
+  r->locals = NULL;
+  r->roledef = NULL;
+  return r;
+}
+
+void
+locVarPrint (Termlist tl)
+{
+  if (tl == NULL)
+    {
+      printf ("No local terms.\n");
+    }
+  else
+    {
+      printf ("Local terms: ");
+      printf ("[");
+      while (tl != NULL)
+	{
+	  termPrint (tl->term);
+	  if (tl->term->stype != NULL)
+	    {
+	      printf (":");
+	      termlistPrint (tl->term->stype);
+	    }
+	  tl = tl->next;
+	  if (tl != NULL)
+	    printf (",");
+	}
+      printf ("]");
+      printf ("\n");
+    }
+}
+
+void
+protocolPrint (Protocol p)
+{
+  if (p == NULL)
+    return;
+
+  indent ();
+  printf ("[[Protocol : ");
+  termPrint (p->nameterm);
+  printf (" (");
+  termlistPrint (p->rolenames);
+  printf (")]]\n");
+  locVarPrint (p->locals);
+  rolesPrint (p->roles);
+}
+
+void
+protocolsPrint (Protocol p)
+{
+  while (p != NULL)
+    {
+      protocolPrint (p);
+      p = p->next;
+    }
+}
+
+void
+rolePrint (Role r)
+{
+  if (r == NULL)
+    return;
+
+  indent ();
+  printf ("[[Role : ");
+  termPrint (r->nameterm);
+  printf ("]]\n");
+  locVarPrint (r->locals);
+
+  Roledef rd = r->roledef;
+  while (rd != NULL)
+    {
+      roledefPrint (rd);
+      printf ("\n");
+      rd = rd->next;
+    }
+}
+
+void
+rolesPrint (Role r)
+{
+  if (r == NULL)
+    {
+      printf ("Empty role.");
+    }
+  else
+    {
+      while (r != NULL)
+	{
+	  rolePrint (r);
+	  r = r->next;
+	}
+    }
+}
+
+int
+untrustedAgent (System sys, Termlist agents)
+{
+  while (agents != NULL)
+    {
+      if (isTermVariable (agents->term))
+	{
+	  if (sys->clp)
+	    {
+	      /* clp: variables are difficult */
+	      /* TODO Add as constraint that they're
+	       * trusted */
+	      /* However, that is a branch as well :(
+	       */
+	      /* claim secret is _really_ a instant-multiple
+	       * read. If it is succesful, we sound
+	       * the alert */
+	    }
+	}
+      else
+	{
+	  if (inTermlist (sys->untrusted, agents->term))
+	    return 1;
+	}
+      agents = agents->next;
+    }
+  return 0;
+}
+
+int
+getMaxTraceLength (const System sys)
+{
+  Roledef rd;
+  int maxlen;
+  int run;
+
+  maxlen = 0;
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      rd = runPointerGet (sys, run);
+      while (rd != NULL)
+	{
+	  rd = rd->next;
+	  maxlen++;
+	}
+    }
+  return maxlen;
+}
+
+/*
+ * Nicely format the role and agents we think we're talking to.
+ */
+
+void
+agentsOfRunPrint (const System sys, const int run)
+{
+  Term role = sys->runs[run].role->nameterm;
+  Termlist roles = sys->runs[run].protocol->rolenames;
+
+  termPrint(role);
+  printf("(");
+  while (roles != NULL)
+    {
+      termPrint(agentOfRunRole(sys,run,roles->term));
+      roles = roles->next;
+      if (roles != NULL)
+	{
+	  printf(",");
+	}
+    }
+  printf(")");
+}
+
+/*
+ * explain a violated claim at point i in the trace
+ */
+
+void
+violatedClaimPrint (const System sys, const int i)
+{
+  printf("Claim stuk");
+}
+
+/*
+ * attackLength yields the real (user friendly) length of an attack by omitting
+ * the redundant events but also the choose events.
+ */
+
+int attackLength(struct tracebuf* tb)
+{
+    int len,i;
+
+    len = 0;
+    i = 0;
+    while (i < tb->length)
+    {
+        if (tb->status[i] != S_RED)
+	{
+	    /* apparently not redundant */
+	    if (!(tb->event[i]->type == READ && tb->event[i]->internal))
+	    {
+	        /* and no internal read, so it counts */
+	        len++;
+	    }
+	}
+	i++;
+    }
+    return len;
+}
diff --git a/src/runs.h b/src/runs.h
new file mode 100644
index 0000000..fc41d04
--- /dev/null
+++ b/src/runs.h
@@ -0,0 +1,200 @@
+#ifndef RUNS
+#define RUNS
+
+#include "terms.h"
+#include "termlists.h"
+#include "knowledge.h"
+#include "constraints.h"
+
+#define	READ	1
+#define SEND	2
+#define CLAIM	3
+
+#define runPointerGet(sys,run)		sys->runs[run].index
+#define runPointerSet(sys,run,newp)	sys->runs[run].index = newp
+
+struct roledef
+{
+  /* flag for internal actions (overriding normal type) */
+  int internal;
+  int type;
+  Term label;
+  Term from;
+  Term to;
+  Term message;
+  struct roledef *next;
+
+  /* illegal injections */
+  Knowledge forbidden;
+  /* knowledge transitions counter */
+  int knowPhase;
+
+  /* evt runid for synchronisation, but that is implied in the
+     base array */
+};
+
+typedef struct roledef *Roledef;
+
+
+struct role
+{
+  Term nameterm;
+  Roledef roledef;
+  Termlist locals;
+  struct role *next;
+};
+
+typedef struct role *Role;
+
+struct protocol
+{
+  Term nameterm;
+  Role roles;
+  Termlist rolenames;
+  Termlist locals;
+  struct protocol *next;
+};
+
+typedef struct protocol *Protocol;
+
+struct run
+{
+  Protocol protocol;
+  Role role;
+  Termlist agents;
+  Roledef index;
+  Roledef start;
+  Knowledge know;
+};
+
+typedef struct run *Run;
+
+struct varbuf
+{
+  Termlist	from;
+  Termlist	to;
+  Termlist	empty;
+};
+
+typedef struct varbuf *Varbuf;
+
+struct tracebuf
+{
+  int		length;
+  int		reallength;
+  Roledef	*event;
+  int		*run;
+  int		*status;
+  int		*link;
+  int		violatedclaim;	// index of violated claim in trace
+  Knowledge	*know;
+  Termlist	requiredterms;
+  Varbuf	variables;
+};
+
+struct system
+{
+  int step;			// can be managed globally
+  Knowledge know;
+  struct parameters *parameters;	// misc
+  /* static run info, maxruns */
+  Run runs;
+
+  /* global */
+  int maxruns;
+
+  /* properties */
+  Termlist secrets;		// integrate secrets list into system
+  int shortestattack;		// length of shortest attack trace
+
+  /* switches */
+  int report;
+  int prune;			// type of pruning
+  int switch_maxtracelength;	// helps to remember the length of the last trace
+  int maxtracelength;		// helps to remember the length of the last trace
+  int switchM;			// memory
+  int switchT;			// time
+  int switchS;			// progress (traversed states)
+  int porparam;			// a multi-purpose integer parameter, passed to the partial order reduction method selected
+  int latex;			// latex output switch
+
+  /* traversal */
+  int traverse;			// traversal method
+  int explore;			// boolean: explore states after actions or not
+
+  /* counters */
+  unsigned long int statesLow;
+  unsigned long int statesHigh;
+  unsigned long int claims;	// number of claims encountered
+  unsigned long int failed;	// number of claims failed
+
+  /* matching */
+  int match;			// matching type
+  int clp;			// do we use clp?
+
+  /* protocol definition */
+  Protocol protocols;
+  Termlist locals;
+  Termlist variables;
+  Termlist untrusted;
+
+  /* constructed trace pointers, static */
+  Roledef *traceEvent;		// MaxRuns * maxRoledef
+  int *traceRun;		// MaxRuns * maxRoledef
+  Knowledge *traceKnow;		// Maxruns * maxRoledef
+
+  /* POR reduction assistance */
+  int PORphase;			// -1: init (all sends), 0...: recurse reads
+  int PORdone;			// simple bit to denote something was done.
+  int knowPhase;		// which knowPhase have we already explored?
+  Constraintlist constraints;	// only needed for CLP match
+
+  /* relevant: storage of shortest attack */
+  struct tracebuf* attack;
+};
+
+typedef struct system *System;
+
+System systemInit ();
+void systemReset (const System sys);
+System systemDuplicate (System fromsys);
+void statesPrint (System sys);
+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);
+Term agentOfRunRole (const System sys, const int run, const Term role);
+Term agentOfRun (const System sys, const int run);
+Roledef roledefDuplicate1 (const Roledef rd);
+Roledef roledefDuplicate (Roledef rd);
+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 roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
+		    Term msg);
+void systemStart (System sys);
+void indentActivate ();
+void indentSet (int i);
+void indent ();
+
+Protocol protocolCreate (Term nameterm);
+Role roleCreate (Term nameterm);
+void locVarPrint (Termlist tl);
+void protocolPrint (Protocol p);
+void protocolsPrint (Protocol p);
+void rolePrint (Role r);
+void rolesPrint (Role r);
+int untrustedAgent (System sys, Termlist agents);
+int getMaxTraceLength (const System sys);
+void agentsOfRunPrint (const System sys, const int run);
+void violatedClaimPrint (const System sys, int i);
+int attackLength(struct tracebuf* tb);
+
+#endif
diff --git a/src/scanner.lex b/src/scanner.lex
new file mode 100644
index 0000000..96a541e
--- /dev/null
+++ b/src/scanner.lex
@@ -0,0 +1,160 @@
+%option yylineno
+
+%{
+/* scanner for security protocols language */
+
+#include <strings.h>
+#include "pheading.h"
+#include "memory.h"
+#include "tac.h"
+
+/* tokens for language */
+#include "tok.h"
+
+void mkname(char *name);
+void mkval(void);
+void mktext(void);
+
+int yyerror(char *s);
+
+Symbol mkstring(char *name);
+
+struct stringlist {
+	char*			string;
+	struct stringlist*	next;
+};
+
+typedef struct stringlist* Stringlist;
+
+static Stringlist allocatedStrings = NULL;
+
+
+int mylineno = 0;
+
+%}
+
+comment1	"//".*
+comment2	"#".*
+delimiter	[ \t\n]
+whitespace	{delimiter}+
+uc_letter	[A-Z]
+lc_letter	[a-z]
+letter		{lc_letter}|{uc_letter}
+digit		[0-9]
+ascii_char	[^\"\n]
+escaped_char	\\n|\\\"
+integer		{digit}+
+text		\"({ascii_char}|{escaped_char})*\"
+id		({letter}|{digit})+
+
+%%
+
+"/*"		{
+			register int c;
+
+			for ( ; ; )
+                        {
+                        	while ( (c = input()) != '*' && c != '\n' && c != EOF )
+                                      ;    /* eat up text of comment */
+
+                                if ( c == '*' )
+                                {
+                                	while ( (c = input()) == '*' )
+                                        	;
+                                      	if ( c == '/' )
+                                        	break;    /* found the end */
+                                }
+
+				if (c == '\n')
+					mylineno++;
+
+                                if ( c == EOF )
+                                {
+                                	yyerror( "EOF in comment" );
+                                	break;
+                        	}
+                	}
+                }
+
+\n		{ mylineno++; }
+{whitespace}	{ }
+{comment1}	{ }
+{comment2}	{ }
+
+protocol	{ return PROTOCOL; }
+role		{ return ROLE; }
+read		{ return READT; }
+send		{ return SENDT; }
+var		{ return VAR; }
+const		{ return CONST; }
+claim		{ return CLAIMT; }
+run		{ return RUN; }
+secret		{ return SECRET; }
+inversekeys	{ return INVERSEKEYS; }
+untrusted	{ return UNTRUSTED; }
+compromised	{ return COMPROMISED; }
+usertype	{ return USERTYPE; }
+{id}		{	
+			yylval.symb = mkstring(yytext);
+			return ID;
+		}
+.		{ return yytext[0]; }
+
+
+
+%%
+
+Symbol mkstring(char *name)
+{
+	Symbol t;
+	char* s;
+	Stringlist sl;
+	int len;
+
+	if (( t = lookup(name)) != NULL)
+	{
+		return t;
+	}
+	// make new name
+	len = strlen(name);
+	s = (char *)memAlloc(len+1);
+	sl = (Stringlist) memAlloc(sizeof(struct stringlist));
+	strncpy(s,name,len);
+	sl->next = allocatedStrings;
+	allocatedStrings = sl;
+	sl->string = s;
+	s[len] = EOS;
+
+	t = get_symb();
+	t->lineno = yylineno;
+	t->type = T_UNDEF;
+	t->text = s;
+
+	insert(t);
+	return t;
+}
+
+void scanner_cleanup(void)
+{
+	yy_delete_buffer (YY_CURRENT_BUFFER);
+}
+
+void strings_cleanup(void)
+{
+	Stringlist sl;
+	while (allocatedStrings != NULL)
+	{
+		sl = allocatedStrings;
+		allocatedStrings = sl->next;
+		memFree(sl->string, strlen(sl->string)+1);
+		memFree(sl, sizeof(struct stringlist));
+	}
+}
+
+/*
+void mkval(void);
+void mktext(void);
+*/
+
+
+// vim:ft=lex:
diff --git a/src/speedtest b/src/speedtest
new file mode 100755
index 0000000..3016a40
--- /dev/null
+++ b/src/speedtest
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+./scyther -d -p0 -r 8 $* <spdl/speedtest.spdl
diff --git a/src/substitutions.c b/src/substitutions.c
new file mode 100644
index 0000000..32f96f4
--- /dev/null
+++ b/src/substitutions.c
@@ -0,0 +1,285 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "terms.h"
+#include "substitutions.h"
+#include "memory.h"
+
+/* substitutions in terms */
+
+Substitution
+makeSubstitution (Term from, Term to)
+{
+  Substitution subs;
+
+  subs = memAlloc (sizeof (struct substitution));
+  subs->from = from;
+  subs->to = to;
+  return subs;
+}
+
+void
+substitutionDelete (Substitution subs)
+{
+  if (subs == NULL)
+    return;
+  memFree (subs, sizeof (struct substitution));
+}
+
+void
+substitutionDestroy (Substitution subs)
+{
+  if (subs == NULL)
+    return;
+  termDelete (subs->from);
+  termDelete (subs->to);
+  memFree (subs, sizeof (struct substitution));
+}
+
+
+
+/*
+   termSubstitute
+
+   Yields a new (deep copy) term of a term, according to the
+   substitution.
+
+   To remove the old term, use termDelete.
+   Be sure to use termNormalize on it afterwards!!
+
+*/
+
+
+Term
+termSubstitute (Term term, Substitution subs)
+{
+  if (term == NULL)
+    return NULL;
+  if (isTermEqual (term, subs->from))
+    {
+      return termDuplicate (subs->to);
+    }
+  else
+    {
+      if (!isTermLeaf (term))
+	{
+	  if (isTermEncrypt (term))
+	    {
+	      return makeTermEncrypt (termSubstitute (term->op, subs),
+				      termSubstitute (term->key, subs));
+	    }
+	  else
+	    {
+	      return
+		makeTermTuple (termSubstitute (term->op1, subs),
+			       termSubstitute (term->op2, subs));
+	    }
+	}
+      else
+	{
+	  return termDuplicate (term);
+	}
+    }
+}
+
+/*
+
+   termlistSubstitute.
+
+   Makes a new list, deep copies of the terms. 
+
+   To remove the old termlist, use termlistDestroy
+
+   TODO
+*/
+
+Termlist
+termlistSubstitute (Termlist tl, Substitution subs)
+{
+  if (tl == NULL)
+    return NULL;
+  else
+    {
+      Termlist tls = termlistSubstitute (tl->next, subs);
+      //return termlistAdd(termlistSubstitute(tl->next, subs),
+      //                 termSubstitute(tl->term, subs));
+      return tls;
+    }
+}
+
+
+void
+substitutionPrint (Term t, Substitution subs)
+{
+  printf ("Substituting ");
+  termPrint (subs->from);
+  printf (" by ");
+  termPrint (subs->to);
+  printf (" in ");
+  termPrint (t);
+  printf ("\n");
+}
+
+/* termSubstituteList
+
+   Not very efficient at the moment. Recursing through the term might be
+   a lot easier. However, this works.
+
+*/
+
+Term
+termSubstituteList (Term term, Substitutionlist sl)
+{
+  Term newt;
+  Term oldt;
+
+  if (sl == NULL)
+    return termDuplicate (term);
+  if (term == NULL)
+    return NULL;
+
+  newt = termSubstitute (term, sl->subst);
+  sl = sl->next;
+  while (sl != NULL)
+    {
+      oldt = newt;
+      newt = termSubstitute (oldt, sl->subst);
+      termDelete (oldt);
+      sl = sl->next;
+    }
+  return newt;
+}
+
+Substitutionlist
+makeSubstitutionList (Substitution subs)
+{
+  Substitutionlist sl;
+
+  sl = memAlloc (sizeof (struct substitutionlist));
+  sl->subst = subs;
+  sl->next = NULL;
+  return sl;
+}
+
+Substitutionlist
+substitutionlistAdd (Substitutionlist sl, Term from, Term to)
+{
+  return substitutionlistConcat (sl,
+				 makeSubstitutionList (makeSubstitution
+						       (from, to)));
+}
+
+void
+substitutionlistDestroy (Substitutionlist sl)
+{
+  if (sl != NULL)
+    {
+      substitutionDelete (sl->subst);
+      substitutionlistDestroy (sl->next);
+      memFree (sl, sizeof (struct substitutionlist));
+    }
+}
+
+void
+substitutionlistAnnihilate (Substitutionlist sl)
+{
+  if (sl != NULL)
+    {
+      substitutionDestroy (sl->subst);
+      substitutionlistDestroy (sl->next);
+      memFree (sl, sizeof (struct substitutionlist));
+    }
+}
+
+Substitutionlist
+substitutionlistConcat (Substitutionlist sl1, Substitutionlist sl2)
+{
+  Substitutionlist scan;
+
+  if (sl1 == NULL)
+    return sl2;
+  scan = sl1;
+  while (scan->next != NULL)
+    scan = scan->next;
+  scan->next = sl2;
+  return sl1;
+}
+
+/* substitute over termlist */
+
+Termlist
+substitutionBatch (Termlist tl, Substitutionlist sl)
+{
+  if (tl == NULL)
+    return NULL;
+  if (sl == NULL)
+    return termlistDuplicate (tl);
+  Termlist newtl = NULL;
+  while (tl != NULL)
+    {
+      newtl = termlistAdd (newtl, termSubstituteList (tl->term, sl));
+      tl = tl->next;
+    }
+  return newtl;
+}
+
+/* substitute over roledef */
+
+Roledef
+substitutionRoledef (Roledef rdorig, Substitutionlist sl)
+{
+  Roledef rd, rdscan;
+
+  rd = roledefDuplicate (rdorig);
+  rdscan = rd;
+
+  while (rdscan != NULL)
+    {
+      rdscan->from = termSubstituteList (rdscan->from, sl);
+      rdscan->to = termSubstituteList (rdscan->to, sl);
+      rdscan->message = termSubstituteList (rdscan->message, sl);
+      rdscan = rdscan->next;
+    }
+  return rd;
+}
+
+/* substitute over knowledge structure */
+
+Knowledge
+substitutionKnowledge (Knowledge know, Substitutionlist sl)
+{
+  /* TODO this is wrong anyway, because it does not respect the knowledge invariants. We should remove the variables occurring on
+     the left, and add to the knowledge the new stuff */
+
+  Termlist repres, repres2;
+
+  Knowledge know2 = emptyKnowledge ();
+  knowledgeSetInverses (know2, knowledgeGetInverses (know));
+  repres = knowledgeSet (know);
+  repres2 = substitutionBatch (repres, sl);
+  knowledgeAddTermlist (know2, repres2);
+  termlistDelete (repres2);
+  termlistDelete (repres);
+  return know2;
+}
+
+void
+substitutionlistPrint (Substitutionlist sl)
+{
+  int i = 1;
+
+  if (sl == NULL)
+    printf ("[empty substitutionlist]\n");
+  else
+    {
+      while (sl != NULL)
+	{
+	  printf ("%i: ", i);
+	  termPrint (sl->subst->from);
+	  printf (" -> ");
+	  termPrint (sl->subst->to);
+	  printf ("\n");
+	  i++;
+	  sl = sl->next;
+	}
+    }
+}
diff --git a/src/substitutions.h b/src/substitutions.h
new file mode 100644
index 0000000..0997859
--- /dev/null
+++ b/src/substitutions.h
@@ -0,0 +1,44 @@
+#ifndef SUBSTITUTIONS
+#define SUBSTITUTIONS
+
+#include "termlists.h"
+#include "knowledge.h"
+#include "runs.h"
+
+struct substitution
+{
+  Term from;
+  Term to;
+};
+
+typedef struct substitution *Substitution;
+
+struct substitutionlist
+{
+  Substitution subst;
+  struct substitutionlist *next;
+};
+
+typedef struct substitutionlist *Substitutionlist;
+
+
+Substitution makeSubstitution (Term from, Term to);
+void substitutionDelete (Substitution subs);
+void substitutionDestroy (Substitution subs);
+Term termSubstitute (Term term, Substitution subs);
+Termlist termlistSubstitute (Termlist tl, Substitution subs);
+void substitutionPrint (Term t, Substitution subs);
+Term termSubstituteList (Term term, Substitutionlist sl);
+Substitutionlist makeSubstitutionList (Substitution subs);
+Substitutionlist substitutionlistAdd (Substitutionlist sl, Term from,
+				      Term to);
+void substitutionlistDestroy (Substitutionlist sl);
+void substitutionlistAnnihilate (Substitutionlist sl);
+Substitutionlist substitutionlistConcat (Substitutionlist sl1,
+					 Substitutionlist sl2);
+Termlist substitutionBatch (Termlist tl, Substitutionlist sl);
+Roledef substitutionRoledef (Roledef rd, Substitutionlist sl);
+Knowledge substitutionKnowledge (Knowledge know, Substitutionlist sl);
+void substitutionlistPrint (Substitutionlist sl);
+
+#endif
diff --git a/src/symbols.c b/src/symbols.c
new file mode 100644
index 0000000..6efae1c
--- /dev/null
+++ b/src/symbols.c
@@ -0,0 +1,145 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+#include "symbols.h"
+#include "memory.h"
+
+/*
+   Symbol processor.
+
+   Stores symbols for the lexical scanner. Can later print them.
+   Implementation uses a hashtable, the size of which is defined in
+   symbols.h.
+*/
+
+extern int yylineno;
+
+/* global declarations */
+
+Symbol symbtab[HASHSIZE];
+Symbol symb_list;
+Symbol symb_alloc;
+
+/* main code */
+
+void
+symbolsInit (void)
+{
+  int i;
+
+  for (i = 0; i < HASHSIZE; i++)
+    symbtab[i] = NULL;
+  symb_list = NULL;
+  symb_alloc = NULL;
+}
+
+void
+symbolsDone (void)
+{
+  Symbol s;
+
+  while (symb_alloc != NULL)
+    {
+      s = symb_alloc;
+      symb_alloc = s->allocnext;
+      memFree (s, sizeof (struct symbol));
+    }
+}
+
+Symbol
+get_symb (void)
+{
+  Symbol t;
+  if (symb_list != NULL)
+    {
+      t = symb_list;
+      symb_list = symb_list->next;
+    }
+  else
+    {
+      t = (Symbol) memAlloc (sizeof (struct symbol));
+      t->allocnext = symb_alloc;
+      symb_alloc = t;
+    }
+  return t;
+}
+
+void
+free_symb (Symbol s)
+{
+  if (s == NULL)
+    return;
+  s->next = symb_list;
+  symb_list = s;
+}
+
+int
+hash (char *s)
+{
+  int hv = 0;
+  int i;
+
+  for (i = 0; s[i] != EOS; i++)
+    {
+      int v = (hv >> 28) ^ (s[i] & 0xf);
+      hv = (hv << 4) | v;
+    }
+  hv = hv & 0x7fffffff;
+  return hv % HASHSIZE;
+}
+
+void
+insert (Symbol s)
+{
+  if (s == NULL)
+    return;			/* illegal insertion of empty stuff */
+
+  int hv = hash (s->text);
+  s->next = symbtab[hv];
+  symbtab[hv] = s;
+}
+
+Symbol
+lookup (char *s)
+{
+  if (s == NULL)
+    return NULL;
+
+  int hv = hash (s);
+  Symbol t = symbtab[hv];
+
+  while (t != NULL)
+    {
+      if (strcmp (t->text, s) == 0)
+	break;
+      else
+	t = t->next;
+    }
+  return t;
+}
+
+void
+symbolPrint (Symbol s)
+{
+  if (s == NULL)
+    return;
+
+  /* TODO maybe action depending on type? */
+  printf ("%s", s->text);
+}
+
+Symbol
+symbolSysConst (char *str)
+{
+  Symbol symb;
+
+  symb = lookup (str);
+  if (symb == NULL)
+    {
+      symb = get_symb ();
+      symb->lineno = yylineno;
+      symb->type = T_SYSCONST;
+      symb->text = str;
+    }
+  return symb;
+}
diff --git a/src/symbols.h b/src/symbols.h
new file mode 100644
index 0000000..ef6b6d7
--- /dev/null
+++ b/src/symbols.h
@@ -0,0 +1,37 @@
+#ifndef SYMBOLS
+#define SYMBOLS
+
+/* Size of hashtable: optimistically large. */
+#define HASHSIZE 997
+
+#define T_UNDEF		-1
+#define T_PROTOCOL	0
+#define T_CONST		1
+#define T_VAR		2
+#define T_SYSCONST	3
+
+#define EOS 0
+
+struct symbol
+{
+  int type;
+  int lineno;
+  char *text;
+  struct symbol *next;
+  struct symbol *allocnext;
+};
+
+typedef struct symbol *Symbol;
+
+void symbolsInit (void);
+void symbolsDone (void);
+
+Symbol get_symb (void);
+void free_symb (Symbol s);
+
+void insert (Symbol s);
+Symbol lookup (char *s);
+void symbolPrint (Symbol s);
+Symbol symbolSysConst (char *str);
+
+#endif
diff --git a/src/tac.c b/src/tac.c
new file mode 100644
index 0000000..55c8a2f
--- /dev/null
+++ b/src/tac.c
@@ -0,0 +1,269 @@
+#include <stdio.h>
+#include "tac.h"
+#include "memory.h"
+
+extern int yylineno;
+
+static Tac allocatedTacs;
+
+void
+tacInit (void)
+{
+  allocatedTacs = NULL;
+}
+
+void
+tacDone (void)
+{
+  Tac ts, tf;
+
+  ts = allocatedTacs;
+  while (ts != NULL)
+    {
+      tf = ts;
+      ts = ts->allnext;
+      memFree (tf, sizeof (struct tacnode));
+    }
+}
+
+Tac
+tacCreate (int op)
+{
+  /* maybe even store in scrapping list, so we could delete them
+   * all later */
+  Tac t = memAlloc (sizeof (struct tacnode));
+  t->allnext = allocatedTacs;
+  allocatedTacs = t;
+  t->lineno = yylineno;
+  t->op = op;
+  t->next = NULL;
+  t->prev = NULL;
+  t->tac1 = NULL;
+  t->tac2 = NULL;
+  t->tac3 = NULL;
+  return t;
+}
+
+Tac
+tacString (char *s)
+{
+  Tac t;
+  t = tacCreate (TAC_STRING);
+  t->str1 = s;
+  return t;
+}
+
+Tac
+tacJoin (int op, Tac t1, Tac t2, Tac t3)
+{
+  Tac t;
+  t = tacCreate (op);
+  t->tac1 = t1;
+  t->tac2 = t2;
+  t->tac3 = t3;
+  return t;
+}
+
+Tac
+tacCat (Tac t1, Tac t2)
+{
+  Tac t1e;
+
+  if (t1 == NULL)
+    {
+      if (t2 == NULL)
+	return NULL;
+      else
+	return t2;
+    }
+  else
+    {
+      t1e = t1;
+      while (t1e->next != NULL)
+	t1e = t1e->next;
+      t1e->next = t2;
+      if (t2 != NULL)
+	{
+	  t2->prev = t1e;
+	}
+      return t1;
+    }
+}
+
+/* in: a list. out: a tuple (for e.g. associativity)
+ * Effectively, this defines how we interpret tuples with
+ * more than two components.
+ */
+
+Tac
+tacTuple (Tac taclist)
+{
+  Tac tc;
+
+  /* check for single node */
+  if (taclist->next == NULL)
+    {
+      /* just return */
+      tc = taclist;
+    }
+  else
+    {
+      /* otherwise, write as (x,(y,(z,..))) */
+      tc = tacCreate (TAC_TUPLE);
+      tc->tac1 = taclist;
+      tc->tac2 = tacTuple (taclist->next);
+
+      /* unlink list */
+      tc->tac1->next = NULL;
+      tc->tac2->prev = NULL;
+    }
+  return tc;
+}
+
+/*
+ * tacPrint
+ * Print the tac. Only for debugging purposes.
+ */
+
+void
+tacPrint (Tac t)
+{
+  if (t == NULL)
+    return;
+  switch (t->op)
+    {
+    case TAC_PROTOCOL:
+      printf ("protocol %s (", t->sym1->text);
+      tacPrint (t->tac3);
+      printf (")\n{\n");
+      tacPrint (t->tac2);
+      printf ("};\n");
+      break;
+    case TAC_ROLE:
+      printf ("role %s\n{\n", t->sym1->text);
+      tacPrint (t->tac2);
+      printf ("};\n");
+      break;
+    case TAC_READ:
+      printf ("read");
+      if (t->sym1 != NULL)
+	{
+	  printf ("_%s", t->sym1->text);
+	}
+      printf ("(");
+      tacPrint (t->tac2);
+      printf (");\n");
+      break;
+    case TAC_SEND:
+      printf ("send");
+      if (t->sym1 != NULL)
+	{
+	  printf ("_%s", t->sym1->text);
+	}
+      printf ("(");
+      tacPrint (t->tac2);
+      printf (");\n");
+      break;
+    case TAC_CLAIM:
+      printf ("claim");
+      if (t->sym1 != NULL)
+	{
+	  printf ("_%s", t->sym1->text);
+	}
+      printf ("(");
+      tacPrint (t->tac2);
+      printf (");\n");
+      break;
+    case TAC_CONST:
+      printf ("const ");
+      tacPrint (t->tac1);
+      if (t->tac2 != NULL)
+	{
+	  printf (" : ");
+	  tacPrint (t->tac2);
+	}
+      printf (";\n");
+      break;
+    case TAC_VAR:
+      printf ("var ");
+      tacPrint (t->tac1);
+      if (t->tac2 != NULL)
+	{
+	  printf (" : ");
+	  tacPrint (t->tac2);
+	}
+      printf (";\n");
+      break;
+    case TAC_UNDEF:
+      printf ("undefined");
+      if (t->next != NULL)
+	printf (",");
+      break;
+    case TAC_STRING:
+      printf ("%s", t->sym1->text);
+      if (t->next != NULL)
+	printf (",");
+      break;
+    case TAC_TUPLE:
+      printf ("(");
+      tacPrint (t->tac1);
+      printf (",");
+      tacPrint (t->tac2);
+      printf (")");
+      break;
+    case TAC_ENCRYPT:
+      printf ("{");
+      tacPrint (t->tac1);
+      printf ("}");
+      tacPrint (t->tac2);
+      if (t->next != NULL)
+	{
+	  printf (",");
+	  t = t->next;
+	  tacPrint (t);
+	}
+      break;
+    case TAC_RUN:
+      printf ("run ");
+      tacPrint (t->tac1);
+      printf ("(");
+      tacPrint (t->tac2);
+      printf (");\n");
+      break;
+    case TAC_ROLEREF:
+      symbolPrint (t->sym1);
+      printf (".");
+      symbolPrint (t->sym2);
+      break;
+    case TAC_COMPROMISED:
+      printf ("compromised ");
+      tacPrint (t->tac1);
+      printf (";\n");
+      break;
+    case TAC_SECRET:
+      printf ("secret ");
+      tacPrint (t->tac1);
+      printf (";\n");
+      break;
+    case TAC_INVERSEKEYS:
+      printf ("inversekeys (");
+      tacPrint (t->tac1);
+      printf (",");
+      tacPrint (t->tac2);
+      printf (");\n");
+      break;
+    case TAC_UNTRUSTED:
+      printf ("untrusted ");
+      tacPrint (t->tac1);
+      printf (";\n");
+      break;
+    default:
+      printf ("[??]");
+    }
+
+  /* and any other stuff */
+  if (t->next != NULL)
+    {
+      tacPrint (t->next);
+    }
+}
diff --git a/src/tac.h b/src/tac.h
new file mode 100644
index 0000000..7ee7f02
--- /dev/null
+++ b/src/tac.h
@@ -0,0 +1,69 @@
+#ifndef TAC_H
+#define TAC_H
+
+#include "symbols.h"
+
+/*
+ * TAC instructions
+ */
+
+#define TAC_UNDEF	0
+#define TAC_SYM		1
+#define TAC_TUPLE	3
+#define TAC_ENCRYPT	4
+#define TAC_VAR		7
+#define TAC_CONST	8
+#define TAC_READ	9
+#define TAC_SEND	10
+#define TAC_CLAIM	11
+#define TAC_FUNC	12
+#define TAC_STRING	13
+#define TAC_ROLE	14
+#define TAC_PROTOCOL	15
+#define TAC_RUN		16
+#define TAC_ROLEREF	17
+#define TAC_SECRET	18
+#define TAC_INVERSEKEYS	19
+#define TAC_UNTRUSTED	20
+#define TAC_COMPROMISED	21
+#define TAC_USERTYPE	22
+
+struct tacnode
+{
+  struct tacnode *next;
+  struct tacnode *prev;
+  struct tacnode *allnext;
+  int op;
+  int lineno;
+  union
+  {
+    Symbol sym1;
+    struct tacnode *tac1;
+    char *str1;
+  };
+  union
+  {
+    Symbol sym2;
+    struct tacnode *tac2;
+    char *str2;
+  };
+  union
+  {
+    Symbol sym3;
+    struct tacnode *tac3;
+    char *str3;
+  };
+};
+
+typedef struct tacnode *Tac;
+
+void tacInit (void);
+void tacDone (void);
+Tac tacCreate (int op);
+Tac tacSymb (char *s);
+Tac tacJoin (int op, Tac t1, Tac t2, Tac t3);
+Tac tacTuple (Tac taclist);
+Tac tacCat (Tac t1, Tac t2);
+void tacPrint (Tac t);
+
+#endif
diff --git a/src/termlists.c b/src/termlists.c
new file mode 100644
index 0000000..b998650
--- /dev/null
+++ b/src/termlists.c
@@ -0,0 +1,702 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "termlists.h"
+#include "debug.h"
+#include "memory.h"
+
+/* system constants.
+ * declared in compiler.c
+ */
+
+extern Term TERM_Function;
+extern Term TERM_Hidden;
+
+void
+termlistsInit (void)
+{
+  return;
+}
+
+void
+termlistsDone (void)
+{
+  return;
+}
+
+/* inline candidate */
+
+Termlist
+makeTermlist ()
+{
+  return (Termlist) memAlloc (sizeof (struct termlist));
+}
+
+/*
+
+termlistDuplicate
+
+A deep copy.
+
+*/
+
+Termlist
+termlistDuplicate (Termlist tl)
+{
+  Termlist newtl;
+
+  if (tl == NULL)
+    return NULL;
+  newtl = makeTermlist ();
+  newtl->term = termDuplicate (tl->term);
+  newtl->prev = NULL;
+  newtl->next = termlistDuplicate (tl->next);
+  if (newtl->next != NULL)
+    (newtl->next)->prev = newtl;
+  return newtl;
+}
+
+/*
+
+termlistShallow
+
+A shallow copy, because I gather we won't be modifying any terms, only
+termlists. Oh, and it reverses the order :) Don't forget!
+
+*/
+
+Termlist
+termlistShallow (Termlist tl)
+{
+  Termlist newtl;
+
+  newtl = NULL;
+  while (tl != NULL)
+    {
+      newtl = termlistAdd (newtl, tl->term);
+      tl = tl->next;
+    }
+  return newtl;
+}
+
+/*
+
+termlistDelete
+
+(shallow)
+
+*/
+
+void
+termlistDelete (Termlist tl)
+{
+  if (tl == NULL)
+    return;
+  termlistDelete (tl->next);
+  memFree (tl, sizeof (struct termlist));
+}
+
+
+/*
+
+termlistDestroy
+
+(deep)
+
+*/
+
+void
+termlistDestroy (Termlist tl)
+{
+  if (tl == NULL)
+    return;
+  termlistDestroy (tl->next);
+  termDelete (tl->term);
+  memFree (tl, sizeof (struct termlist));
+}
+
+/*
+
+inTermlist
+
+check whether a term occurs in a termlist
+
+*/
+
+int
+inTermlist (Termlist tl, Term term)
+{
+  if (tl == NULL)
+    {
+      if (term == NULL)
+	return 1;
+      else
+	return 0;
+    }
+  else
+    {
+      if (isTermEqual (tl->term, term))
+	return 1;
+      else
+	return inTermlist (tl->next, term);
+    }
+}
+
+/* are all elements of list 1 in list 2, and vice versa? 
+ Note that we assume unique elements !
+ */
+
+int
+isTermlistEqual (Termlist tl1, Termlist tl2)
+{
+  if (termlistLength (tl1) != termlistLength (tl2))
+    return 0;
+  while (tl2 != NULL)
+    {
+      if (!inTermlist (tl1, tl2->term))
+	return 0;
+      tl2 = tl2->next;
+    }
+  return 1;
+}
+
+/*
+
+termlistAdd
+
+Adds a term. Duplicates are allowed.
+A new list pointer is returned.
+
+*/
+
+Termlist
+termlistAdd (Termlist tl, Term term)
+{
+  Termlist newtl;
+
+  newtl = makeTermlist ();
+  newtl->term = term;
+  newtl->next = tl;
+
+  if (tl == NULL)
+    {
+      newtl->prev = NULL;
+    }
+  else
+    {
+      newtl->prev = tl->prev;
+      if (newtl->prev != NULL)
+	(newtl->prev)->next = newtl;
+      tl->prev = newtl;
+    }
+  return newtl;
+}
+
+/*
+
+termlistAppend
+
+Appends a term to the end of the list. Duplicates are allowed.
+A new list pointer is returned.
+
+*/
+
+Termlist
+termlistAppend (const Termlist tl, const Term term)
+{
+  Termlist newtl;
+  Termlist scantl;
+
+  newtl = makeTermlist ();
+  newtl->term = term;
+  newtl->next = NULL;
+
+  if (tl == NULL)
+    {
+      newtl->prev = NULL;
+      return newtl;
+    }
+  else
+    {
+      scantl = tl;
+      while (scantl->next != NULL)
+	scantl = scantl->next;
+      scantl->next = newtl;
+      newtl->prev = scantl;
+    }
+  return tl;
+}
+
+Termlist
+termlistConcat (Termlist tl1, Termlist tl2)
+{
+  if (tl1 == NULL)
+    return tl2;
+  if (tl2 == NULL)
+    return tl1;
+
+  Termlist scan = tl1;
+  while (scan->next != NULL)
+    scan = scan->next;
+  scan->next = tl2;
+  return tl1;
+}
+
+/*
+
+termlistDelTerm
+
+remove the current element from the termlist. Easier because of the
+double linked list.
+
+*/
+Termlist
+termlistDelTerm (Termlist tl)
+{
+  Termlist newhead;
+
+  if (tl == NULL)
+    return NULL;
+  if (tl->prev != NULL)
+    {
+      (tl->prev)->next = tl->next;
+      newhead = tl->prev;
+      while (newhead->prev != NULL)
+	newhead = newhead->prev;
+    }
+  else
+    {
+      newhead = tl->next;
+    }
+  if (tl->next != NULL)
+    (tl->next)->prev = tl->prev;
+  memFree (tl, sizeof (struct termlist));
+  return newhead;
+}
+
+Termlist
+termlistConjunct (Termlist tl1, Termlist tl2)
+{
+  Termlist newtl;
+  Termlist scan;
+
+  scan = tl1;
+  newtl = NULL;
+  while (scan != NULL)
+    {
+      if (inTermlist (tl2, scan->term))
+	newtl = termlistAdd (newtl, scan->term);
+      scan = scan->next;
+    }
+  return newtl;
+}
+
+Termlist
+termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
+{
+  Termlist newtl;
+  Termlist scan;
+
+  scan = tl1;
+  newtl = NULL;
+  while (scan != NULL)
+    {
+      if (((scan->term)->type == termtype) && (inTermlist (tl2, scan->term)))
+	newtl = termlistAdd (newtl, scan->term);
+      scan = scan->next;
+    }
+  return newtl;
+}
+
+Termlist
+termlistType (Termlist tl, int termtype)
+{
+  Termlist newtl;
+  Termlist scan;
+
+  scan = tl;
+  newtl = NULL;
+  while (scan != NULL)
+    {
+      if ((scan->term)->type == termtype)
+	newtl = termlistAdd (newtl, scan->term);
+      scan = scan->next;
+    }
+  return newtl;
+}
+
+void
+termlistPrint (Termlist tl)
+{
+  if (tl == NULL)
+    {
+      printf ("[Empty]");
+      return;
+    }
+  printf ("[");
+  while (tl != NULL)
+    {
+      termPrint (tl->term);
+      tl = tl->next;
+      if (tl != NULL)
+	  printf(", ");
+    }
+  printf ("]");
+}
+
+Termlist
+termlistAddVariables (Termlist tl, Term t)
+{
+  if (t == NULL)
+    return tl;
+
+  t = deVar (t);
+  if (isTermLeaf (t))
+    {
+      if (isTermVariable (t) && !inTermlist (tl, t))
+	return termlistAdd (tl, t);
+      else
+	return tl;
+    }
+  else
+    {
+      if (isTermEncrypt (t))
+	return termlistAddVariables (termlistAddVariables (tl, t->op),
+				     t->key);
+      else
+	return
+	  termlistAddVariables (termlistAddVariables (tl, t->op1), t->op2);
+    }
+}
+    
+Termlist
+termlistAddRealVariables (Termlist tl, Term t)
+{
+  if (t == NULL)
+    return tl;
+
+  if (realTermLeaf (t))
+    {
+      if (realTermVariable (t))
+	{
+	  Term tbuf = t->subst;
+	  t->subst = NULL;
+	  if (!inTermlist (tl,t))
+	    {
+	      tl = termlistAdd (tl,t);
+	    }
+	  t->subst = tbuf;
+	  return termlistAddRealVariables (tl,t->subst);
+	}
+      else
+	{
+	  return tl;
+	}
+    }
+  else
+    {
+      if (realTermEncrypt (t))
+	return termlistAddVariables (termlistAddVariables (tl, t->op),
+				     t->key);
+      else
+	return
+	  termlistAddVariables (termlistAddVariables (tl, t->op1), t->op2);
+    }
+}
+
+Termlist
+termlistAddBasic (Termlist tl, Term t)
+{
+  if (t == NULL)
+    return tl;
+  if (!isTermLeaf (t))
+    {
+      if (isTermEncrypt (t))
+	return termlistAddBasic (termlistAddBasic (tl, t->op), t->key);
+      else
+	return termlistAddBasic (termlistAddBasic (tl, t->op1), t->op2);
+    }
+  else
+    {
+      if (!inTermlist (tl, t))
+	{
+	  return termlistAdd (tl, t);
+	}
+
+    }
+  return tl;
+}
+
+Termlist
+termlistAddBasics (Termlist tl, Termlist scan)
+{
+  while (scan != NULL)
+    {
+      tl = termlistAddBasic (tl, scan->term);
+      scan = scan->next;
+    }
+  return tl;
+}
+
+/*
+ * termlistMinusTerm
+ *
+ * Remove a term from a termlist, and yield a new termlist pointer.
+ * Semantics: remove the first occurrence of the term.
+ */
+
+Termlist
+termlistMinusTerm (Termlist tl, Term t)
+{
+  Termlist scan;
+
+  scan = tl;
+  while (scan != NULL)
+    {
+      if (isTermEqual (scan->term, t))
+	return termlistDelTerm (scan);
+      else
+	scan = scan->next;
+    }
+  return tl;
+}
+
+int
+termlistLength (Termlist tl)
+{
+  int i = 0;
+
+  while (tl != NULL)
+    {
+      tl = tl->next;
+      i++;
+    }
+  return i;
+}
+
+/*
+
+inverseKey
+
+Gives the inverse Key of some term (which is used to encrypt something), as is defined
+by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
+
+*/
+
+
+Term
+inverseKey (Termlist inverses, Term key)
+{
+  key = deVar (key);
+
+  /* is this a function application? i.e. hash? */
+  if (isTermLeaf (key) && inTermlist (key->stype, TERM_Function))
+    {
+      /* functions cannot be inverted by default */
+      return termDuplicate (TERM_Hidden);
+    }
+  /* check for the special case first: when it is effectively a function application  */
+  if (isTermEncrypt (key) && isTermLeaf (key->key)
+      && inTermlist (deVar (key->key)->stype, TERM_Function))
+    {
+      /* we are scanning for functions */
+      /* scan the list */
+      /* key is function application kk(op), or {op}kk */
+      Term funKey (Term orig, Term newk)
+      {
+	/* in: {op}kk, nk
+	 * out: {op'}nk */
+	return makeTermEncrypt (termDuplicate (orig->op),
+				termDuplicate (newk));
+      }
+      while (inverses != NULL && inverses->next != NULL)
+	{
+
+	  if (isTermEqual (key->key, inverses->term))
+	    return funKey (key, inverses->next->term);
+	  if (isTermEqual (key->key, inverses->next->term))
+	    return funKey (key, inverses->term);
+	  inverses = inverses->next->next;
+	}
+    }
+  else
+    {
+      /* scanning for a direct inverse */
+
+      /* scan the list */
+      while (inverses != NULL && inverses->next != NULL)
+	{
+	  if (isTermEqual (key, inverses->term))
+	    return termDuplicate (inverses->next->term);
+	  if (isTermEqual (key, inverses->next->term))
+	    return termDuplicate (inverses->term);
+	  inverses = inverses->next->next;
+	}
+    }
+  return termDuplicate (key);	/* defaults to symmetrical */
+}
+
+/*
+ * localTerm
+ *
+ * Creates a term local to a run.
+ * We assume that at this point, no variables have been instantiated yet that occur in this term.
+ * We also assume that fromlist, tolist and locals only hold real leaves.
+ */
+
+Term
+termLocal (const Term t, Termlist fromlist, Termlist tolist,
+	   const Termlist locals, const int runid)
+{
+  if (t == NULL)
+    return NULL;
+
+  if (realTermLeaf (t))
+    {
+      while (fromlist != NULL && tolist != NULL)
+	{
+	  if (isTermEqual (fromlist->term, t))
+	    {
+	      // matches!
+	      return tolist->term;
+	    }
+	  fromlist = fromlist->next;
+	  tolist = tolist->next;
+	}
+      if (inTermlist (locals, t))
+	{
+	  // return termRunid(t,runid);
+	}
+      return t;
+    }
+  else
+    {
+      Term newt = termDuplicate (t);
+      if (realTermTuple (t))
+	{
+	  newt->op1 = termLocal (t->op1, fromlist, tolist, locals, runid);
+	  newt->op2 = termLocal (t->op2, fromlist, tolist, locals, runid);
+	}
+      else
+	{
+	  newt->op = termLocal (t->op, fromlist, tolist, locals, runid);
+	  newt->key = termLocal (t->key, fromlist, tolist, locals, runid);
+	}
+      return newt;
+    }
+}
+
+/*
+ * termlistLocal
+ *
+ * We expand the previous concept to termlists.
+ */
+
+Termlist
+termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
+	       const Termlist locals, int runid)
+{
+  Termlist newtl = NULL;
+
+  while (tl != NULL)
+    {
+      newtl =
+	termlistAdd (newtl,
+		     termLocal (tl->term, fromlist, tolist, locals, runid));
+      tl = tl->next;
+    }
+  return newtl;
+}
+
+/*
+ * Check whether tl2 is contained in tl1.
+ */
+
+int
+termlistContained (const Termlist tlbig, Termlist tlsmall)
+{
+  while (tlsmall != NULL)
+    {
+      if (!inTermlist (tlbig, tlsmall->term))
+	return 0;
+      tlsmall = tlsmall->next;
+    }
+  return 1;
+}
+
+/*
+ * Determine whether a variable has been substituted with something with
+ * the right type.
+ */
+
+int
+validSubst (const int matchmode, const Term term)
+{
+  if (!realTermVariable (term) || term->subst == NULL)
+    return 1;
+  else
+    {
+      switch (matchmode)
+	{
+	case 0:		/* real type match */
+	  return realTermLeaf (term->subst)
+	    && termlistContained (term->stype, term->subst->stype);
+	case 1:		/* basic type match */
+	  /* subst must be a leaf */
+	  /* TODO: what about functions? */
+	  return realTermLeaf (term->subst);
+	case 2:		/* no type match */
+	  /* anything goes */
+	  return 1;
+	default:
+	  return 0;
+	}
+    }
+}
+
+/*
+ * termFunction
+ *
+ * An assist function that helps to simulate Term->Term functions, using
+ * termlists. One termlist functions as the domain, and the other as the
+ * range.
+ *
+ * Extending a function with a value y = f(x) amounts to extending the
+ * domain with x, and the range with y.
+ */
+
+Term
+termFunction (Termlist fromlist, Termlist tolist, Term tx)
+{
+  while (fromlist != NULL && tolist != NULL)
+    {
+      if (isTermEqual (fromlist->term, tx))
+	{
+	  return tolist->term;
+	}
+      fromlist = fromlist->next;
+      tolist = tolist->next;
+    }
+  return NULL;
+}
+
+/*
+ * Forward the termlist pointer to the last item
+ */
+
+Termlist
+termlistForward (Termlist tl)
+{
+  if (tl == NULL)
+    {
+      return NULL;
+    }
+  else
+    {
+      while (tl->next != NULL)
+	{
+	  tl = tl->next;
+	}
+      return tl;
+    }
+}
+
diff --git a/src/termlists.h b/src/termlists.h
new file mode 100644
index 0000000..235bb73
--- /dev/null
+++ b/src/termlists.h
@@ -0,0 +1,48 @@
+#ifndef TERMLISTS
+#define TERMLISTS
+
+#include "terms.h"
+
+struct termlist
+{
+  Term term;
+  struct termlist *next;
+  struct termlist *prev;
+};
+
+typedef struct termlist *Termlist;
+
+void termlistsInit (void);
+void termlistsDone (void);
+Termlist termlistDuplicate (Termlist tl);
+Termlist termlistShallow (Termlist tl);
+void termlistDelete (Termlist tl);
+void termlistDestroy (Termlist tl);
+void termlistPrint (Termlist tl);
+int inTermlist (Termlist tl, Term term);
+int isTermlistEqual (Termlist tl1, Termlist tl2);
+Termlist termlistAdd (Termlist tl, Term term);
+Termlist termlistAppend (const Termlist tl, const Term term);
+Termlist termlistConcat (Termlist tl1, Termlist tl2);
+Termlist termlistDelTerm (Termlist tl);
+Termlist termlistConjunct (Termlist tl1, Termlist tl2);
+Termlist termlistConjunctType (Termlist tl1, Termlist tl2, int termtype);
+Termlist termlistType (Termlist tl, int termtype);
+Termlist termlistAddVariables (Termlist tl, Term t);
+Termlist termlistAddRealVariables (Termlist tl, Term t);
+Termlist termlistAddBasic (Termlist tl, Term t);
+Termlist termlistAddBasics (Termlist tl, Termlist scan);
+Termlist termlistMinusTerm (Termlist tl, Term t);
+int termlistLength (Termlist tl);
+Term inverseKey (Termlist inverses, Term key);
+Term termLocal (const Term t, Termlist fromlist, Termlist tolist,
+		const Termlist locals, const int runid);
+Termlist termlistLocal (Termlist tl, const Termlist fromlist,
+			const Termlist tolist, const Termlist locals,
+			const int runid);
+int termlistContained (const Termlist tlbig, Termlist tlsmall);
+int validSubst (const int matchmode, const Term term);
+Term termFunction (Termlist fromlist, Termlist tolist, Term tx);
+Termlist termlistForward (Termlist tl);
+
+#endif
diff --git a/src/terms.c b/src/terms.c
new file mode 100644
index 0000000..7ddcec1
--- /dev/null
+++ b/src/terms.c
@@ -0,0 +1,680 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <limits.h>
+#include "terms.h"
+#include "debug.h"
+#include "memory.h"
+#include "ctype.h"
+
+
+/* external definitions */
+
+extern Term TERM_Function;
+extern int inTermlist ();	// suppresses a warning, but at what cost?
+extern int globalLatex;
+
+/* forward declarations */
+
+void indent (void);
+
+/* useful macros */
+
+#define RID_UNDEF MIN_INT
+/* main code */
+
+/* Two types of terms: general, and normalized. Normalized rewrites all
+   tuples to (x,(y,z))..NULL form, making list traversal easy. */
+
+void
+termsInit (void)
+{
+  return;
+}
+
+void
+termsDone (void)
+{
+  return;
+}
+
+Term
+makeTerm ()
+{
+  return (Term) memAlloc (sizeof (struct term));
+}
+
+Term
+makeTermEncrypt (Term t1, Term t2)
+{
+  Term term = makeTerm ();
+  term->type = ENCRYPT;
+  term->stype = NULL;
+  term->op = t1;
+  term->key = t2;
+  return term;
+}
+
+Term
+makeTermTuple (Term t1, Term t2)
+{
+  if (t1 == NULL)
+    {
+      if (t2 == NULL)
+	{
+#ifdef DEBUG
+	  debug (5, "Trying to make a tuple node with an empty term.");
+#endif
+	  return NULL;
+	}
+      else
+	return t2;
+    }
+  if (t2 == NULL)
+    {
+      return t1;
+    }
+
+  Term tt = makeTerm ();
+  tt->type = TUPLE;
+  tt->stype = NULL;
+  tt->op1 = t1;
+  tt->op2 = t2;
+  return tt;
+}
+
+Term
+makeTermType (const int type, const Symbol symb, const int runid)
+{
+  Term term = makeTerm ();
+  term->type = type;
+  term->stype = NULL;
+  term->subst = NULL;
+  term->symb = symb;
+  term->runid = runid;
+  return term;
+}
+
+/* deVar unwraps any substitutions.
+ *
+ * For speed, it is a macro. Sometimes it will call
+ * deVarScan to do the actual unwinding.
+ */
+
+Term
+deVarScan (Term t)
+{
+  while (realTermVariable (t) && t->subst != NULL)
+    t = t->subst;
+  return t;
+}
+
+int
+hasTermVariable (Term term)
+{
+  if (term == NULL)
+    return 0;
+  term = deVar (term);
+  if (realTermLeaf (term))
+    return realTermVariable (term);
+  else
+    {
+      if (realTermTuple (term))
+	return (hasTermVariable (term->op1) || hasTermVariable (term->op2));
+      else
+	return (hasTermVariable (term->op) || hasTermVariable (term->key));
+    }
+}
+
+/*
+
+isTermEqualFn(term,term)
+
+Tests whether two terms are completely identical. This also includes
+variables. This is the recursive function.
+
+We assume the term is normalized, e.g. no tupling has direct
+subtupling.
+
+Out: 0 unequal, 1 equal
+*/
+
+int
+isTermEqualFn (Term term1, Term term2)
+{
+  term1 = deVar (term1);
+  term2 = deVar (term2);
+
+  if (term1 == term2)
+    return 1;
+  if ((term1 == NULL) || (term2 == NULL))
+    return 0;
+
+  if (term1->type != term2->type)
+    {
+      return 0;
+    }
+  if (realTermLeaf (term1))
+    {
+      return (term1->symb == term2->symb && term1->runid == term2->runid);
+    }
+  else
+    {
+      /* ENCRYPT or TUPLE */
+
+      if (realTermEncrypt (term1))
+	{
+	  /* for optimization of encryption equality, we compare
+	     operator 2 first (we expect it to be a smaller term)
+	   */
+	  return (isTermEqualFn (term1->key, term2->key) &&
+		  isTermEqualFn (term1->op, term2->op));
+	}
+      else
+	{
+	  /* tuple */
+
+	  return (isTermEqualFn (term1->op1, term2->op1) &&
+		  isTermEqualFn (term1->op2, term2->op2));
+	}
+    }
+}
+
+int
+termOccurs (Term t, Term tsub)
+{
+  t = deVar (t);
+  tsub = deVar (tsub);
+
+  if (isTermEqual (t, tsub))
+    return 1;
+  if (realTermLeaf (t))
+    return 0;
+  if (realTermTuple (t))
+    return (termOccurs (t->op1, tsub) || termOccurs (t->op2, tsub));
+  else
+    return (termOccurs (t->op, tsub) || termOccurs (t->key, tsub));
+}
+
+
+void
+termPrint (Term term)
+{
+  if (term == NULL)
+    {
+      printf ("Empty term");
+      return;
+    }
+#ifdef DEBUG
+  if (!DEBUGL (1))
+    {
+      term = deVar (term);
+    }
+#else
+  term = deVar (term);
+#endif
+  if (realTermLeaf (term))
+    {
+      symbolPrint (term->symb);
+      if (realTermVariable (term))
+	printf ("V");
+      if (term->runid >= 0)
+	{
+	  if (globalLatex)
+	    printf ("\\sharp%i", term->runid);
+	  else
+	    printf ("#%i", term->runid);
+	}
+      if (term->subst != NULL)
+	{
+	  if (globalLatex)
+	    printf ("\\rightarrow");
+	  else
+	    printf ("->");
+	  termPrint (term->subst);
+	}
+    }
+  if (realTermTuple (term))
+    {
+      printf ("(");
+      while (realTermTuple (term))
+	{
+	  termPrint (term->op1);
+	  printf (",");
+	  term = term->op2;
+	  if (!realTermTuple (term))
+	    termPrint (term);
+
+	}
+      printf (")");
+      return;
+    }
+  if (realTermEncrypt (term))
+    {
+      if (isTermLeaf (term->key)
+	  && inTermlist (term->key->stype, TERM_Function))
+	{
+	  /* function application */
+	  termPrint (term->key);
+	  printf ("(");
+	  termPrint (term->op);
+	  printf (")");
+	}
+      else
+	{
+	  /* normal encryption */
+	  if (globalLatex)
+	    {
+	      printf ("\\{");
+	      termPrint (term->op);
+	      printf ("\\}_{");
+	      termPrint (term->key);
+	      printf ("}");
+	    }
+	  else
+	    {
+	      printf ("{");
+	      termPrint (term->op);
+	      printf ("}");
+	      termPrint (term->key);
+	    }
+	}
+    }
+}
+
+
+/*
+
+Duplicate
+
+make a deep copy of a term, but not of leaves.
+
+*/
+
+Term
+termDuplicate (const Term term)
+{
+  Term newterm;
+
+  if (term == NULL)
+    return NULL;
+  if (realTermLeaf (term))
+    return term;
+
+  newterm = (Term) memAlloc (sizeof (struct term));
+  newterm->type = term->type;
+  if (realTermEncrypt (term))
+    {
+      newterm->op = termDuplicate (term->op);
+      newterm->key = termDuplicate (term->key);
+    }
+  else
+    {
+      newterm->op1 = termDuplicate (term->op1);
+      newterm->op2 = termDuplicate (term->op2);
+    }
+  return newterm;
+}
+
+/*
+
+DuplicateDeep
+
+make a deep copy of a term, and also of leaves.
+
+*/
+
+Term
+termDuplicateDeep (const Term term)
+{
+  Term newterm;
+
+  if (term == NULL)
+    return NULL;
+
+  newterm = (Term) memAlloc (sizeof (struct term));
+  if (realTermLeaf (term))
+    {
+      memcpy (newterm, term, sizeof (struct term));
+    }
+  else
+    {
+      newterm->type = term->type;
+      if (realTermEncrypt (term))
+	{
+	  newterm->op = termDuplicateDeep (term->op);
+	  newterm->key = termDuplicateDeep (term->key);
+	}
+      else
+	{
+	  newterm->op1 = termDuplicateDeep (term->op1);
+	  newterm->op2 = termDuplicateDeep (term->op2);
+	}
+    }
+  return newterm;
+}
+
+/*
+ * DuplicateUV
+ *
+ * Remove all instantiated variables on the way down.
+ */
+
+Term
+termDuplicateUV (Term term)
+{
+  Term newterm;
+
+  if (term == NULL)
+    return NULL;
+  term = deVar (term);
+  if (realTermLeaf (term))
+    return term;
+
+  newterm = (Term) memAlloc (sizeof (struct term));
+  newterm->type = term->type;
+  if (realTermEncrypt (term))
+    {
+      newterm->op = termDuplicateUV (term->op);
+      newterm->key = termDuplicateUV (term->key);
+    }
+  else
+    {
+      newterm->op1 = termDuplicateUV (term->op1);
+      newterm->op2 = termDuplicateUV (term->op2);
+    }
+  return newterm;
+}
+
+/*
+
+realTermDuplicate
+
+make a deep copy of a term, also of leaves.
+
+*/
+
+Term
+realTermDuplicate (const Term term)
+{
+  Term newterm;
+
+  if (term == NULL)
+    return NULL;
+
+  newterm = (Term) memAlloc (sizeof (struct term));
+  if (realTermLeaf (term))
+    {
+      memcpy (newterm, term, sizeof (struct term));
+    }
+  else
+    {
+      newterm->type = term->type;
+      if (realTermEncrypt (term))
+	{
+	  newterm->op = realTermDuplicate (term->op);
+	  newterm->key = realTermDuplicate (term->key);
+	}
+      else
+	{
+	  newterm->op1 = realTermDuplicate (term->op1);
+	  newterm->op2 = realTermDuplicate (term->op2);
+	}
+    }
+  return newterm;
+}
+
+/*
+
+termDelete
+
+Removes a term and deallocates memory
+
+*/
+
+void
+termDelete (const Term term)
+{
+  if (term != NULL && !realTermLeaf (term))
+    {
+      if (realTermEncrypt (term))
+	{
+	  termDelete (term->op);
+	  termDelete (term->key);
+	}
+      else
+	{
+	  termDelete (term->op1);
+	  termDelete (term->op2);
+	}
+      memFree (term, sizeof (struct term));
+    }
+}
+
+/*
+   termNormalize
+
+   avoids problems with associativity by rewriting every ((x,y),z) to
+   (x,y,z)), i.e. a normal form for terms, after which equality is
+   okay.
+*/
+
+void
+termNormalize (Term term)
+{
+  term = deVar (term);
+  if (term == NULL || realTermLeaf (term))
+    return;
+
+  if (realTermEncrypt (term))
+    {
+      termNormalize (term->op);
+      termNormalize (term->key);
+    }
+  else
+    {
+      /* normalize left hand first,both for tupling and for
+         encryption */
+      termNormalize (term->op1);
+      /* check for ((x,y),z) construct */
+      if (realTermTuple (term->op1))
+	{
+	  /* temporarily store the old terms */
+	  Term tx = (term->op1)->op1;
+	  Term ty = (term->op1)->op2;
+	  Term tz = term->op2;
+	  /* move node */
+	  term->op2 = term->op1;
+	  /* construct (x,(y,z)) version */
+	  term->op1 = tx;
+	  (term->op2)->op1 = ty;
+	  (term->op2)->op2 = tz;
+	}
+      termNormalize (term->op2);
+    }
+}
+
+
+Term
+termRunid (Term term, int runid)
+{
+  if (term == NULL)
+    return NULL;
+  if (realTermLeaf (term))
+    {
+      /* leaf */
+      if (term->runid == runid)
+	return term;
+      else
+	{
+	  Term newt = termDuplicate (term);
+	  newt->runid = runid;
+	  return newt;
+	}
+    }
+  else
+    {
+      /* anything else, recurse */
+      if (realTermEncrypt (term))
+	{
+	  return makeTermEncrypt (termRunid (term->op, runid),
+				  termRunid (term->key, runid));
+	}
+      else
+	{
+	  return makeTermTuple (termRunid (term->op1, runid),
+				termRunid (term->op2, runid));
+	}
+    }
+}
+
+/* tupleCount yields the size of the top tuple in the term */
+
+int
+tupleCount (Term tt)
+{
+  if (tt == NULL)
+    {
+      return 0;
+    }
+  else
+    {
+      deVar (tt);
+      if (!realTermTuple (tt))
+	{
+	  return 1;
+	}
+      else
+	{
+	  return (tupleCount (tt->op1) + tupleCount (tt->op2));
+	}
+    }
+}
+
+/* tupleProject yields the projection pi (0 .. n-1) on a top tuple. Returns
+ * NULL if the range is incorrect. */
+
+Term
+tupleProject (Term tt, int n)
+{
+  if (tt == NULL)
+    {
+      return NULL;
+    }
+  deVar (tt);
+  if (!realTermTuple (tt))
+    {
+      if (n > 0)
+	{
+	  /* no tuple, adressing error */
+	  return NULL;
+	}
+      else
+	{
+	  /* no tuple */
+	  return tt;
+	}
+    }
+  else
+    {
+      /* there is a tuple to traverse */
+      int left = tupleCount (tt->op1);
+      if (n >= left)
+	{
+	  /* it's in the right hand side */
+	  return tupleProject (tt->op2, n - left);
+	}
+      else
+	{
+	  /* left hand side */
+	  return tupleProject (tt->op1, n);
+	}
+    }
+}
+
+/* number of elements in a term.
+ *
+ * Currently, the encryption operator is weighed as well.
+ */
+
+int
+termSize(Term t)
+{
+  if (t == NULL)
+    {
+      return 0;
+    }
+
+  t = deVar(t);
+  if (realTermLeaf(t))
+    {
+      return 1;
+    }
+  else
+    {
+      if (realTermEncrypt(t))
+	{
+	  return 1 + termSize(t->op) + termSize(t->key);
+	}
+      else
+	{
+	  return termSize(t->op1) + termSize(t->op2);
+	}
+    }
+}
+
+/* Yield some sort of distance between two terms, as a float between 0 and 1.
+ */
+
+float
+termDistance(Term t1, Term t2)
+{
+  /* First the special cases: no equal subterms, completely equal */
+  if (isTermEqual(t1,t2))
+      return 1;
+
+  t1 = deVar(t1);
+  t2 = deVar(t2);
+
+  int t1s = termSize(t1);
+  int t2s = termSize(t2);
+
+  if (t1 == NULL || t2 == NULL)
+    {
+      return 0;
+    }
+  if (t1->type != t2->type)
+    {
+      /* unequal type, maybe one is a subterm of the other? */
+      if (t1s > t2s && termOccurs(t1,t2))
+	{
+	  return (float) t2s / t1s;
+	}
+      if (t2s > t1s && termOccurs(t2,t1))
+	{
+	  return (float) t1s / t2s;
+	}
+      return 0;
+    }
+  else
+    {
+      /* equal types */
+      if (isTermLeaf(t1))
+	{
+	  /* we had established before that they are not equal */
+	  return 0;
+	}
+      else
+	{
+	  /* non-leaf recurse */
+	  if (isTermEncrypt(t1))
+	    {
+	      /* encryption */
+	      return (termDistance(t1->op, t2->op) + termDistance(t1->key, t2->key)) / 2;
+	    }
+	  else
+	    {
+	      return (termDistance(t1->op1, t2->op1) + termDistance(t1->op2, t2->op2)) / 2;
+	    }
+	}
+    }
+}
diff --git a/src/terms.h b/src/terms.h
new file mode 100644
index 0000000..5b82c51
--- /dev/null
+++ b/src/terms.h
@@ -0,0 +1,93 @@
+#ifndef TERMS
+#define TERMS
+
+#include "symbols.h"
+
+#define	GLOBAL	 1
+#define VARIABLE 2
+#define LEAF	 3		// type <= LEAF means it's a leaf, nkay?
+#define	ENCRYPT  4
+#define	TUPLE	 5
+
+struct term
+{
+  /* basic  : name,runid
+     encrypt: op,key
+     tuple  : op,next
+   */
+  int type;
+  void *stype;			// only for leaf, termlist pointer
+  struct term *subst;		// only for variable/leaf, substitution term
+
+  union
+  {
+    Symbol symb;
+    struct term *op;
+    struct term *op1;
+    struct term *next;		// for alternative memory management
+  };
+  union
+  {
+    int runid;
+    struct term *key;
+    struct term *op2;
+  };
+};
+
+typedef struct term *Term;
+
+void termsInit (void);
+void termsDone (void);
+Term makeTermEncrypt (Term t1, Term t2);
+Term makeTermTuple (Term t1, Term t2);
+Term makeTermType (const int type, const Symbol symb, const int runid);
+Term deVarScan (Term t);
+#define substVar(t)		((t != NULL && t->type == VARIABLE && t->subst != NULL) ? 1 : 0)
+#define deVar(t)		( substVar(t) ? deVarScan(t->subst) : t)
+#define realTermLeaf(t)		(t != NULL && t->type <= LEAF)
+#define realTermTuple(t)	(t != NULL && t->type == TUPLE)
+#define realTermEncrypt(t)	(t != NULL && t->type == ENCRYPT)
+#define realTermVariable(t)	(t != NULL && t->type == VARIABLE)
+#define isTermLeaf(t)		realTermLeaf(deVar(t))
+#define isTermTuple(t)		realTermTuple(deVar(t))
+#define isTermEncrypt(t)	realTermEncrypt(deVar(t))
+#define isTermVariable(t)	realTermVariable(deVar(t))
+#define isTermEqual(t1,t2)	((substVar(t1) || substVar(t2)) \
+				?	isTermEqualFn(t1,t2) \
+				:	( \
+					(t1 == t2) \
+					?	1 \
+					:	( \
+						(t1 == NULL || t2 == NULL || t1->type != t2->type) \
+						?	0 \
+						:	( \
+							realTermLeaf(t1) \
+							?	(t1->symb == t2->symb && t1->runid == t2->runid) \
+							:	( \
+								realTermEncrypt(t2) \
+								?	(isTermEqualFn(t1->key, t2->key) && \
+									 isTermEqualFn(t1->op,  t2->op)) \
+								:	(isTermEqualFn(t1->op1, t2->op1) && \
+									 isTermEqualFn(t1->op2, t2->op2)) \
+								) \
+							) \
+						 )  \
+					) \
+				)
+
+int hasTermVariable (Term term);
+int isTermEqualFn (Term term1, Term term2);
+int termOccurs (Term t, Term tsub);
+void termPrint (Term term);
+Term termDuplicate (const Term term);
+Term termDuplicateDeep (const Term term);
+Term termDuplicateUV (Term term);
+void termDelete (const Term term);
+void termNormalize (Term term);
+Term termRunid (Term term, int runid);
+int tupleCount (Term tt);
+Term tupleProject (Term tt, int n);
+int termSize(Term t);
+float termDistance(Term t1, Term t2);
+
+#endif
diff --git a/src/testl b/src/testl
new file mode 100755
index 0000000..bb0416c
--- /dev/null
+++ b/src/testl
@@ -0,0 +1,22 @@
+#!/bin/bash
+#
+# Shell script to display the latex output relatively quickly. For
+# internal testing only, as it depends on the spdl subdirectory.
+#
+# Usage example:
+#
+#	./testl ns3
+#
+
+file=spdl/$1.spdl outfile=tempattack
+
+if [ -f $file ]
+then 
+  ./scyther --latex <$file >$outfile.tex
+  latex $outfile.tex
+  xdvi $outfile.dvi
+else
+  echo "No file $file found."
+fi
+
+
diff --git a/src/todo.txt b/src/todo.txt
new file mode 100644
index 0000000..6349d5b
--- /dev/null
+++ b/src/todo.txt
@@ -0,0 +1,80 @@
+- Remove stupid preamble postamble stuff, or maybe integrate this behaviour
+  into some switch, where default would be a standalone latex file, and
+  another option would generate a file that can be included.
+- Variables have to be 'saved' and 'stored' into some structure. However, for
+  this we need a global list of all variables, which is not available at the
+  moment. The compiler and run instantiator should maintain such a list, and
+  then we could save it into a struct with three lists. (from,to,empty)
+  This will need a sys allVariables list.
+- Timer output is broken for values e.g. above an hour. Fix or remove
+  altogether.
+- ns3 doesn't even reach a claim in --cl and -t8. Check.
+- in Runs.c, revise 'untrustedAgent' to cope with some weird exceptions.
+- CLP: variables in keys must be branched: maybe even in three situations
+  (have key and contents, have inverse key and content, nothing)
+- Implement delayed protocol compiler (on run demand only).
+- Implement run knowledge, and use this in protocol compiler.
+- Remove any remaining global variables, if any.
+- When choosing agents for runs (with an initial read), it does not make
+  sense to choose untrusted agents.
+- Introduce 'Ticket' default type in the compiler, along with some
+  handling for that.
+- Make a shell script 'test $filename $commandline'
+  Generates a $test-$date.out and $test-$date.err. Useful for storing
+  test data.
+- How should claims behave (trusted/untrusted) wrt uninstantiated
+  agents? Branch again? That's what is causing the nsl3-var problem.
+- The 'choose' operator must always be typed, I think.
+- Synchronisation test can be expensive, because a good protocol will
+  yield few such tests, and a bad protocol will prune most traces after
+  failure. The performance loss will only be 'felt' when the whole state
+  space is explored (-p0), which is only used for theoretical tests.
+- The woolam-ce is incorrect because it is illegal to have a variable
+  term in a key that is read, by CMV semantics. I don't know what it
+  means for CE semantics (yet).
+- Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
+  1. These local terms are given to the intruder. Technically this
+  should only happen _after_ they are first sent in the run. Maybe add
+  this to send semantics: if termOccurs(sendterm, compromisedterm) then
+  add compromisedterm to M, remove compromisedterm from list of terms to
+  compromise.
+  2. All claims in the run are ignored (add untrusted flag to run)
+  Alternative: run x.x(x) untrusted; or just compromised, to give up
+  all constants.
+  Note this is not sufficient yet, because it does not consider any
+  partner runs. Maybe declare a 'compromised' section first; other runs
+  will only activate after these have completed. Note this is much more
+  expensive.
+- Issue: how do untrusted claims work in the context of an intruder?
+  Claim must be checked if it can be solved such that at least one of 
+  the agents is trusted.
+- Fix the first environment read with a special (hidden) label.
+  1. Hide it or print differently in output.
+  2. Ensure typed matching for it, even when using -m1 switch.
+- Woolam-ce gives nothing. But then again, it's a wrong impl.
+- consider option -finline-functions for gcc, test.
+- Currently, match_basic unrolls substitutions to compare message with
+  the forbidden list, but I don't think that it is required. Test.
+- -m2 is much better with a lot of variables. Compare this to unfolding
+  of the runs with -t4 -m0/1.
+- Global/protocol variables should not exist in the current system.
+- File freopen stuff, instead of this sdtin stuff.
+- Solve the 'version' issue. How is it defined?
+- run nsl.initiator(alice, all Agent) constructs?
+  - 'all' would generate the roles with the corresponding type.
+  - or maybe for clarity/complexity control: use 'runs' for constructs
+    with 'all' in it.
+- Constraints might be a part of a knowledge thing, because with we
+  might now have a number of local knowledge sets, each with their own
+  constraint sets. That doesn't make it easier though :( and will cause
+  some performance loss I suppose. Each local set has to remain
+  solveable as well.
+- Maybe function application ought to be a different basic term type.
+- After role construction, msc consistency can be checked.
+- Make sure module knowledge has an interface instead of reference to
+  internals (i.e. no ref to basic/encr)
+- Reduce knowledge to a simple term list? That would simplify a number
+  of things, and also allow for easier addition of stuff.
+- How is % notation handled in Casper?
+- Vernam encryption?
+- Count number of illegal injections rejected for statistics.
diff --git a/src/tracebuf.c b/src/tracebuf.c
new file mode 100644
index 0000000..484717f
--- /dev/null
+++ b/src/tracebuf.c
@@ -0,0 +1,200 @@
+/*
+ * tracebuf.c
+ *
+ * trace buffer operations
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "runs.h"
+#include "memory.h"
+#include "tracebuf.h"
+#include "varbuf.h"
+
+/* reconstruct the knowledge sequence, -1 if it can be done, event nr of last depending read otherwise.
+ * There is one exception: if it returns tb->length, the required terms are not in the last knowledge 
+ */
+
+int
+tracebufRebuildKnow(struct tracebuf *tb)
+{
+  Knowledge k;
+  Roledef rd;
+  int i;
+  int flag;
+  Termlist tl;
+
+  if (tb == NULL || tb->length == 0)
+    {
+      /* stupid, but true */
+      return -1;
+    }
+
+  flag = -1;
+  k = knowledgeDuplicate(tb->know[0]);
+  i = 0;
+  while (i < tb->length)
+    {
+      rd = tb->event[i];
+      if (tb->status[i] != S_RED)
+	{
+	  /* simulate execution of the event */
+	  switch (rd->type)
+	    {
+	    case READ:
+	      if (!inKnowledge (k, rd->message))
+		{
+		  flag = i;
+		}
+	      break;
+	    case SEND:
+	      knowledgeAddTerm (k, rd->message);
+	      break;
+	    case CLAIM:
+	      /* TODO parse term requirements ? */
+	      /* Probably not needed */
+	      break;
+	    default:
+	      /* Anything else */
+	      break;
+	    }
+	}
+      /* write the new knowledge, overwriting old stuff */
+      knowledgeDelete (tb->know[i+1]);
+      tb->know[i+1] = knowledgeDuplicate (k);
+
+      i++;
+    }
+  tl = tb->requiredterms;
+  while (tl != NULL)
+    {
+      if (!inKnowledge (k, tl->term))
+        {
+          flag = tb->length;
+        }
+      tl = tl->next;
+    }
+  knowledgeDelete(k);
+  return flag;
+}
+
+/*
+ * traceBufInit
+ *
+ * initializes the trace buffer.
+ */
+
+struct tracebuf*
+tracebufInit (void)
+{
+  struct tracebuf *tb = (struct tracebuf *) memAlloc(sizeof(struct tracebuf));
+  tb->length = 0;
+  tb->reallength = 0;
+  tb->event = NULL;
+  tb->know = NULL;
+  tb->run = NULL;
+  tb->status = NULL;
+  tb->link = NULL;
+  tb->requiredterms = NULL;
+  tb->violatedclaim = 0;
+  tb->variables = NULL;
+  return tb;
+}
+
+void
+tracebufDone (struct tracebuf *tb)
+{
+  if (tb == NULL)
+    {
+      return;
+    }
+
+  Roledef rd;
+
+  varbufDone (tb->variables);
+  if (tb->length > 0)
+    {
+      int i;
+
+      i = 0;
+      /* note: knowledge domain is length+1 */
+      knowledgeDelete(tb->know[0]);
+      while (i < tb->length)
+	{
+      	  rd = tb->event[i];
+	  termDelete (rd->from);
+	  termDelete (rd->to);
+	  termDelete (rd->message);
+          roledefDelete(rd);
+	  knowledgeDelete(tb->know[i+1]);
+	  i++;
+	}
+
+      memFree(tb->know, (i+1) * sizeof (struct knowledge*));
+      memFree(tb->event, i * sizeof (struct roledef*));
+      memFree(tb->run, i * sizeof(int));
+      memFree(tb->status, i * sizeof(int));
+      memFree(tb->link, i * sizeof(int));
+    }
+  memFree(tb, sizeof(tracebuf));
+}
+
+struct tracebuf*
+tracebufSet (const System sys, int length, int claimev)
+{
+  struct tracebuf *tb;
+  int i;
+  Roledef rd;
+
+  /* TODO For the constraint logic approach, we would simply insert 
+   * any constant from the constraint for a variable.
+   */
+
+  tb = tracebufInit();
+  if (length == 0)
+    {
+      return tb;
+    }
+  tb->length = length;
+  tb->reallength = length;
+  tb->variables = (Varbuf) varbufInit (sys);
+  tb->event = (Roledef *) memAlloc(length * sizeof(struct roledef*));
+  tb->status = (int *) memAlloc(length * sizeof(int));
+  tb->link = (int *) memAlloc(length * sizeof(int));
+  tb->run = (int *) memAlloc(length * sizeof(int));
+  tb->know = (Knowledge *) memAlloc((length + 1) * sizeof (struct knowledge*));
+
+  /* when duplicating the knowledge, we want to instantiate the variables as well
+   */
+
+  tb->know[0] = knowledgeSubstDo (sys->traceKnow[0]);
+
+  i = 0;
+  while (i < length)
+    {
+      rd = roledefDuplicate1 (sys->traceEvent[i]);
+      if (rd == NULL)
+	{
+	  printf("Empty event in trace at %i of %i?\n",i,length);
+	  exit(1);
+	}
+
+      /* make a copy without variables */ 
+      rd->to      = termDuplicateUV (rd->to);
+      rd->from    = termDuplicateUV (rd->from);
+      rd->message = termDuplicateUV (rd->message);
+
+      tb->event[i] = rd;
+      tb->link[i] = -1;
+      tb->status[i] = S_UNK;
+      tb->run[i] = sys->traceRun[i];
+      tb->know[i+1] = NULL;
+      i++;
+    }
+
+  /* mark claim */
+  tb->violatedclaim = claimev;
+  tb->status[claimev] = S_OKE;
+  tracebufRebuildKnow (tb);
+  return tb;
+}
diff --git a/src/tracebuf.h b/src/tracebuf.h
new file mode 100644
index 0000000..1b95482
--- /dev/null
+++ b/src/tracebuf.h
@@ -0,0 +1,27 @@
+#ifndef TRACEBUF
+#define TRACEBUF
+
+#include "terms.h"
+#include "termlists.h"
+#include "knowledge.h"
+#include "runs.h"
+
+/* STATUS symbols */
+#define S_UNK 0 // UNKnown   : unprocessed.
+#define S_OKE 1 // OKE       : done, but required for the attack.
+#define S_RED 2 // REDundant : is not needed for attack, we're sure.
+#define S_TOD 3	// TODo      : The previous suggestion REQ was too similar to RED.
+		//             This is reserved for reads.
+
+
+/*
+ * tracebuf struct is defined in runs.h to avoid loops.
+ */
+
+int tracebufRebuildKnow(struct tracebuf *tb);
+struct tracebuf* tracebufInit (void);
+void tracebufDone (struct tracebuf *tb);
+struct tracebuf* tracebufSet (const System sys, int length, int claimev);
+
+
+#endif
diff --git a/src/varbuf.c b/src/varbuf.c
new file mode 100644
index 0000000..bff1660
--- /dev/null
+++ b/src/varbuf.c
@@ -0,0 +1,94 @@
+/*
+ * varbuf.c
+ *
+ * Operations on a variable substitutions buffer.
+ * The type is actually defined in runs.h
+ */
+
+#include "memory.h"
+#include "runs.h"
+
+/*
+ * create a new varbuffer from the current state of the system
+ */
+
+Varbuf
+varbufInit (System sys)
+{
+  Varbuf vb;
+  Termlist tl;
+  Term termfrom, termto;
+  
+  vb = (Varbuf) memAlloc(sizeof(struct varbuf));
+  vb->from = NULL;
+  vb->to = NULL;
+  vb->empty = NULL;
+  tl = sys->variables;
+  while (tl != NULL)
+    {
+      if (realTermVariable(tl->term))
+	{
+	  /* this is actually a variable */
+	  if (tl->term->subst == NULL)
+	    {
+	      /* non-instantiated */
+	      vb->empty = termlistAdd (vb->empty, tl->term);
+	    }
+	  else
+	    {
+	      /* store instantiation */
+	      termfrom = tl->term;
+	      termto = termfrom->subst;
+	      termfrom->subst = NULL;	// temp disable
+	      vb->from = termlistAdd (vb->from, termfrom);
+	      vb->to = termlistAdd (vb->to, termto);
+	      termfrom->subst = termto;	// restore
+	    }
+	}
+      tl = tl->next;
+    }
+  return vb;
+}
+
+/*
+ * copy the variable state back into the system
+ */
+
+void
+varbufSet (System sys, Varbuf vb)
+{
+  Termlist tl1, tl2;
+
+  tl1 = vb->from;
+  tl2 = vb->to;
+  while (tl1 != NULL && tl2 != NULL)
+    {
+      tl1->term->subst = tl2->term;
+      tl1 = tl1->next;
+      tl2 = tl2->next;
+    }
+  tl1 = vb->empty;
+  while (tl1 != NULL)
+    {
+      tl1->term->subst = NULL;
+      tl1 = tl1->next;
+    }
+}
+
+/*
+ * cleanup
+ */
+
+void
+varbufDone (Varbuf vb)
+{
+  if (vb != NULL)
+    {
+      termlistDelete (vb->from);
+      termlistDelete (vb->to);
+      termlistDelete (vb->empty);
+      memFree(vb, sizeof(struct varbuf));
+    }
+}
+
+
diff --git a/src/varbuf.h b/src/varbuf.h
new file mode 100644
index 0000000..b68c348
--- /dev/null
+++ b/src/varbuf.h
@@ -0,0 +1,10 @@
+#ifndef VARBUF
+#define VARBUF
+
+#include "runs.h"
+
+Varbuf varbufInit (System sys);
+void varbufSet (System sys, Varbuf vb);
+void varbufDone (Varbuf vb);
+
+#endif