- Secrecy claims are now handled fairly okayish, as long as only one

term is in the claim. This should be tupling-or, really, for
  convenience.
This commit is contained in:
ccremers 2004-08-14 19:19:23 +00:00
parent 18415c95a2
commit 0fee6b5797
3 changed files with 31 additions and 1 deletions

View File

@ -18,6 +18,10 @@
#include "claim.h"
#include "debug.h"
extern CLAIM_Secret;
extern CLAIM_Nisynch;
extern CLAIM_Niagree;
static System sys;
Protocol INTRUDER; // Pointers, to be set by the Init
Role I_GOAL; // Same here.
@ -715,6 +719,18 @@ prune ()
return 0;
}
//! Setup system for specific claim test
add_claim_specifics (Claimlist cl, Roledef rd)
{
if (isTermEqual (cl->type, CLAIM_Secret))
{
/**
* Secrecy claim
*/
create_intruder_goal (rd->message);
}
}
//------------------------------------------------------------------------
// Main logic core
//------------------------------------------------------------------------
@ -877,6 +893,12 @@ arachne ()
roleInstance (sys, p, r, NULL);
sys->runs[0].length = cl->ev + 1;
/**
* Add specific goal info
*/
add_claim_specifics (cl, roledef_shift(sys->runs[0].start, cl->ev));
#ifdef DEBUG
if (DEBUGL (5))
{
@ -890,7 +912,10 @@ arachne ()
iterate ();
//! Destroy
roleInstanceDestroy (sys);
while (sys->maxruns > 0)
{
roleInstanceDestroy (sys);
}
// next
cl = cl->next;

View File

@ -467,6 +467,7 @@ commEvent (int event, Tac tc)
cl->protocol = thisProtocol;
cl->rolename = fromrole;
cl->role = thisRole;
cl->roledef = NULL;
cl->count = 0;
cl->failed = 0;
cl->prec = NULL;
@ -1113,6 +1114,8 @@ compute_prec_sets (const System sys)
// Store in claimlist structure
cl->r = r1;
cl->ev = ev1;
cl->roledef = rd;
/*
* We have found the claim roledef, and r1,ev1
* Now we compute the preceding label set

View File

@ -24,6 +24,8 @@ struct claimlist
Term rolename;
//! The pointer to the role structure
void *role;
//! The pointer to the roledef
void *roledef;
//! Number of occurrences in system exploration.
states_t count;
//! Number of occurrences that failed.