diff --git a/src/arachne.c b/src/arachne.c index c504077..87b5ee6 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1916,7 +1916,7 @@ makeTraceClass (const System sys, Termlist varlist) void attackOutputStart (void) { - if (switches.prune == 2) + if (switches.prune != 0) { FILE *fd; @@ -2181,7 +2181,7 @@ iterate () int iterate_buffer_attacks (void) { - if (switches.prune != 2) + if (switches.prune == 0) { return iterate (); } diff --git a/src/cost.c b/src/cost.c index 4d025af..71b4a39 100644 --- a/src/cost.c +++ b/src/cost.c @@ -8,6 +8,7 @@ */ #include "switches.h" #include "system.h" +#include //************************************************************************ // Private methods @@ -28,18 +29,43 @@ int attackCost (const System sys) { - int cost; + if (switches.prune == 0) + { + return 0; + } + if (switches.prune == 1) + { + // Use nice heuristic cf. work of Gijs Hollestelle. Hand-picked parameters. + int cost; - cost = 0; + cost = 0; - //cost += get_semitrace_length (); + //cost += get_semitrace_length (); - cost += 10 * selfInitiators (sys); - cost += 7 * selfResponders (sys); - cost += 10 * sys->num_regular_runs; - cost += 3 * countInitiators (sys); - cost += 2 * countBindingsDone (); - cost += 1 * sys->num_intruder_runs; + cost += 10 * selfInitiators (sys); + cost += 7 * selfResponders (sys); + cost += 10 * sys->num_regular_runs; + cost += 3 * countInitiators (sys); + cost += 2 * countBindingsDone (); + cost += 1 * sys->num_intruder_runs; - return cost; + return cost; + } + if (switches.prune == 2) + { + // Select the first attack. + // Implied by having the cost of traces after finding an attack to be always higher. + // + if (sys->current_claim->failed > 0) + { + // we already have an attack + return INT_MAX; + } + else + { + // return some value relating to the cost (anything less than int_max will do) + return 1; + } + } + error ("Unknown pruning method (cost function not found)"); } diff --git a/src/prune_bounds.c b/src/prune_bounds.c index 4db30f5..cbfa3ec 100644 --- a/src/prune_bounds.c +++ b/src/prune_bounds.c @@ -137,7 +137,7 @@ prune_bounds (const System sys) } /* prune for cheaper */ - if (switches.prune == 2 && attack_leastcost <= attackCost (sys)) + if (switches.prune != 0 && attack_leastcost <= attackCost (sys)) { // We already had an attack at least this cheap. if (switches.output == PROOF) diff --git a/src/switches.c b/src/switches.c index 0b114ae..5eb248c 100644 --- a/src/switches.c +++ b/src/switches.c @@ -41,7 +41,7 @@ switchesInit (int argc, char **argv) switches.tupling = 0; // Pruning and Bounding - switches.prune = 2; // default pruning method (just output a single one) + switches.prune = 1; // default pruning method (use heuristic) switches.maxproofdepth = INT_MAX; switches.maxtracelength = INT_MAX; switches.runs = 5; // default is 5 for usability, but -r 0 or --maxruns=0 will set it back to INT_MAX @@ -711,7 +711,7 @@ switcher (const int process, int index, int commandline) if (!process) { /* not very important - helptext (" --prune=", "pruning method when an attack is found [2]"); + helptext (" --prune=", "pruning method when an attack is found [1]"); */ } else