diff --git a/src/arachne.c b/src/arachne.c index 53728c1..3c88c7e 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -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; diff --git a/src/compiler.c b/src/compiler.c index 1542aaf..6bd20f6 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -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 diff --git a/src/role.h b/src/role.h index 7b5c183..3d791b7 100644 --- a/src/role.h +++ b/src/role.h @@ -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.