diff --git a/src/compiler.c b/src/compiler.c index 9832cdb..1493586 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -3,6 +3,7 @@ #include "tac.h" #include "term.h" #include "termlist.h" +#include "label.h" #include "memory.h" #include "system.h" #include "knowledge.h" @@ -20,19 +21,6 @@ static System sys; static Tac tac_root; -/* - * Structure to store label information - */ -struct labelinfo -{ - Term label; - Term protocol; - Term sendrole; - Term readrole; -}; - -typedef struct labelinfo Labelinfo; - /* * Declaration from system.c */ @@ -391,6 +379,7 @@ commEvent (int event, Tac tc) Term claimbig = NULL; int n = 0; Tac trip; + Labelinfo linfo; /* Construct label, if any */ if (tc->t1.sym == NULL) @@ -417,6 +406,20 @@ commEvent (int event, Tac tc) makeTermTuple (thisProtocol->nameterm, label); } } + /** + * We now know the label. Find the corresponding labelinfo bit or make a new one + */ + linfo = label_find (sys->labellist, label); + if (linfo == NULL) + { + /* Not found, make a new one */ + linfo = label_create (label, thisProtocol); + sys->labellist = list_append (sys->labellist, linfo); + } + + /** + * Parse the specific event type + */ trip = tc->t2.tac; switch (event) { @@ -434,11 +437,24 @@ commEvent (int event, Tac tc) if (event == SEND) { + /* set sendrole */ + if (linfo->sendrole != NULL) + error ("Label defined twice for sendrole!"); + linfo->sendrole = fromrole; + /* set keylevels based on send events */ term_set_keylevels (fromrole); term_set_keylevels (torole); term_set_keylevels (msg); } + else + { + // READ + /* set readrole */ + if (linfo->readrole != NULL) + error ("Label defined twice for readrole!"); + linfo->readrole = torole; + } break; case CLAIM: @@ -518,6 +534,7 @@ commEvent (int event, Tac tc) cl->complete = 0; cl->failed = 0; cl->prec = NULL; + cl->roles = NULL; cl->next = sys->claimlist; sys->claimlist = cl; @@ -905,6 +922,30 @@ compute_role_variables (const System sys, Protocol p, Role r) } } +//! Compute term list of rolenames involved in a given term list of labels +Termlist +compute_label_roles (Termlist labels) +{ + Termlist roles; + + roles = NULL; + while (labels != NULL) + { + Labelinfo linfo; + + linfo = label_find (sys->labellist, labels->term); +#ifdef DEBUG + if (linfo == NULL) + error ("Label in prec list not found in label info list"); +#endif + roles = termlistAddNew (roles, linfo->sendrole); + roles = termlistAddNew (roles, linfo->readrole); + + labels = labels->next; + } + return roles; +} + //! Compute prec() sets for each claim. /** * Generates two auxiliary structures. First, a table that contains @@ -1180,6 +1221,12 @@ compute_prec_sets (const System sys) } r2++; } + /** + * cl->prec is done, now we infer cl->roles + */ + + cl->roles = compute_label_roles (cl->prec); + /** * --------------------------- * Distinguish types of claims @@ -1268,9 +1315,21 @@ compute_prec_sets (const System sys) } else { - // printf ("Preceding label set for r:%i, ev:%i = ", r1,ev1); - // termlistPrint (cl->prec); - // printf ("\n"); +#ifdef DEBUG + if (DEBUGL (3)) + { + Protocol p; + + printf ("Preceding label set for r:%i, ev:%i = ", r1,ev1); + termlistPrint (cl->prec); + printf (", involving roles "); + termlistPrint (cl->roles); + printf (", from protocol "); + p = (Protocol) cl->protocol; + termPrint (p->nameterm); + printf ("\n"); + } +#endif } // Proceed to next claim diff --git a/src/label.c b/src/label.c index 8e4b3f6..9aa228b 100644 --- a/src/label.c +++ b/src/label.c @@ -5,8 +5,11 @@ #include "memory.h" #include "term.h" #include "label.h" +#include "list.h" +#include "system.h" -Labelinfo label_create (const Term label, const Term protocol) +//! Create a new labelinfo node +Labelinfo label_create (const Term label, const Protocol protocol) { Labelinfo li; @@ -18,8 +21,35 @@ Labelinfo label_create (const Term label, const Term protocol) return li; } +//! Destroy a labelinfo node void label_destroy (Labelinfo linfo) { memFree (linfo, sizeof (struct labelinfo)); } +//! Given a list of label infos, yield the correct one or NULL +Labelinfo label_find (List labellist, const Term label) +{ + Labelinfo linfo; + + int scan (void *data) + { + Labelinfo linfo_scan; + + linfo_scan = (Labelinfo) data; + if (isTermEqual (label, linfo_scan->label)) + { + linfo = linfo_scan; + return 0; + } + else + { + return 1; + } + } + + linfo = NULL; + list_iterate (labellist, scan); + return linfo; +} + diff --git a/src/label.h b/src/label.h index 71ed060..2f6b1fa 100644 --- a/src/label.h +++ b/src/label.h @@ -2,6 +2,8 @@ #define LABEL #include "term.h" +#include "list.h" +#include "system.h" /* * Structure to store label information @@ -16,7 +18,8 @@ struct labelinfo typedef struct labelinfo* Labelinfo; -Labelinfo label_create (const Term label, const Term protocol); +Labelinfo label_create (const Term label, const Protocol protocol); void label_destroy (Labelinfo linfo); +Labelinfo label_find (List labellist, const Term label); #endif diff --git a/src/role.h b/src/role.h index bee51d8..777e14d 100644 --- a/src/role.h +++ b/src/role.h @@ -37,6 +37,8 @@ struct claimlist int ev; //!< event index in role //! Preceding label list Termlist prec; + //! Roles that are involved (nameterms) + Termlist roles; //! Next node pointer or NULL for the last element of the function. struct claimlist *next; }; diff --git a/src/termlist.c b/src/termlist.c index 7aa04d9..b674478 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -222,7 +222,7 @@ termlistAppend (const Termlist tl, const Term term) Termlist termlistAddNew (const Termlist tl, const Term t) { - if (inTermlist (tl, t)) + if (t == NULL || inTermlist (tl, t)) return tl; else return termlistAdd (tl, t);