- Added claim symmetry reduction; this doesn't help much for lower

number of runs. It is on by default.

src/main.c

@@ -135,6 +135,9 @@ main (int argc, char **argv)
 	      "disable no more claims reductions");
   struct arg_lit *switch_disable_endgame_reductions =
     arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
+  struct arg_lit *switch_disable_claim_symmetry =
+    arg_lit0 (NULL, "no-claimsymmetry-red",
+	      "disable claim symmetry reductions");
   struct arg_lit *switch_summary = arg_lit0 (NULL, "summary",
 					     "show summary on stdout instead of stderr");
   struct arg_lit *switch_echo =
@@ -178,6 +181,7 @@ main (int argc, char **argv)
     switch_disable_agent_symmetries,
     switch_disable_noclaims_reductions,
     switch_disable_endgame_reductions,
+    switch_disable_claim_symmetry,
 #ifdef DEBUG
     switch_por_parameter,
     switch_debug_indent,
@@ -368,6 +372,8 @@ main (int argc, char **argv)
     sys->switchNomoreClaims = 0;	/* disable no more claims cutter */
   if (switch_disable_endgame_reductions->count > 0)
     sys->switchReduceEndgame = 0;	/* disable endgame cutter */
+  if (switch_disable_claim_symmetry->count > 0)
+    sys->switchReduceClaims = 0;	/* disable claim symmetry cutter */
   if (switch_summary->count > 0)
     sys->output = SUMMARY;	/* report summary on stdout */
 

src/modelchecker.c

@@ -237,21 +237,11 @@ executeStep (const System sys, const int run)
   return 1;
 }
 
-/**
+//! Determine end of run after removing end reads, and optionally claims.
- * Determine for a roledef that is instantiated, the uninteresting ends bits.
- *
- *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties.
- */
 Roledef
-removeIrrelevant (const System sys, const int run, Roledef rd)
+removeDangling (Roledef rd, const int killclaims)
 {
   Roledef rdkill;
-  int killclaims;
-
-  if (untrustedAgent (sys, sys->runs[run].agents))
-    killclaims = 1;
-  else
-    killclaims = 0;
 
   rdkill = rd;
   while (rd != NULL)
@@ -260,26 +250,30 @@ removeIrrelevant (const System sys, const int run, Roledef rd)
 	rdkill = rd;
       rd = rd->next;
     }
-  /* report part */
-  /*
-     rd = rdkill->next;
-     killclaims = 0;
-     while (rd != NULL)
-     {
-     killclaims++;
-     rd = rd->next;
-     }
-     if (killclaims > 1)
-     {
-     warning ("%i events stripped from run %i.", killclaims, run);
-     runPrint (rdkill->next);
-     }
-   */
-
   /* remove after rdkill */
   return rdkill;
 }
 
+/**
+ * Determine for a roledef that is instantiated, the uninteresting ends bits.
+ *
+ *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties.
+ */
+Roledef
+removeIrrelevant (const System sys, const int run, Roledef rd)
+{
+  if (untrustedAgent (sys, sys->runs[run].agents))
+    {
+      // untrusted, so also remove claims
+      return removeDangling (rd, 1);
+    }
+  else
+    {
+      // trusted, so only remove reads
+      return removeDangling (rd, 0);
+    }
+}
+
 
 //! Unblock any waiting sends of my type.
 /**
@@ -438,19 +432,29 @@ explorify (const System sys, const int run)
 	  else
 	    {
 	      /* dependent run has chosen, so we can compare */
-	      if (termlistOrder (sys->runs[run].agents,
+	      int order;
-				 sys->runs[ridSymm].agents) < 0)
+
+	      order =
+		termlistOrder (sys->runs[run].agents,
+			       sys->runs[ridSymm].agents);
+	      if (order < 0)
 		{
 		  /* we only explore the other half */
 		  return 0;
 		}
+	      if (order == 0 && sys->switchReduceClaims)
+		{
+		  /* identical run; only the first would be checked for a claim */
+		  /* so we cut off this run, including claims, turning it into a dummy run */
+		  roleCap = removeDangling (rd, 1);
+		}
 	    }
 	}
 
       /* Special check 3: if after choosing, this run ends on (read|skippedclaim)*, we can remove that part already.
        */
 
-      if (sys->switchReduceEndgame)
+      if (sys->switchReduceEndgame && roleCap == NULL)
 	roleCap = removeIrrelevant (sys, run, rd);
 
       /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted,

src/system.c

@@ -66,6 +66,7 @@ systemInit ()
   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
+  sys->switchReduceClaims = 1;	// default remove claims from duplicate instance choosers
   sys->switchClaims = 0;	// default don't report on claims
   sys->switchClaimToCheck = NULL;	// default check all claims
 

src/system.h

@@ -135,6 +135,7 @@ struct system
   int switchSymmOrder;		//!< Enable symmetry order reduction
   int switchNomoreClaims;	//!< Enable no more claims cutter
   int switchReduceEndgame;	//!< Enable endgame cutter
+  int switchReduceClaims;	//!< Symmetry reduction on claims (only works when switchAgentSymm is true)
   int switchClaims;		//!< Enable clails report
   Term switchClaimToCheck;	//!< Which claim should be checked?