From f883499d07aae5e99c605d5c6d84a9d39fa0f944 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Mon, 24 Jan 2011 17:32:24 +0100 Subject: [PATCH] CHANGE: Changed setup of running & commit. Now: claim(A,Commit,B,data) => claim(B,Running,A,data) and also B is running the right protocol and role. --- src/claim.c | 44 +++++++++++++++++++++++++++++++++++++++++--- src/dotout.c | 26 +++++++++++++++++++++----- src/termlist.c | 11 +++++++++++ src/termlist.h | 1 + 4 files changed, 74 insertions(+), 8 deletions(-) diff --git a/src/claim.c b/src/claim.c index ba6495e..973a7dc 100644 --- a/src/claim.c +++ b/src/claim.c @@ -771,6 +771,14 @@ arachne_claim_weakagree (const System sys, const int claim_run, } //! Test commit(X) => running(X) +/** + * To be precise: + * + * for all claim(a,Commit,b,data) => + * claim(b,Running,a,data)#rid and role(rid) == ROLE(b in claim role spec) + * + * For now we assume data is non-empty + */ int arachne_claim_commit (const System sys, const int claim_run, const int claim_index) @@ -779,8 +787,17 @@ arachne_claim_commit (const System sys, const int claim_run, int run; Roledef rd_claim; + Term actor_a; + Term actor_b; + Term partner_role; + Termlist params_a; rd_claim = roledef_shift (sys->runs[claim_run].start, claim_index); + params_a = tuple_to_termlist(rd_claim->message); + actor_a = rd_claim->from; + actor_b = params_a->term; + partner_role = termLeft(rd_claim->claiminfo->parameter); + /* * Iterate over all preceding events (include claim run for consistency with formal definition) */ @@ -803,10 +820,30 @@ arachne_claim_commit (const System sys, const int claim_run, // (Check: maybe below can also be rd->to) if (isTermEqual (rd->claiminfo->type, CLAIM_Running)) { - if (isTermEqual (rd->message, rd_claim->message)) + // Now check whether they match up nicely + // protocols should be the same + if (sys->current_claim->protocol == rd->claiminfo->protocol) { - // Claim holds - return true; + Termlist params_b; + + params_b = tuple_to_termlist(rd->message); + // check agent requirements + if (isTermEqual(rd->from,actor_b) && isTermEqual(params_b->term,actor_a)) + { + // check role (also same protocol) + if (isTermEqual(partner_role,rd->claiminfo->rolename)) + { + // check parameters + if (isTermlistEqual (params_a->next,params_b->next)) + { + // Claim holds + termlistDelete(params_b); + termlistDelete(params_a); + return true; + } + } + } + termlistDelete(params_b); } } } @@ -814,6 +851,7 @@ arachne_claim_commit (const System sys, const int claim_run, rd = rd->next; } } + termlistDelete(params_a); return false; } diff --git a/src/dotout.c b/src/dotout.c index 6ffb72c..34d6c45 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -27,6 +27,7 @@ #include "type.h" #include "debug.h" #include "error.h" +#include "specialterm.h" extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c extern Role I_M; // Same here. @@ -607,6 +608,10 @@ isCommunicationExact (const System sys, Binding b) } //! Ignore some events +/** + * Used only in graph drawing. Return true to ignore, return false to + * draw. + */ int isEventIgnored (const System sys, int run, int ev) { @@ -615,17 +620,28 @@ isEventIgnored (const System sys, int run, int ev) rd = eventRoledef (sys, run, ev); if (rd->type == CLAIM) { - if (run != 0) + // If we are doing a reachability analysis, show all + if (isTermEqual(sys->current_claim->type, CLAIM_Reachable)) { - return true; + return false; } - else + // If the claim type is commit, we also show running claims + if (isTermEqual(sys->current_claim->type, CLAIM_Commit) || isTermEqual(sys->current_claim->type, CLAIM_Reachable)) { - if (ev != sys->current_claim->ev) + if (isTermEqual(rd->claiminfo->type, CLAIM_Running)) { - return true; + return false; } } + // Remaining cases: only active claim is shown + if (run == 0) + { + if (ev == sys->current_claim->ev) + { + return false; + } + } + return true; } return false; } diff --git a/src/termlist.c b/src/termlist.c index 0506abb..832df1d 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -925,6 +925,17 @@ tuple_to_termlist (Term t) } } +//! Get the leftmost term of a tuple (e.g. a non-tuple) +Term termLeft(Term t) +{ + t = deVar(t); + if (realTermTuple (t)) + { + return termLeft(TermOp1 (t)); + } + return t; +} + //! Remove all items from tlbig that occur in tlsmall, and return the pointer to the new tlbig. Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall) diff --git a/src/termlist.h b/src/termlist.h index b65d804..efc7dce 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -77,6 +77,7 @@ int termlistOrder (Termlist tl1, Termlist tl2); int termlist_iterate (Termlist tl, int (*func) ()); Term termlist_to_tuple (Termlist tl); Termlist tuple_to_termlist (Term t); +Term termLeft(Term t); Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall); #define TERMLISTADD(l,t) l = termlistAdd (l,t)