Introduced markers in proof output for consistency with book description.

This commit is contained in:
Cas Cremers 2012-10-02 13:43:30 +02:00
parent 10c62a6863
commit 1bbd2f1ab7
5 changed files with 75 additions and 3 deletions

View File

@ -1084,6 +1084,53 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
return true;
}
//! Proof markers
void
proof_go_down(const Term label, const Term t)
{
Termlist l;
int depth;
int len;
if (switches.output != PROOF)
return;
// Prepend the terms (the list is in reverse)
TERMLISTPREPEND(sys->proofstate,label);
TERMLISTPREPEND(sys->proofstate,t);
len = termlistLength(sys->proofstate) / 2;
// Display state
eprintf("Proof state: branch at level %i\n", len);
l = termlistForward(sys->proofstate);
depth = 0;
while (l != NULL)
{
int i;
eprintf("Proof state: ");
for (i = 0; i < depth; i++)
{
eprintf(" ");
}
termPrint(l->prev->term);
eprintf("(");
termPrint(l->term);
eprintf("); ");
l = l->prev->prev;
eprintf("\n");
depth++;
}
}
void
proof_go_up(void)
{
if (switches.output != PROOF)
return;
sys->proofstate = termlistDelTerm(sys->proofstate);
sys->proofstate = termlistDelTerm(sys->proofstate);
return;
}
//! Print the current semistate
void
printSemiState ()
@ -1382,12 +1429,16 @@ bind_goal_regular_run (const Binding b)
#ifdef DEBUG
debug (5, "Trying to bind to existing run.");
#endif
proof_go_down(TERM_DeEx,b->term);
sflag = bind_existing_run (b, p, r, index);
proof_go_up();
// bind to new run
#ifdef DEBUG
debug (5, "Trying to bind to new run.");
#endif
proof_go_down(TERM_DeNew,b->term);
sflag = sflag && bind_new_run (b, p, r, index);
proof_go_up();
indentDepth--;
return sflag;
@ -1583,17 +1634,21 @@ bind_goal_all_options (const Binding b)
if (know_only)
{
// Special case: only from intruder
proof_go_down(TERM_CoOld,b->term);
flag = flag && bind_goal_old_intruder_run (b);
//flag = flag && bind_goal_new_intruder_run (b);
proof_go_up();
}
else
{
// Normal case
{
flag = bind_goal_regular_run (b);
}
flag = bind_goal_regular_run (b);
proof_go_down(TERM_CoOld,b->term);
flag = flag && bind_goal_old_intruder_run (b);
proof_go_up();
proof_go_down(TERM_CoNew,b->term);
flag = flag && bind_goal_new_intruder_run (b);
proof_go_up();
}
proofDepth--;

View File

@ -39,6 +39,10 @@
Term TERM_Agent;
Term TERM_Function;
Term TERM_Hidden;
Term TERM_CoOld;
Term TERM_CoNew;
Term TERM_DeEx;
Term TERM_DeNew;
Term TERM_Type;
Term TERM_Nonce;
Term TERM_Ticket;
@ -81,6 +85,10 @@ specialTermInit (const System sys)
langhide (TERM_Type, "Type");
langhide (TERM_Hidden, "Hidden");
langhide (TERM_Claim, "Claim");
langhide (TERM_CoOld, "Co(Old)");
langhide (TERM_CoNew, "Co(New)");
langhide (TERM_DeEx, "DeEx");
langhide (TERM_DeNew, "DeNew");
langcons (TERM_Agent, "Agent", TERM_Type);
langcons (TERM_Function, "Function", TERM_Type);

View File

@ -31,6 +31,11 @@
extern Term TERM_Agent;
extern Term TERM_Function;
extern Term TERM_Hidden;
extern Term TERM_CoOld;
extern Term TERM_CoNew;
extern Term TERM_DeEx;
extern Term TERM_DeNew;
extern Term TERM_Type;
extern Term TERM_Nonce;
extern Term TERM_Ticket;

View File

@ -128,6 +128,9 @@ systemReset (const System sys)
/* transfer switches */
sys->maxtracelength = switches.maxtracelength;
/* proof state */
sys->proofstate = NULL; // list of proof state terms
}
//! Initialize runtime system (according to cut traces, limited runs)

View File

@ -153,6 +153,7 @@ struct system
List bindings; //!< List of bindings
Claimlist current_claim; //!< The claim under current investigation
Termlist trustedRoles; //!< Roles that should be trusted for this claim (the default, NULL, means all)
Termlist proofstate; //!< State of the proof markers
};
typedef struct system *System;