diff --git a/src/switches.c b/src/switches.c index 7cfdd34..b6ef9a3 100644 --- a/src/switches.c +++ b/src/switches.c @@ -39,7 +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; + switches.tupling = 0; // Pruning and Bounding switches.prune = 2; // default pruning method @@ -379,21 +379,52 @@ switcher (const int process, int index) } } + if (detect (' ', "ra-tupling", 0)) + { + if (!process) + { + /* for experts only + helptext ("--ra-tupling", "compile using right-associative tupling"); + */ + } + else + { + switches.tupling = 0; + return index; + } + } + if (detect (' ', "la-tupling", 0)) { if (!process) { - /* not very important + /* for experts only helptext ("--la-tupling", "compile using left-associative tupling"); */ } else { - switches.la_tupling = true; + switches.tupling = 1; return index; } } + if (detect (' ', "tupling", 1)) + { + if (!process) + { + /* for experts only + helptext ("--tupling", "tupling type to use"); + */ + } + else + { + switches.tupling = integer_argument (); + return index; + } + } + + /* ================== * Modelchecker only */ diff --git a/src/switches.h b/src/switches.h index 00d8e9c..22a895d 100644 --- a/src/switches.h +++ b/src/switches.h @@ -18,7 +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. + int tupling; //!< Tupling is by default 0: right-associative, optionally 1: left-associative. // Pruning and Bounding int prune; //!< Type of pruning. diff --git a/src/tac.c b/src/tac.c index b3f2e33..c04d42b 100644 --- a/src/tac.c +++ b/src/tac.c @@ -167,17 +167,19 @@ tacTuple (Tac taclist) } else { - if (switches.la_tupling) - { - /* switch --la-tupling */ - /* left-associative */ - return tacTupleLa (taclist); - } - else + switch (switches.tupling) { + case 0: + /* case 0: as well as */ /* DEFAULT behaviour */ /* right-associative */ return tacTupleRa (taclist); + case 1: + /* switch --la-tupling */ + /* left-associative */ + return tacTupleLa (taclist); + default: + error ("Unknown tupling mode (--tupling=%i)", switches.tupling); } } }