- Cleaned up heuristic code. Note that there is a "hidden" heuristic:

implicitly, older goals are resolved first, if some goals have equal
  weights. This is encoded in the "w <=" comparison; if this is set to
  "w <", the heuristic becomes much less effective.
This commit is contained in:
ccremers 2006-02-23 15:03:43 +00:00
parent 10d44ad611
commit b16023bf0e
5 changed files with 74 additions and 106 deletions

View File

@ -1946,7 +1946,7 @@ iterate ()
* Check whether its a final state (i.e. all goals bound) * Check whether its a final state (i.e. all goals bound)
*/ */
b = select_goal (sys); b = (Binding) select_goal (sys);
if (b == NULL) if (b == NULL)
{ {
/* /*

View File

@ -208,7 +208,8 @@ term_noncevariables_level (const Term t)
//! Determine weight based on hidelevel //! Determine weight based on hidelevel
float float
weighHidelevel (const System sys, const Term t) weighHidelevel (const System sys, const Term t, const float massknow,
const float massprot)
{ {
unsigned int hl; unsigned int hl;
@ -217,9 +218,9 @@ weighHidelevel (const System sys, const Term t)
case HLFLAG_NONE: case HLFLAG_NONE:
return 0; return 0;
case HLFLAG_KNOW: case HLFLAG_KNOW:
return 0.3; return massknow;
case HLFLAG_PROT: case HLFLAG_PROT:
return 0.6; return massprot;
} }
return 1; return 1;
} }
@ -235,16 +236,11 @@ newkeylevel (const int level)
return 1; return 1;
} }
//! Goal selection //! Determine the weight of a given goal
/** /**
* Selects the most constrained goal. * 0 to ... (lower is better)
* *
* First selection is on level; thus, keys are selected first. * --heuristic has two distint interpretations. If it is 0 or greater, it a
*
* Because the list starts with the newest terms, and we use <= (as opposed to <), we
* ensure that for goals with equal constraint levels, we select the oldest one.
*
* --select-goal has two distint interpretations. If it is 0 or greater, it a
* selection mask. If it is smaller than 0, it is some special tactic. * selection mask. If it is smaller than 0, it is some special tactic.
* *
* selection masks for --select-goal * selection masks for --select-goal
@ -259,16 +255,60 @@ newkeylevel (const int level)
* -1: random goal selection * -1: random goal selection
* *
*/ */
float
computeGoalWeight (const System sys, const Binding b)
{
float w;
int smode;
Term t;
void erode (const float deltaw)
{
if (smode & 1)
{
w = w + deltaw;
}
smode = smode / 2;
}
// Total weight
w = 0;
// We will shift this mode variable
smode = switches.heuristic;
t = b->term;
// Determine buf_constrain levels
// Bit 0: 1 use hidelevel
erode (2 * weighHidelevel (sys, t, 0.5, 0.5));
// Bit 1: 2 key level (inverted)
erode (0.5 * (1 - b->level));
// Bit 2: 4 constrain level
erode (term_constrain_level (t));
// Bit 3: 8 nonce variables level (Cf. what I think is in Athena)
erode (term_noncevariables_level (t));
// Define legal range
if (smode > 0)
error ("--heuristic mode %i is illegal", switches.heuristic);
// Return total weight
return w;
}
//! Goal selection
/**
* Selects the most constrained goal.
*
* Because the list starts with the newest terms, and we use <= (as opposed to <), we
* ensure that for goals with equal constraint levels, we select the oldest one.
*
*/
Binding Binding
select_goal_masked (const System sys) select_goal_masked (const System sys)
{ {
List bl; List bl;
Binding best; Binding best;
float min_constrain; float best_weight;
int mode;
// mode bits local storage
mode = switches.arachneSelector;
// Find the most constrained goal // Find the most constrained goal
if (switches.output == PROOF) if (switches.output == PROOF)
@ -276,9 +316,9 @@ select_goal_masked (const System sys)
indentPrint (); indentPrint ();
eprintf ("Listing open goals that might be chosen: "); eprintf ("Listing open goals that might be chosen: ");
} }
min_constrain = FLT_MAX; best_weight = FLT_MAX;
bl = sys->bindings;
best = NULL; best = NULL;
bl = sys->bindings;
while (bl != NULL) while (bl != NULL)
{ {
Binding b; Binding b;
@ -288,88 +328,20 @@ select_goal_masked (const System sys)
// Only if not done and not blocked // Only if not done and not blocked
if (is_goal_selectable (b)) if (is_goal_selectable (b))
{ {
int allow; if (!isTermVariable (b->term))
Term gterm; {
float w;
allow = 0; w = computeGoalWeight (sys, b);
gterm = deVar (b->term);
if (mode & 8)
{
// check for singular variable
if (realTermVariable (gterm))
{
// singular variable only if it is not a role name variable
allow = !gterm->roleVar;
}
else
{
// not a singular variable, allow
allow = 1;
}
}
else
{
// Normally (mode & 8 == 0) we ignore any singular variables
allow = !realTermVariable (gterm);
}
if (allow)
{
float buf_constrain;
int buf_weight;
int smode;
void adapt (const int w, const float fl)
{
buf_constrain = buf_constrain + w * fl;
buf_weight = buf_weight + w;
}
void erode (const int w, const float fl)
{
if (smode & 1)
{
adapt (w, fl);
}
smode = smode / 2;
}
// buf_constrain is the addition of the factors before division by weight
buf_constrain = 0;
buf_weight = 0;
// Spacing between output
if (switches.output == PROOF && best != NULL) if (switches.output == PROOF && best != NULL)
eprintf (", "); eprintf (", ");
// We will shift this mode variable // Better alternative?
smode = mode; if (w <= best_weight)
// Determine buf_constrain levels
// Bit 0: 1 constrain level
erode (1, term_constrain_level (b->term));
// Bit 1: 2 key level (inverted)
erode (1, 0.5 * (1 - b->level));
// Bit 2: 4 consequence level
erode (1, termBindConsequences (sys, b->term));
// Bit 3: 8 single variables first (crappy performance, counter-intuitive anyway)
erode (1, 1 - isTermVariable (b->term));
// Bit 4: 16 nonce variables level (Cf. what I think is in Athena)
erode (1, term_noncevariables_level (b->term));
// Bit 5: 32 use hidelevel information
erode (1, weighHidelevel (sys, b->term));
// Bit 5: 64 use hidelevel information
erode (1, 2 * weighHidelevel (sys, b->term));
// Bit 6: 128 use key level
erode (1, newkeylevel (b->level));
// Define legal range
if (smode > 0)
error ("--heuristic mode %i is illegal", mode);
// Weigh result
if (buf_weight == 0 || buf_constrain <= min_constrain)
{ {
min_constrain = buf_constrain; best_weight = w;
best = b; best = b;
if (switches.output == PROOF) if (switches.output == PROOF)
eprintf ("*"); eprintf ("*");
@ -377,11 +349,7 @@ select_goal_masked (const System sys)
if (switches.output == PROOF) if (switches.output == PROOF)
{ {
termPrint (b->term); termPrint (b->term);
if (mode & 2) eprintf ("<%.2f>", w);
{
eprintf ("[%i]", b->level);
}
eprintf ("<%.2f>", buf_constrain);
} }
} }
} }
@ -437,7 +405,7 @@ select_goal_random (const System sys)
Binding Binding
select_goal (const System sys) select_goal (const System sys)
{ {
if (switches.arachneSelector >= 0) if (switches.heuristic >= 0)
{ {
// Masked // Masked
return select_goal_masked (sys); return select_goal_masked (sys);
@ -445,7 +413,7 @@ select_goal (const System sys)
else else
{ {
// Special cases // Special cases
switch (switches.arachneSelector) switch (switches.heuristic)
{ {
case -1: case -1:
return select_goal_random (sys); return select_goal_random (sys);

View File

@ -544,7 +544,7 @@ main (int argc, char **argv)
if (switch_prune_trace_length->ival[0] >= 0) if (switch_prune_trace_length->ival[0] >= 0)
switches.maxtracelength = switch_prune_trace_length->ival[0]; switches.maxtracelength = switch_prune_trace_length->ival[0];
if (switch_goal_select_method->ival[0] >= 0) if (switch_goal_select_method->ival[0] >= 0)
switches.arachneSelector = switch_goal_select_method->ival[0]; switches.heuristic = switch_goal_select_method->ival[0];
#ifdef DEBUG #ifdef DEBUG
/* in debugging mode, some extra switches */ /* in debugging mode, some extra switches */
if (switch_debug_indent->count > 0) if (switch_debug_indent->count > 0)

View File

@ -65,7 +65,7 @@ switchesInit (int argc, char **argv)
switches.scenarioSize = 0; switches.scenarioSize = 0;
// Arachne // Arachne
switches.arachneSelector = 34; // default goal selection method switches.heuristic = 3; // default goal selection method
switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events
switches.agentTypecheck = 1; // default do check agent types switches.agentTypecheck = 1; // default do check agent types
switches.concrete = true; // default removes symbols, and makes traces concrete switches.concrete = true; // default removes symbols, and makes traces concrete
@ -830,12 +830,12 @@ switcher (const int process, int index, int commandline)
{ {
if (switches.expert) if (switches.expert)
{ {
helptext (" --heuristic=<int>", "use heuristic <int> [34]"); helptext (" --heuristic=<int>", "use heuristic <int> [3]");
} }
} }
else else
{ {
switches.arachneSelector = integer_argument (); switches.heuristic = integer_argument ();
return index; return index;
} }
} }

View File

@ -43,7 +43,7 @@ struct switchdata
int scenarioSize; //!< Scenario size, also called fixed trace prefix length int scenarioSize; //!< Scenario size, also called fixed trace prefix length
// Arachne // Arachne
int arachneSelector; //!< Goal selection method for Arachne engine int heuristic; //!< Goal selection method for Arachne engine
int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt) int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
int agentTypecheck; //!< Check type of agent variables in all matching modes int agentTypecheck; //!< Check type of agent variables in all matching modes
int concrete; //!< Swap out variables at the end. int concrete; //!< Swap out variables at the end.