diff --git a/src/main.c b/src/main.c index d40d702..522f1ec 100644 --- a/src/main.c +++ b/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 */ diff --git a/src/modelchecker.c b/src/modelchecker.c index 9e8089f..7317213 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -237,21 +237,11 @@ executeStep (const System sys, const int run) return 1; } -/** - * 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. - */ +//! Determine end of run after removing end reads, and optionally claims. 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, - sys->runs[ridSymm].agents) < 0) + int order; + + 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, diff --git a/src/system.c b/src/system.c index 0d84373..714c2d0 100644 --- a/src/system.c +++ b/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 @@ -647,10 +648,10 @@ roleInstanceDestroy (const System sys) if (sys->engine == ARACHNE_ENGINE) { // Remove artefacts - artefacts = myrun.artefacts; + artefacts = myrun.artefacts; while (artefacts != NULL) { - memFree(artefacts->term, sizeof (struct term)); + memFree (artefacts->term, sizeof (struct term)); artefacts = artefacts->next; } } diff --git a/src/system.h b/src/system.h index 791b5cb..5ed620a 100644 --- a/src/system.h +++ b/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?