diff --git a/src/binding.c b/src/binding.c index d7cd100..de9d55e 100644 --- a/src/binding.c +++ b/src/binding.c @@ -4,12 +4,14 @@ #include "list.h" #include "role.h" +#include "label.h" #include "system.h" #include "binding.h" #include "warshall.h" #include "memory.h" #include "debug.h" #include "term.h" +#include "termmap.h" static System sys; static int *graph; @@ -342,6 +344,58 @@ goal_unbind (const Binding b) } } +//! Determine whether some label set is ordered w.r.t. send/read order. +/** + * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid. + */ +int +labels_ordered (Termmap runs, Termlist labels) +{ + goal_graph_create (); + while (labels != NULL) + { + // Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and readrole + Labelinfo linfo; + int send_run, send_ev, read_run, read_ev; + + int get_index (const int run) + { + Roledef rd; + int i; + + i = 0; + rd = sys->runs[run].start; + while (rd != NULL && !isTermEqual (rd->label, labels->term)) + { + rd = rd->next; + i++; + } +#ifdef DEBUG + if (rd == NULL) + error + ("Could not locate send or read for label, after niagree holds, to test for order."); +#endif + return i; + } + + linfo = label_find (sys->labellist, labels->term); + send_run = termmapGet (runs, linfo->sendrole); + read_run = termmapGet (runs, linfo->readrole); + send_ev = get_index (send_run); + read_ev = get_index (read_run); + if (graph[graph_nodes (nodes, send_run, send_ev, read_run, read_ev)] == + 0) + { + // Not ordered; false + return 0; + } + + // Proceed + labels = labels->next; + } + return 1; +} + //! Prune invalid state w.r.t. <=C minimal requirement /** * Intuition says this can be done a lot more efficient. Luckily this is the prototype. diff --git a/src/binding.h b/src/binding.h index 87e2831..736eb65 100644 --- a/src/binding.h +++ b/src/binding.h @@ -2,6 +2,7 @@ #define BINDINGS #include "term.h" +#include "termmap.h" #include "system.h" /* @@ -41,6 +42,7 @@ void goal_add (Term term, const int run, const int ev, const int level); void goal_remove_last (); int goal_bind (const Binding b, const int run, const int ev); void goal_unbind (const Binding b); +int labels_ordered (Termmap runs, Termlist labels); int bindings_c_minimal (); diff --git a/src/claim.c b/src/claim.c index dfa3dcc..02a897b 100644 --- a/src/claim.c +++ b/src/claim.c @@ -4,6 +4,7 @@ #include "label.h" #include "error.h" #include "debug.h" +#include "binding.h" #define MATCH_NONE 0 #define MATCH_ORDER 1 @@ -475,7 +476,8 @@ check_claim_niagree (const System sys, const int i) //! Check generic agree claim for a given set of runs, arachne style -int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) +int +arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) { Termlist labels; int flag; @@ -499,48 +501,48 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs Labelinfo linfo; Roledef get_label_event (const Term role, const Term label) - { - Roledef rd, rd_res; - int i; - int run; + { + Roledef rd, rd_res; + int i; + int run; - run = termmapGet (runs, role); + run = termmapGet (runs, role); #ifdef DEBUG - if (run < 0 || run >= sys->maxruns ) - { - globalError++; - eprintf ("Run mapping %i out of bounds for role ", run); - termPrint (role); - eprintf (" and label "); - termPrint (label); - eprintf ("\n"); - eprintf ("This label has sendrole "); - termPrint (linfo->sendrole); - eprintf (" and readrole "); - termPrint (linfo->readrole); - eprintf ("\n"); - globalError--; - error ("Run mapping is out of bounds."); - } + if (run < 0 || run >= sys->maxruns) + { + globalError++; + eprintf ("Run mapping %i out of bounds for role ", run); + termPrint (role); + eprintf (" and label "); + termPrint (label); + eprintf ("\n"); + eprintf ("This label has sendrole "); + termPrint (linfo->sendrole); + eprintf (" and readrole "); + termPrint (linfo->readrole); + eprintf ("\n"); + globalError--; + error ("Run mapping is out of bounds."); + } #endif - rd = sys->runs[run].start; - rd_res = NULL; - i = 0; - while (i < sys->runs[run].step && rd != NULL) - { - if (isTermEqual (rd->label, label)) - { - rd_res = rd; - rd = NULL; - } - else - { - rd = rd->next; - } - i++; - } - return rd_res; - } + rd = sys->runs[run].start; + rd_res = NULL; + i = 0; + while (i < sys->runs[run].step && rd != NULL) + { + if (isTermEqual (rd->label, label)) + { + rd_res = rd; + rd = NULL; + } + else + { + rd = rd->next; + } + i++; + } + return rd_res; + } // Main linfo = label_find (sys->labellist, labels->term); @@ -567,12 +569,14 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs return flag; } -//! Check arachne agreement claim +//! Check arachne authentications claim /** * Per default, occurs in run 0, but for generality we have left the run parameter in. *@returns 1 if the claim is true, 0 if it is not. */ -int arachne_claim_niagree (const System sys, const int claim_run, const int claim_index) +int +arachne_claim_authentications (const System sys, const int claim_run, + const int claim_index, const int require_order) { Claimlist cl; Roledef rd; @@ -580,38 +584,57 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai int flag; int fill_roles (Termlist roles_tofill) - { - if (roles_tofill == NULL) - { - // All roles have been chosen - return arachne_runs_agree (sys, cl, runs_involved); - } - else - { - // Choose a run for this role, if possible - // Note that any will do - int run, flag; + { + if (roles_tofill == NULL) + { + // All roles have been chosen + if (arachne_runs_agree (sys, cl, runs_involved)) + { + // niagree holds + if (!require_order) + { + return 1; + } + else + { + // Stronger claim: nisynch. Test for ordering as well. + return labels_ordered (runs_involved, cl->prec); + } + } + else + { + // niagree does not hold + return 0; + } + } + else + { + // Choose a run for this role, if possible + // Note that any will do + int run, flag; - run = 0; - flag = 0; - while (run < sys->maxruns) - { - // Has to be from the right protocol - if (sys->runs[run].protocol == cl->protocol) - { - // Has to be the right name - if (isTermEqual (sys->runs[run].role->nameterm, roles_tofill->term)) - { - // Choose, iterate - runs_involved = termmapSet (runs_involved, roles_tofill->term, run); - flag = flag || fill_roles (roles_tofill->next); - } - } - run++; - } - return flag; - } - } + run = 0; + flag = 0; + while (run < sys->maxruns) + { + // Has to be from the right protocol + if (sys->runs[run].protocol == cl->protocol) + { + // Has to be the right name + if (isTermEqual + (sys->runs[run].role->nameterm, roles_tofill->term)) + { + // Choose, iterate + runs_involved = + termmapSet (runs_involved, roles_tofill->term, run); + flag = flag || fill_roles (roles_tofill->next); + } + } + run++; + } + return flag; + } + } #ifdef DEBUG if (DEBUGL (5)) @@ -623,7 +646,7 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai rd = roledef_shift (sys->runs[claim_run].start, claim_index); #ifdef DEBUG if (rd == NULL) - error ("Retrieving claim info for NULL node??"); + error ("Retrieving claim info for NULL node??"); #endif cl = rd->claiminfo; @@ -634,9 +657,18 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai return flag; } -//! Test nisynch -int arachne_claim_nisynch (const System sys, const int claim_run, const int claim_index) +//! Test niagree +int +arachne_claim_niagree (const System sys, const int claim_run, + const int claim_index) { - //!@todo For now, only agreement claim - return arachne_claim_niagree (sys, claim_run, claim_index); + return arachne_claim_authentications (sys, claim_run, claim_index, 0); +} + +//! Test nisynch +int +arachne_claim_nisynch (const System sys, const int claim_run, + const int claim_index) +{ + return arachne_claim_authentications (sys, claim_run, claim_index, 1); }