diff --git a/src/main.c b/src/main.c index 5a6db41..20f5074 100644 --- a/src/main.c +++ b/src/main.c @@ -103,6 +103,8 @@ main (int argc, char **argv) struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions."); struct arg_lit *switchAS = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions."); struct arg_lit *switchSO = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions."); + struct arg_lit *switchNC = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions."); + struct arg_lit *switchRE = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions."); #ifdef DEBUG struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter."); struct arg_lit *switchI = arg_lit0 ("I", "debug-indent", @@ -131,6 +133,8 @@ main (int argc, char **argv) switchRS, switchAS, switchSO, + switchNC, + switchRE, #ifdef DEBUG porparam, switchI, @@ -289,11 +293,13 @@ main (int argc, char **argv) sys->switchReadSymm = 1; } if (switchSO->count > 0) - /* enable symmetry order */ - sys->switchSymmOrder = 1; + sys->switchSymmOrder = 1; /* enable symmetry order */ if (switchAS->count > 0) - /* disable agent symmetry order */ - sys->switchAgentSymm = 0; + sys->switchAgentSymm = 0; /* disable agent symmetry order */ + if (switchNC->count > 0) + sys->switchNomoreClaims = 0; /* disable no more claims cutter */ + if (switchRE->count > 0) + sys->switchReduceEndgame = 0; /* disable endgame cutter */ #ifdef DEBUG sys->porparam = porparam->ival[0]; diff --git a/src/modelchecker.c b/src/modelchecker.c index 3216068..6c7102e 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -280,7 +280,7 @@ explorify (const System sys, const int run) * further traversal. */ //!@todo This implementation relies on the fact that there are only secrecy, synchr and agreement properties. - if (sys->secrets == NULL) + if (sys->switchNomoreClaims && sys->secrets == NULL) { /* there are no remaining secrecy claims to be checked */ Roledef rdscan; int validclaim; @@ -349,8 +349,8 @@ explorify (const System sys, const int run) /* Special check 3: if after choosing, this run ends on (read|skippedclaim)*, we can remove that part already. */ - roleCap = removeIrrelevant (sys, run, rd); - + if (sys->switchReduceEndgame) + roleCap = removeIrrelevant (sys, run, rd); /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted, * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not diff --git a/src/runs.c b/src/runs.c index 212e8ec..74989d5 100644 --- a/src/runs.c +++ b/src/runs.c @@ -68,6 +68,8 @@ systemInit () sys->switchReadSymm = 0; // don't force read symmetries by default sys->switchAgentSymm = 1; // default enable agent symmetry sys->switchSymmOrder = 0; // don't force symmetry order reduction by default + sys->switchNomoreClaims = 1; // default cutter when there are no more claims + sys->switchReduceEndgame = 1; // default cutter of last events in a trace /* set illegal traversal by default, to make sure it is set later */ diff --git a/src/runs.h b/src/runs.h index e4e25d7..fe5a22c 100644 --- a/src/runs.h +++ b/src/runs.h @@ -213,6 +213,8 @@ struct system int switchReadSymm; //!< Enable read symmetry reduction int switchAgentSymm; //!< Enable agent symmetry reduction int switchSymmOrder; //!< Enable symmetry order reduction + int switchNomoreClaims; //!< Enable no more claims cutter + int switchReduceEndgame; //!< Enable endgame cutter //! Latex output switch. /**