- Changed my mind.
--prune 0 : all attacks --prune 1 : select first attack --prune 2+: use heuristic (currently only 2 supported)
This commit is contained in:
parent
a8dee79504
commit
dcb1625c3a
32
src/cost.c
32
src/cost.c
@ -34,6 +34,22 @@ attackCost (const System sys)
|
|||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
if (switches.prune == 1)
|
if (switches.prune == 1)
|
||||||
|
{
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (switches.prune == 2)
|
||||||
{
|
{
|
||||||
// Use nice heuristic cf. work of Gijs Hollestelle. Hand-picked parameters.
|
// Use nice heuristic cf. work of Gijs Hollestelle. Hand-picked parameters.
|
||||||
int cost;
|
int cost;
|
||||||
@ -51,21 +67,5 @@ attackCost (const System sys)
|
|||||||
|
|
||||||
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)");
|
error ("Unknown pruning method (cost function not found)");
|
||||||
}
|
}
|
||||||
|
@ -41,7 +41,7 @@ switchesInit (int argc, char **argv)
|
|||||||
switches.tupling = 0;
|
switches.tupling = 0;
|
||||||
|
|
||||||
// Pruning and Bounding
|
// Pruning and Bounding
|
||||||
switches.prune = 1; // default pruning method (use heuristic)
|
switches.prune = 2; // default pruning method (use nice heuristic)
|
||||||
switches.maxproofdepth = INT_MAX;
|
switches.maxproofdepth = INT_MAX;
|
||||||
switches.maxtracelength = 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
|
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)
|
if (!process)
|
||||||
{
|
{
|
||||||
/* not very important
|
/* not very important
|
||||||
helptext (" --prune=<int>", "pruning method when an attack is found [1]");
|
helptext (" --prune=<int>", "pruning method when an attack is found [2]");
|
||||||
*/
|
*/
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
Loading…
Reference in New Issue
Block a user