From 56f7cf5df22bf0a652e58b11c78d7c74135f168d Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 12 Aug 2005 07:28:44 +0000 Subject: [PATCH] - 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. --- .tdldb | Bin 261 -> 415 bytes spdl/multiparty/test-variants.py | 33 +++++++++++--- src/switches.c | 16 +++++++ src/switches.h | 1 + src/tac.c | 76 ++++++++++++++++++++++++++++--- 5 files changed, 113 insertions(+), 13 deletions(-) diff --git a/.tdldb b/.tdldb index d92a1c6e5975045fa3d5cafd83c7e5445ecb8f63..69aeceeec91508c5281a1812bbbbe0295f17cdd5 100644 GIT binary patch delta 172 zcmXAiAr1mT3`J)dvj&U7RPG8m1Si0efSL@2*}!&^wj)-d5J)77gK#HqKtdNPn)loP z+w0`%>&MGg&N+XtKbO^ex-%+A*>K delta 16 XcmbQw+{(l;b2kGc0|NuoM2^1zBAx^v diff --git a/spdl/multiparty/test-variants.py b/spdl/multiparty/test-variants.py index bcb9ecc..f73f1e1 100755 --- a/spdl/multiparty/test-variants.py +++ b/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) - for P in range(2,7): - for runs in range(P-1,P+2): + candidates = startset() + for P in range(3,7): + for runs in range(P-1,P+3): candidates = scan(candidates,P,runs) print print "Good variants:" diff --git a/src/switches.c b/src/switches.c index 0775de3..d9dfb0a 100644 --- a/src/switches.c +++ b/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 */ diff --git a/src/switches.h b/src/switches.h index b81b8c1..774626a 100644 --- a/src/switches.h +++ b/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. diff --git a/src/tac.c b/src/tac.c index 20b6127..b3f2e33 100644 --- a/src/tac.c +++ b/src/tac.c @@ -1,31 +1,37 @@ #include #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) - * Effectively, this defines how we interpret tuples with - * more than two components. - */ - +//! List to right-associative tuple 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.