- Added switch '--la-tupling' to enforce left-associative tupling

instead of the default right-associative tupling. Note that this only
  matters for full typeflaw matching.
- Adapted multi-nsl test script to test for both association variants.

spdl/multiparty/test-variants.py

@@ -8,10 +8,25 @@
 #
 import commands
 
-def testvariant(variant,P,runs):
+def startset():
+	return range(0,32)
+	
+	mainlist = [11, 12, 15, 28]
+	print "Starting with", mainlist
+	return mainlist
+
+def tuplingchoice(variant,P,runs,latupling):
+	#	variant is in range [0..64>,
+	#	where we use the highest bid to signify the
+	#	associativity of the tupling.
+
+	extraflags = ""
+	if latupling:
+		extraflags += " --la-tupling"
+
 	s = "./multinsl-generator.py"
 	s += " %i %s" % (P,variant)
-	s += " | scyther -a -r%i -m2 --summary" % runs
+	s += " | scyther -a -r%i -m2 --summary %s" % (runs, extraflags)
 	#s += " | scyther -a -r%i --summary" % runs
 	#print s
 	s += " | grep \"failed:\""
@@ -23,6 +38,12 @@ def testvariant(variant,P,runs):
 		#print out
 		return False
 
+def testvariant(v,p,r):
+	if not tuplingchoice (v,p,r, False):
+		return False
+	else:
+		return tuplingchoice (v,p,r, True)
+
 def removeattacks (testlist, P, runs):
 	okaylist = []
 	for v in testlist:
@@ -39,14 +60,14 @@ def scan(testlist, P, runs):
 			if testlist[i] not in results:
 				attacked.append(testlist[i])
 		print "Using P %i and %i runs, we find attacks on %s" % (P,runs, str(attacked))
-		print "Therefore, we are left with %i candidates: " % (len(testlist)), results 
+		print "Therefore, we are left with %i candidates: " % (len(results)), results 
 
 	return results
 
 def main():
-	candidates = range(0,32)
+	candidates = startset()
-	for P in range(2,7):
+	for P in range(3,7):
-		for runs in range(P-1,P+2):
+		for runs in range(P-1,P+3):
 			candidates = scan(candidates,P,runs)
 	print
 	print "Good variants:"

src/switches.c

@@ -39,6 +39,7 @@ switchesInit (int argc, char **argv)
   switches.engine = POR_ENGINE;	// default is partial ordering engine
   switches.match = 0;		// default matching
   switches.clp = 0;
+  switches.la_tupling = false;
 
   // Pruning and Bounding
   switches.prune = 2;		// default pruning method
@@ -377,6 +378,21 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "la-tupling", 0))
+    {
+      if (!process)
+	{
+	  /* not very important
+	     helptext ("--la-tupling", "compile using left-associative tupling");
+	   */
+	}
+      else
+	{
+	  switches.la_tupling = true;
+	  return index;
+	}
+    }
+
   /* ==================
    *  Modelchecker only
    */

src/switches.h

@@ -18,6 +18,7 @@ struct switchdata
   int engine;			//!< Engine type (POR_ENGINE,ARACHNE_ENGINE)
   int match;			//!< Matching type.
   int clp;			//!< Do we use clp?
+  int la_tupling;		//!< Tupling is by default right-associative, optionally left-associative.
 
   // Pruning and Bounding
   int prune;			//!< Type of pruning.

src/tac.c

@@ -1,31 +1,37 @@
 #include <stdio.h>
 #include "tac.h"
 #include "memory.h"
+#include "switches.h"
 
 extern int yylineno;
 
 static Tac allocatedTacs;
 
+//! Init segment
 void
 tacInit (void)
 {
   allocatedTacs = NULL;
 }
 
+//! Closing segment
 void
 tacDone (void)
 {
-  Tac ts, tf;
+  Tac ts;
 
   ts = allocatedTacs;
   while (ts != NULL)
     {
+      Tac tf;
+
       tf = ts;
       ts = ts->allnext;
       memFree (tf, sizeof (struct tacnode));
     }
 }
 
+//! Create a tac node of some type
 Tac
 tacCreate (int op)
 {
@@ -90,13 +96,9 @@ tacCat (Tac t1, Tac t2)
     }
 }
 
-/* in: a list. out: a tuple (for e.g. associativity)
+//! List to right-associative tuple
- * Effectively, this defines how we interpret tuples with
- * more than two components.
- */
-
 Tac
-tacTuple (Tac taclist)
+tacTupleRa (Tac taclist)
 {
   Tac tc;
 
@@ -120,6 +122,66 @@ tacTuple (Tac taclist)
   return tc;
 }
 
+//! List to left-associative tuple
+Tac
+tacTupleLa (Tac taclist)
+{
+  Tac tc;
+
+  /* initial node is simple the first item */
+  tc = taclist;
+  tc->prev = NULL;
+
+  /* add any other nodes (one is ensured) */
+  do
+    {
+      Tac tcnew;
+
+      taclist = taclist->next;
+      /* add a new node (taclist) to the existing thing by first making the old one into the left-hand side of a tuple */
+      tcnew = tacCreate (TAC_TUPLE);
+      tcnew->t1.tac = tc;
+      tcnew->t2.tac = taclist;
+      tc = tcnew;
+      /* unlink */
+      tc->t1.tac->next = NULL;
+      tc->t2.tac->prev = NULL;
+    }
+  while (taclist->next != NULL);
+
+  return tc;
+}
+
+//! Compile a list into a tuple
+/* 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)
+{
+  if (taclist == NULL || taclist->next == NULL)
+    {
+      /* just return */
+      return taclist;
+    }
+  else
+    {
+      if (switches.la_tupling)
+	{
+	  /* switch --la-tupling */
+	  /* left-associative */
+	  return tacTupleLa (taclist);
+	}
+      else
+	{
+	  /* DEFAULT behaviour */
+	  /* right-associative */
+	  return tacTupleRa (taclist);
+	}
+    }
+}
+
 /*
  * tacPrint
  * Print the tac. Only for debugging purposes.