- Implemented --no-noclaims-red and --no-endgame-red

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];

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,9 +349,9 @@ 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.
        */
 
+      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
        * be violated anymore if they contain no terms that are encrypted with such keys */

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 */

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.
   /**