- Improved proof reports.

- Minor (epsilon type) efficiency improvement.
This commit is contained in:
ccremers 2006-03-05 15:18:39 +00:00
parent c7605d03a3
commit 1678577ce0
3 changed files with 43 additions and 11 deletions

View File

@ -87,6 +87,7 @@ arachneInit (const System mysys)
{ {
rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL); rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
} }
Role add_role (const char *rolenamestring) Role add_role (const char *rolenamestring)
{ {
Role r; Role r;
@ -886,7 +887,10 @@ createDecryptionChain (const Binding b, const int run, const int index,
if (switches.output == PROOF) if (switches.output == PROOF)
{ {
indentPrint (); indentPrint ();
eprintf ("Bound: trying new createDecryptionChain.\n"); eprintf ("Bound ");
termPrint (b->term);
eprintf (" to r%ii%i: trying new createDecryptionChain.\n",
smallrun, 2);
} }
// Iterate with the new goal // Iterate with the new goal
@ -940,6 +944,19 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
{ {
if (sl == NULL) if (sl == NULL)
{ {
if (switches.output == PROOF)
{
Roledef rd;
indentPrint ();
eprintf ("Suppose ");
termPrint (b->term);
eprintf (" originates first at run %i, event %i, as part of ",
run, index);
rd = roledef_shift (sys->runs[run].start, index);
termPrint (rd->message);
eprintf ("\n");
}
// new create key goals, bind etc. // new create key goals, bind etc.
createDecryptionChain (b, run, index, keylist, iterate); createDecryptionChain (b, run, index, keylist, iterate);
} }
@ -960,12 +977,14 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
if (!realTermVariable (tsubst)) if (!realTermVariable (tsubst))
{ {
// Only for non-variables (i.e. local constants) // Only for non-variables (i.e. local constants)
int r1, e1, r2, e2; int r1, e1;
r1 = TermRunid (tsubst); r1 = TermRunid (tsubst);
e1 = firstOccurrence (sys, r1, tsubst, SEND); e1 = firstOccurrence (sys, r1, tsubst, SEND);
if (e1 >= 0) if (e1 >= 0)
{ {
int r2, e2;
r2 = TermRunid (tvar); r2 = TermRunid (tvar);
e2 = firstOccurrence (sys, r2, tsubst, READ); e2 = firstOccurrence (sys, r2, tsubst, READ);
if (e2 >= 0) if (e2 >= 0)

View File

@ -141,6 +141,12 @@ goal_bind (const Binding b, const int run, const int ev)
if (dependPushEvent (run, ev, b->run_to, b->ev_to)) if (dependPushEvent (run, ev, b->run_to, b->ev_to))
{ {
b->done = true; b->done = true;
if (switches.output == PROOF)
{
indentPrint ();
binding_print (b);
eprintf ("\n");
}
return true; return true;
} }
} }
@ -350,7 +356,7 @@ labels_ordered (Termmap runs, Termlist labels)
int int
valid_binding (Binding b) valid_binding (Binding b)
{ {
if (b->done && !b->blocked) if (b->done && (!b->blocked))
return true; return true;
else else
return false; return false;
@ -458,7 +464,6 @@ bindings_c_minimal ()
if (valid_binding (b)) if (valid_binding (b))
{ {
int run; int run;
int node_from;
// Find all preceding events // Find all preceding events
for (run = 0; run < sys->maxruns; run++) for (run = 0; run < sys->maxruns; run++)
@ -494,6 +499,14 @@ bindings_c_minimal ()
return false; return false;
} }
} }
else
{
// If this event is not before the target, then the
// next in the run certainly is not either (because
// that would imply that this one is before it)
// Thus, we effectively exit the loop.
break;
}
} }
} }
} }

View File

@ -249,25 +249,25 @@ termSubTerm (Term t, Term tsub)
if (isTermEqual (t, tsub)) if (isTermEqual (t, tsub))
{ {
return 1; return true;
} }
else else
{ {
if (t == NULL) if (t == NULL)
{ {
return 0; return false;
} }
else else
{ {
if (tsub == NULL) if (tsub == NULL)
{ {
return 1; return true;
} }
else else
{ {
if (realTermLeaf (t)) if (realTermLeaf (t))
{ {
return 0; return false;
} }
else else
{ {
@ -296,13 +296,13 @@ termInTerm (Term t, Term tsub)
tsub = deVar (tsub); tsub = deVar (tsub);
if (isTermEqual (t, tsub)) if (isTermEqual (t, tsub))
return 1; return true;
if (realTermLeaf (t)) if (realTermLeaf (t))
return 0; return false;
if (realTermTuple (t)) if (realTermTuple (t))
return (termInTerm (TermOp1 (t), tsub) || termInTerm (TermOp2 (t), tsub)); return (termInTerm (TermOp1 (t), tsub) || termInTerm (TermOp2 (t), tsub));
else else
return 0; return false;
} }
//! Print a term to stdout. //! Print a term to stdout.