- Fixed bug in new --max-attacks semantics.

This commit is contained in:
ccremers 2006-11-23 10:40:10 +00:00
parent e28c494a18
commit d8414daf95
3 changed files with 21 additions and 10 deletions

View File

@ -45,10 +45,10 @@ prune_bounds (const System sys)
return 1; return 1;
} }
/* prune for number of attacks */ /* prune for number of attacks if we are actually outputting them */
if (enoughAttacks (sys)) if (enoughAttacks (sys))
{ {
// Oh no, we ran out of time! // Oh no, we ran out of possible attacks!
if (switches.output == PROOF) if (switches.output == PROOF)
{ {
indentPrint (); indentPrint ();

View File

@ -762,6 +762,13 @@ switcher (const int process, int index, int commandline)
{ {
/* not very important /* not very important
helptext (" --prune=<int>", "pruning method when an attack is found [2]"); helptext (" --prune=<int>", "pruning method when an attack is found [2]");
Semantics:
0 - Show all attacks (up to the maximum)
1 - Show first attack
2 - Show 'best' attack (use heuristics)
Thus, a value of '0' means multiple attacks are output, otherwise just one.
*/ */
} }
else else

View File

@ -1202,6 +1202,9 @@ scenarioPrint (const System sys)
int int
enoughAttacks (const System sys) enoughAttacks (const System sys)
{ {
// Only if we are outputting more than one
if (switches.prune == 0)
{
if (switches.maxAttacks != 0) if (switches.maxAttacks != 0)
{ {
if (sys->attackid >= switches.maxAttacks) if (sys->attackid >= switches.maxAttacks)
@ -1209,6 +1212,7 @@ enoughAttacks (const System sys)
return 1; return 1;
} }
} }
}
return 0; return 0;
} }