diff --git a/src/arachne.c b/src/arachne.c index 49e08ec..4fd0905 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -137,13 +137,13 @@ arachneInit (const System mysys) add_event (SEND, NULL); I_M = add_role ("I_M: Atomic message"); - add_event (READ, NULL); - add_event (READ, NULL); + add_event (RECV, NULL); + add_event (RECV, NULL); add_event (SEND, NULL); I_RRS = add_role ("I_E: Encrypt"); - add_event (READ, NULL); - add_event (READ, NULL); + add_event (RECV, NULL); + add_event (RECV, NULL); add_event (SEND, NULL); I_RRSD = add_role ("I_D: Decrypt"); @@ -171,8 +171,8 @@ arachneDone () //! Just a defined integer for invalid #define INVALID -1 -//! can this roledef constitute a read Goal? -#define isGoal(rd) (rd->type == READ && !rd->internal) +//! can this roledef constitute a recv Goal? +#define isGoal(rd) (rd->type == RECV && !rd->internal) //! is this roledef already bound? #define isBound(rd) (rd->bound) @@ -401,7 +401,7 @@ fixAgentKeylevels (void) *@returns The number of goals added (for destructions) */ int -add_read_goals (const int run, const int old, const int new) +add_recv_goals (const int run, const int old, const int new) { if (new <= sys->runs[run].height) { @@ -419,7 +419,7 @@ add_read_goals (const int run, const int old, const int new) count = 0; while (i < new && rd != NULL) { - if (rd->type == READ) + if (rd->type == RECV) { if (switches.output == PROOF) { @@ -661,7 +661,7 @@ iterate_role_sends (int (*func) ()) //! Create decryption role instance /** - * Note that this does not add any bindings for the reads. + * Note that this does not add any bindings for the receives. * *@param term The term to be decrypted (implies decryption key) *@param key The key that is needed to decrypt the term @@ -902,9 +902,9 @@ bind_existing_to_goal (const Binding b, const int run, const int index, return true; } // We need some adapting because the height would increase; we therefore - // have to add read goals before we know whether it unifies. + // have to add recv goals before we know whether it unifies. old_length = sys->runs[run].height; - newgoals = add_read_goals (run, old_length, index + 1); + newgoals = add_recv_goals (run, old_length, index + 1); { // wrap substitution lists @@ -955,7 +955,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index, int r2, e2; r2 = TermRunid (tvar); - e2 = firstOccurrence (sys, r2, tsubst, READ); + e2 = firstOccurrence (sys, r2, tsubst, RECV); if (e2 >= 0) { @@ -1074,7 +1074,7 @@ bind_new_run (const Binding b, const Protocol p, const Role r, { int newgoals; - newgoals = add_read_goals (run, 0, index + 1); + newgoals = add_recv_goals (run, 0, index + 1); indentDepth++; bind_existing_to_goal (b, run, index, true); indentDepth--; @@ -1248,7 +1248,7 @@ bind_goal_new_encrypt (const Binding b) { int newgoals; - newgoals = add_read_goals (run, 0, index + 1); + newgoals = add_recv_goals (run, 0, index + 1); { indentDepth++; @@ -2283,7 +2283,7 @@ arachneClaimTest (Claimlist cl) } proof_suppose_run (run, 0, cl->ev + 1); - newgoals = add_read_goals (run, 0, cl->ev + 1); + newgoals = add_recv_goals (run, 0, cl->ev + 1); /** * Add initial knowledge node @@ -2499,7 +2499,7 @@ arachne () * completely ignores any information on unbound variables, and regards them * as bound constants. * - * Because everything is supposed to be bound, we conclude that even 'read' + * Because everything is supposed to be bound, we conclude that even 'recv' * events imply a certain knowledge. * * If aftercomplete is 0 or false, we actually check the ordering; otherwise we @@ -2536,10 +2536,10 @@ knowledgeAtArachne (const System sys, const int myrun, const int myindex, // Check whether this event precedes myevent if (aftercomplete || isDependEvent (run, index, myrun, myindex)) { - // If it is a send (trivial) or a read (remarkable, but true + // If it is a send (trivial) or a recv (remarkable, but true // because of bindings) we can add the message and the agents to // the knowledge. - if (rd->type == SEND || rd->type == READ) + if (rd->type == SEND || rd->type == RECV) { knowledgeAddTerm (know, rd->message); if (rd->from != NULL) diff --git a/src/binding.c b/src/binding.c index 6bc8c12..277fa42 100644 --- a/src/binding.c +++ b/src/binding.c @@ -295,7 +295,7 @@ goal_remove_last (int n) } } -//! Determine whether some label set is ordered w.r.t. send/read order. +//! Determine whether some label set is ordered w.r.t. send/recv order. /** * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid. */ @@ -304,9 +304,9 @@ labels_ordered (Termmap runs, Termlist labels) { 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 + // Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and recvrole Labelinfo linfo; - int send_run, send_ev, read_run, read_ev; + int send_run, send_ev, recv_run, recv_ev; int get_index (const int run) { @@ -323,7 +323,7 @@ labels_ordered (Termmap runs, Termlist labels) #ifdef DEBUG if (rd == NULL) error - ("Could not locate send or read for label, after niagree holds, to test for order."); + ("Could not locate send or recv for label, after niagree holds, to test for order."); #endif return i; } @@ -332,10 +332,10 @@ labels_ordered (Termmap runs, Termlist labels) if (!linfo->ignore) { send_run = termmapGet (runs, linfo->sendrole); - read_run = termmapGet (runs, linfo->readrole); + recv_run = termmapGet (runs, linfo->recvrole); send_ev = get_index (send_run); - read_ev = get_index (read_run); - if (!isDependEvent (send_run, send_ev, read_run, read_ev)) + recv_ev = get_index (recv_run); + if (!isDependEvent (send_run, send_ev, recv_run, recv_ev)) { // Not ordered; false return false; @@ -550,7 +550,7 @@ bindings_c_minimal () //!@todo hardcoded reference to step, should be length for (ev = 0; ev < sys->runs[run].step; ev++) { - if (rd->type == SEND || rd->type == READ) + if (rd->type == SEND || rd->type == RECV) { if (isDependEvent (run, ev, b->run_from, b->ev_from)) { diff --git a/src/claim.c b/src/claim.c index f3a82b6..1a501af 100644 --- a/src/claim.c +++ b/src/claim.c @@ -129,14 +129,14 @@ events_match (const System sys, const int i, const int j) isTermEqual (rdi->label, rdj->label) && !(rdi->internal || rdj->internal)) { - if (rdi->type == SEND && rdj->type == READ) + if (rdi->type == SEND && rdj->type == RECV) { if (i < j) return MATCH_ORDER; else return MATCH_REVERSE; } - if (rdi->type == READ && rdj->type == SEND) + if (rdi->type == RECV && rdj->type == SEND) { if (i > j) return MATCH_ORDER; @@ -175,7 +175,7 @@ oki_nisynch_full (const System sys, const Termmap label_to_index) return 1; } -//! Evaluate claims or internal reads (chooses) +//! Evaluate claims or internal recvs (chooses) __inline__ int oki_nisynch_other (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index) @@ -196,13 +196,13 @@ oki_nisynch_other (const System sys, const int trace_index, return result; } -//! Evaluate reads +//! Evaluate recvs __inline__ int -oki_nisynch_read (const System sys, const int trace_index, +oki_nisynch_recv (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index) { /* - * Read is only relevant for already involved runs, and labels in prec + * Recv is only relevant for already involved runs, and labels in prec */ Termmap role_to_run_scan; int result = 7; @@ -228,7 +228,7 @@ oki_nisynch_read (const System sys, const int trace_index, termmapSet (label_to_index_buf, rd->label, trace_index); #ifdef OKIDEBUG indact (); - eprintf ("Exploring because this (read) run is involved.\n"); + eprintf ("Exploring because this (recv) run is involved.\n"); indac++; #endif result = @@ -248,7 +248,7 @@ oki_nisynch_read (const System sys, const int trace_index, // Apparently not involved #ifdef OKIDEBUG indact (); - eprintf ("Exploring further assuming this (read) run is not involved.\n"); + eprintf ("Exploring further assuming this (recv) run is not involved.\n"); indac++; #endif result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index); @@ -305,10 +305,10 @@ oki_nisynch_send (const System sys, const int trace_index, // Was not involved yet in a registerd way, or was the correct rid partner_index = termmapGet (label_to_index, rd->label); // Ordered match needed for this label - // So it already needs to be filled by a read + // So it already needs to be filled by a recv if (partner_index >= 0) { - // There is already a read for it + // There is already a recv for it if (events_match (sys, partner_index, trace_index) == MATCH_ORDER) { // They match in the right order @@ -385,12 +385,12 @@ oki_nisynch (const System sys, const int trace_index, if (type == CLAIM || sys->traceEvent[trace_index]->internal) return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index); - if (type == READ) - return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index); + if (type == RECV) + return oki_nisynch_recv (sys, trace_index, role_to_run, label_to_index); if (type == SEND) return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index); /* - * Exception: no claim, no send, no read, what is it? + * Exception: no claim, no send, no recv, what is it? */ error ("Unrecognized event type in claim scanner at %i.", trace_index); return 0; @@ -540,8 +540,8 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) while (flag && labels != NULL) { // For each label, check whether it matches. Maybe a bit too strict (what about variables?) - // Locate roledefs for read & send, and check whether they are before step - Roledef rd_send, rd_read; + // Locate roledefs for recv & send, and check whether they are before step + Roledef rd_send, rd_recv; Labelinfo linfo; Roledef get_label_event (const Term role, const Term label) @@ -564,8 +564,8 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) eprintf ("\n"); eprintf ("This label has sendrole "); termPrint (linfo->sendrole); - eprintf (" and readrole "); - termPrint (linfo->readrole); + eprintf (" and recvrole "); + termPrint (linfo->recvrole); eprintf ("\n"); globalError--; error ("Run mapping is out of bounds."); @@ -600,9 +600,9 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) if (!linfo->ignore) { rd_send = get_label_event (linfo->sendrole, labels->term); - rd_read = get_label_event (linfo->readrole, labels->term); + rd_recv = get_label_event (linfo->recvrole, labels->term); - if (rd_send == NULL || rd_read == NULL) + if (rd_send == NULL || rd_recv == NULL) { // False! flag = 0; @@ -610,7 +610,7 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs) else { // Compare - if (events_match_rd (rd_send, rd_read) != MATCH_CONTENT) + if (events_match_rd (rd_send, rd_recv) != MATCH_CONTENT) { // False! flag = 0; diff --git a/src/compiler.c b/src/compiler.c index fa4322a..d3ffb31 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -119,15 +119,15 @@ compilerDone (void) return; } -//! Compute read variables for a role +//! Compute recv variables for a role Termlist -compute_read_variables (const Role r) +compute_recv_variables (const Role r) { Termlist tl; int process_event (Roledef rd) { - if (rd->type == READ) + if (rd->type == RECV) { tl = termlistAddVariables (tl, rd->from); tl = termlistAddVariables (tl, rd->to); @@ -549,20 +549,20 @@ claimCreate (const System sys, const Protocol protocol, const Role role, if (claim == CLAIM_Secret) { Termlist claimvars; - Termlist readvars; + Termlist recvvars; /* now check whether the claim contains variables that can actually be influenced by the intruder */ claimvars = termlistAddVariables (NULL, msg); - readvars = compute_read_variables (thisRole); + recvvars = compute_recv_variables (thisRole); while (claimvars != NULL) { if (!inTermlist (protocol->rolenames, claimvars->term)) { /* only if it is not a role */ - if (!inTermlist (readvars, claimvars->term)) + if (!inTermlist (recvvars, claimvars->term)) { - /* this claimvar does not occur in the reads? */ + /* this claimvar does not occur in the recvs? */ /* then we should ignore it later */ cl->alwaystrue = true; cl->warnings = true; @@ -574,14 +574,14 @@ claimCreate (const System sys, const Protocol protocol, const Role role, eprintf (" contains a variable "); termPrint (claimvars->term); eprintf - (" which is never read; therefore the claim will be true.\n"); + (" which is never recv; therefore the claim will be true.\n"); globalError--; } } claimvars = claimvars->next; } termlistDelete (claimvars); - termlistDelete (readvars); + termlistDelete (recvvars); } return cl; } @@ -590,7 +590,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role, void commEvent (int event, Tac tc) { - /* Add an event to the roledef, send or read */ + /* Add an event to the roledef, send or recv */ Claimlist cl; Term fromrole = NULL; Term torole = NULL; @@ -606,8 +606,8 @@ commEvent (int event, Tac tc) if (tc->t1.sym == NULL) { /* right, now this should not be NULL anyway, if so we construct a fresh one. - * This can be a weird choice if it is a read or send, because in that case - * we cannot chain them anymore and the send-read correspondence is lost. + * This can be a weird choice if it is a recv or send, because in that case + * we cannot chain them anymore and the send-recv correspondence is lost. */ int n; Roledef rd; @@ -646,7 +646,7 @@ commEvent (int event, Tac tc) trip = tc->t2.tac; switch (event) { - case READ: + case RECV: case SEND: /** * We know the label. Find the corresponding labelinfo bit or make a new one @@ -687,18 +687,18 @@ commEvent (int event, Tac tc) } else { - // READ - /* set readrole */ + // RECV + /* set recvrole */ if (!isTermEqual (torole, thisRole->nameterm)) error - ("Read role does not correspond to execution role at line %i.", + ("Recv role does not correspond to execution role at line %i.", tc->lineno); - if (linfo->readrole != NULL) - error ("Label defined twice for readrole!"); - linfo->readrole = torole; + if (linfo->recvrole != NULL) + error ("Label defined twice for recvrole!"); + linfo->recvrole = torole; } - /* and make that read/send event */ + /* and make that recv/send event */ thisRole->roledef = roledefAdd (thisRole->roledef, event, label, fromrole, torole, msg, cl); /* mark last one with line number */ @@ -990,18 +990,18 @@ roleCompile (Term nameterm, Tac tc) { switch (tc->op) { - case TAC_READ: + case TAC_RECV: if (firstEvent) { - // First a read, thus responder + // First a recv, thus responder /* - * Semantics: defaults (in role.c) to initiator _unless_ the first event is a read, + * Semantics: defaults (in role.c) to initiator _unless_ the first event is a recv, * in which case we assume that the agent names are possibly received as variables */ thisRole->initiator = 0; firstEvent = 0; } - commEvent (READ, tc); + commEvent (RECV, tc); break; case TAC_SEND: firstEvent = 0; @@ -1412,7 +1412,7 @@ compute_label_roles (Termlist labels) error ("Label in prec list not found in label info list"); #endif roles = termlistAddNew (roles, linfo->sendrole); - roles = termlistAddNew (roles, linfo->readrole); + roles = termlistAddNew (roles, linfo->recvrole); labels = labels->next; } @@ -1479,8 +1479,8 @@ order_label_roles (const Claimlist cl) } } - roles_test (linfo->sendrole, linfo->readrole); - roles_test (linfo->readrole, linfo->sendrole); + roles_test (linfo->sendrole, linfo->recvrole); + roles_test (linfo->recvrole, linfo->sendrole); } } return 1; @@ -1673,7 +1673,7 @@ compute_prec_sets (const System sys) Roledef rd2; rd2 = roledef_re (r2, ev2); - if (rd2 != NULL && rd2->type == READ + if (rd2 != NULL && rd2->type == RECV && isTermEqual (rd1->label, rd2->label)) { SETBIT (prec + rowsize * index (r1, ev1), @@ -1769,9 +1769,9 @@ compute_prec_sets (const System sys) { // This event precedes the claim - if (rd->type == READ) + if (rd->type == RECV) { - // Only store read labels (but send would work as well) + // Only store recv labels (but send would work as well) cl->prec = termlistAdd (cl->prec, rd->label); } } @@ -1941,7 +1941,7 @@ checkRoleVariables (const System sys, const Protocol p, const Role r) int process_event (Roledef rd) { - if (rd->type == READ) + if (rd->type == RECV) { vars = termlistAddVariables (vars, rd->from); vars = termlistAddVariables (vars, rd->to); @@ -1950,11 +1950,11 @@ checkRoleVariables (const System sys, const Protocol p, const Role r) return 1; } - /* Gather all variables occurring in the reads */ + /* Gather all variables occurring in the recvs */ vars = NULL; roledef_iterate_events (r->roledef, process_event); - /* Now, all variables for this role should be in the reads */ + /* Now, all variables for this role should be in the recvs */ declared = r->declaredvars; while (declared != NULL) { @@ -1970,7 +1970,7 @@ checkRoleVariables (const System sys, const Protocol p, const Role r) termPrint (p->nameterm); eprintf (","); termPrint (r->nameterm); - eprintf (" but never used in a read event.\n"); + eprintf (" but never used in a recv event.\n"); globalError--; } } @@ -2081,13 +2081,13 @@ checkEventMatch (const Roledef rd1, const Roledef rd2, return true; } -//! Check label matchup for protocol p,r, roledef rd (which is a read) +//! Check label matchup for protocol p,r, roledef rd (which is a recv) /** * Any send with the same label should match */ void -checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, - const Roledef readevent) +checkLabelMatchThis (const System sys, const Protocol p, const Role recvrole, + const Roledef recvevent) { Role sendrole; int found; @@ -2103,13 +2103,13 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, { if (event->type == SEND) { - if (isTermEqual (event->label, readevent->label)) + if (isTermEqual (event->label, recvevent->label)) { // Same labels, so they should match up! - if (!checkEventMatch (event, readevent, p->rolenames)) + if (!checkEventMatch (event, recvevent, p->rolenames)) { globalError++; - eprintf ("error: [%i]", readevent->lineno); + eprintf ("error: [%i]", recvevent->lineno); if (sys->protocols != NULL) { if (sys->protocols->next != NULL) @@ -2124,8 +2124,8 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, eprintf ("error: [%i] ", event->lineno); roledefPrint (event); eprintf (" does not match\n"); - eprintf ("error: [%i] ", readevent->lineno); - roledefPrint (readevent); + eprintf ("error: [%i] ", recvevent->lineno); + roledefPrint (recvevent); eprintf ("\n"); error_die (); globalError--; @@ -2141,7 +2141,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, eprintf (" to match: "); roledefPrint (event); eprintf (" <> "); - roledefPrint (readevent); + roledefPrint (recvevent); eprintf ("\n"); } #endif @@ -2160,8 +2160,8 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, if (found == 0) { globalError++; - eprintf ("error: [%i] for the read event ", readevent->lineno); - roledefPrint (readevent); + eprintf ("error: [%i] for the recv event ", recvevent->lineno); + roledefPrint (recvevent); eprintf (" of protocol "); termPrint (p->nameterm); eprintf @@ -2175,7 +2175,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, void checkLabelMatchProtocol (const System sys, const Protocol p) { - // For each read label the sends should match + // For each recv label the sends should match Role r; r = p->roles; @@ -2186,7 +2186,7 @@ checkLabelMatchProtocol (const System sys, const Protocol p) rd = r->roledef; while (rd != NULL) { - if (rd->type == READ) + if (rd->type == RECV) { // We don't check all, if they start with a bang we ignore them. Labelinfo li; diff --git a/src/dotout.c b/src/dotout.c index 3f0fd33..4e7b680 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -36,7 +36,7 @@ extern Role I_RRS; extern Role I_RRSD; #define INVALID -1 -#define isGoal(rd) (rd->type == READ && !rd->internal) +#define isGoal(rd) (rd->type == RECV && !rd->internal) #define isBound(rd) (rd->bound) #define length step @@ -283,7 +283,7 @@ roledefDraw (Roledef rd) } } - if (rd->type == READ) + if (rd->type == RECV) { eprintf ("recv"); optlabel (); @@ -1244,7 +1244,7 @@ showLocal (const int run, Term told, Term tnew, char *prefix, char *cursep) { if (termOccursInRun (tnew, run)) { - // Variables are mapped, maybe. But then we wonder whether they occur in reads. + // Variables are mapped, maybe. But then we wonder whether they occur in recvs. eprintf (cursep); eprintf (prefix); termPrintRemap (told); diff --git a/src/label.c b/src/label.c index 7573977..836caf7 100644 --- a/src/label.c +++ b/src/label.c @@ -53,7 +53,7 @@ label_create (const Term label, const Protocol protocol) li->label = label; li->protocol = protocol; li->sendrole = NULL; - li->readrole = NULL; + li->recvrole = NULL; // Should we ignore it? li->ignore = false; tl = rightMostTerm (label); diff --git a/src/label.h b/src/label.h index e4e89e2..6efbbc5 100644 --- a/src/label.h +++ b/src/label.h @@ -33,7 +33,7 @@ struct labelinfo int ignore; Protocol protocol; Term sendrole; - Term readrole; + Term recvrole; }; typedef struct labelinfo *Labelinfo; diff --git a/src/parser.y b/src/parser.y index cac0466..78868e2 100644 --- a/src/parser.y +++ b/src/parser.y @@ -176,14 +176,14 @@ roledef : /* empty */ * but that will take a while I guess. */ event : READT label '(' termlist ')' ';' - { Tac t = tacCreate(TAC_READ); + { Tac t = tacCreate(TAC_RECV); t->t1.sym = $2; /* TODO test here: tac2 should have at least 3 elements */ t->t2.tac = $4; $$ = t; } | RECVT label '(' termlist ')' ';' - { Tac t = tacCreate(TAC_READ); + { Tac t = tacCreate(TAC_RECV); t->t1.sym = $2; /* TODO test here: tac2 should have at least 3 elements */ t->t2.tac = $4; diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 7f8adef..0c4edf5 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -65,7 +65,7 @@ correctLocalOrder (const System sys) e1 = firstOccurrence (sys, r1, t, ANYEVENT); if (e1 >= 0) { - if (roledef_shift (sys->runs[r1].start, e1)->type == READ) + if (roledef_shift (sys->runs[r1].start, e1)->type == RECV) { e2 = firstOccurrence (sys, r2, t, SEND); if (e2 >= 0) diff --git a/src/role.c b/src/role.c index bf8fa85..1f79c96 100644 --- a/src/role.c +++ b/src/role.c @@ -54,15 +54,15 @@ roledefPrintGeneric (Roledef rd, int print_actor) eprintf ("[Empty roledef]"); return; } - if (rd->type == READ && rd->internal) + if (rd->type == RECV && rd->internal) { - /* special case: internal read == choose ! */ + /* special case: internal recv == choose ! */ eprintf ("CHOOSE("); termPrint (rd->message); eprintf (")"); return; } - if (rd->type == READ) + if (rd->type == RECV) eprintf ("RECV"); if (rd->type == SEND) eprintf ("SEND"); @@ -93,14 +93,14 @@ roledefPrintGeneric (Roledef rd, int print_actor) eprintf ("("); if (!(rd->from == NULL && rd->to == NULL)) { - if (print_actor || rd->type == READ) + if (print_actor || rd->type == RECV) { termPrint (rd->from); eprintf (","); } if (rd->type == CLAIM) eprintf (" "); - if (print_actor || rd->type != READ) + if (print_actor || rd->type != RECV) { termPrint (rd->to); eprintf (", "); @@ -205,7 +205,7 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) newEvent->forbidden = NULL; // no forbidden stuff newEvent->knowPhase = -1; // we haven't explored any knowledge yet newEvent->claiminfo = cl; // only for claims - if (type == READ) + if (type == RECV) newEvent->bound = 0; // bound goal (Used for arachne only). Technically involves choose events as well. else newEvent->bound = 1; // other stuff does not need to be bound @@ -247,7 +247,7 @@ roleCreate (Term name) r->variables = NULL; r->declaredvars = NULL; r->declaredconsts = NULL; - r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c) + r->initiator = 1; //! Will be determined later, if a recv is the first action (in compiler.c) r->singular = false; // by default, a role is not singular r->next = NULL; r->knows = NULL; @@ -470,7 +470,7 @@ WellFormedEvent (Term role, Knowledge know, Roledef rd) { return know; } - if (rd->type == READ) + if (rd->type == RECV) { // Read if (!isTermEqual (role, rd->to)) diff --git a/src/role.h b/src/role.h index febb8c5..aac01af 100644 --- a/src/role.h +++ b/src/role.h @@ -27,7 +27,7 @@ #include "states.h" enum eventtype -{ READ, SEND, CLAIM, ANYEVENT }; +{ RECV, SEND, CLAIM, ANYEVENT }; //! The container for the claim info list /** @@ -88,13 +88,13 @@ struct roledef { //! flag for internal actions. /** - * Typically, this is true to signify internal reads (e.g. variable choices) - * as opposed to a normal read. + * Typically, this is true to signify internal recvs (e.g. variable choices) + * as opposed to a normal recv. */ int internal; //! Type of event. /** - *\sa READ, SEND, CLAIM + *\sa RECV, SEND, CLAIM */ int type; //! Event label. @@ -109,7 +109,7 @@ struct roledef struct roledef *next; /* - * Substructure for reads + * Substructure for recvs */ //! Illegal injections for this event. /** diff --git a/src/switches.c b/src/switches.c index 0c6fe8b..facbdc5 100644 --- a/src/switches.c +++ b/src/switches.c @@ -104,7 +104,7 @@ switchesInit (int argc, char **argv) switches.reportMemory = 0; switches.reportTime = 0; switches.countStates = false; // default off - switches.extendNonReads = 0; // default off + switches.extendNonRecvs = 0; // default off switches.extendTrivial = 0; // default off switches.plain = false; // default colors for terminal switches.monochrome = false; // default colors for dot @@ -204,7 +204,7 @@ openFileSearch (char *filename, FILE * reopener) if (switches.expert) { globalError++; - eprintf ("Reading file %s.\n", buffer); + eprintf ("Recving file %s.\n", buffer); globalError--; } @@ -987,7 +987,7 @@ switcher (const int process, int index, int commandline) } } - if (detect (' ', "extend-nonreads", 0)) + if (detect (' ', "extend-nonrecvs", 0)) { if (!process) { @@ -996,7 +996,7 @@ switcher (const int process, int index, int commandline) } else { - switches.extendNonReads = 1; + switches.extendNonRecvs = 1; return index; } } diff --git a/src/switches.h b/src/switches.h index 4fcad04..93a73a0 100644 --- a/src/switches.h +++ b/src/switches.h @@ -80,7 +80,7 @@ struct switchdata int reportMemory; //!< Memory display switch. int reportTime; //!< Time display switch. int countStates; //!< Count states - int extendNonReads; //!< Show further events in arachne xml output. + int extendNonRecvs; //!< Show further events in arachne xml output. int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension) int plain; //!< Disable color output on terminal int monochrome; //!< Disable colors in dot output diff --git a/src/system.c b/src/system.c index 1e08d75..5a176e6 100644 --- a/src/system.c +++ b/src/system.c @@ -142,7 +142,7 @@ systemRuns (const System sys) Roledef rd; rd = runPointerGet (sys, run); - if (rd != NULL && rd->internal && rd->type == READ) + if (rd != NULL && rd->internal && rd->type == RECV) { /* increasing run traversal, so this yields max */ sys->lastChooseRun = run; @@ -243,7 +243,7 @@ ensureValidRun (const System sys, int run) sys->runs[i].prevSymmRun = -1; - sys->runs[i].firstNonAgentRead = -1; + sys->runs[i].firstNonAgentRecv = -1; sys->runs[i].firstReal = 0; } } @@ -283,13 +283,13 @@ runsPrint (const System sys) } } -//! Determine whether a term is sent or claimed, but not read first in a roledef +//! Determine whether a term is sent or claimed, but not recv first in a roledef /** * @returns True iff the term occurs, and is sent/claimed first. If this returns true, - * we have to prefix a read. + * we have to prefix a recv. */ int -not_read_first (const Roledef rdstart, const Term t) +not_recv_first (const Roledef rdstart, const Term t) { Roledef rd; @@ -298,12 +298,12 @@ not_read_first (const Roledef rdstart, const Term t) { if (termSubTerm (rd->message, t)) { - return (rd->type != READ); + return (rd->type != RECV); } rd = rd->next; } - /* this term is not read or sent explicitly, which is no problem */ - /* So we signal we don't have to prefix a read */ + /* this term is not recv or sent explicitly, which is no problem */ + /* So we signal we don't have to prefix a recv */ return 0; } @@ -349,12 +349,12 @@ agentOfRun (const System sys, const int run) return agentOfRunRole (sys, run, sys->runs[run].role->nameterm); } -//! Determine first read with variables besides agents +//! Determine first recv with variables besides agents /** - *@todo For now, we assume it is simply the first read after the choose, if there is one. + *@todo For now, we assume it is simply the first recv after the choose, if there is one. */ int -firstNonAgentRead (const System sys, int rid) +firstNonAgentRecv (const System sys, int rid) { int step; Roledef rd; @@ -366,21 +366,21 @@ firstNonAgentRead (const System sys, int rid) } rd = sys->runs[rid].start; step = 0; - while (rd != NULL && rd->internal && rd->type == READ) // assumes lazy LR eval + while (rd != NULL && rd->internal && rd->type == RECV) // assumes lazy LR eval { rd = rd->next; step++; } - if (rd != NULL && !rd->internal && rd->type == READ) // assumes lazy LR eval + if (rd != NULL && !rd->internal && rd->type == RECV) // assumes lazy LR eval { #ifdef DEBUG warning - ("First read %i with dependency on symmetrical found in run %i.", + ("First recv %i with dependency on symmetrical found in run %i.", step, rid); #endif return step; } - /* no such read */ + /* no such recv */ return -1; } @@ -391,7 +391,7 @@ firstNonAgentRead (const System sys, int rid) * *************************************************/ -//! Prefix a read before a given run. +//! Prefix a recv before a given run. /** * Maybe this simply needs integration in the role definitions. However, in practice it * depends on the specific scenario. For Arachne it can thus depend on the roledef. @@ -399,15 +399,15 @@ firstNonAgentRead (const System sys, int rid) * Stores the (new) rd pointer in start and index */ void -run_prefix_read (const System sys, const int run, Roledef rd, +run_prefix_recv (const System sys, const int run, Roledef rd, const Term extterm) { - /* prefix a read for such reads. TODO: this should also cover any external stuff */ + /* prefix a recv for such recvs. TODO: this should also cover any external stuff */ if (extterm != NULL) { Roledef rdnew; - rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL); + rdnew = roledefInit (RECV, NULL, NULL, NULL, extterm, NULL); /* this is an internal action! */ rdnew->internal = 1; /* Store this new pointer */ @@ -524,12 +524,12 @@ roleInstanceArachne (const System sys, const Protocol protocol, TERMLISTAPPEND (runs[rid].rho, newt); if (!role->initiator) { - // For non-initiators, we prepend the reading of the role names + // For non-initiators, we prepend the recving of the role names // XXX disabled for now TODO [x] [cc] - if (0 == 1 && not_read_first (rd, oldt)) + if (0 == 1 && not_recv_first (rd, oldt)) { - /* this term is forced as a choose, or it does not occur in the (first) read event */ + /* this term is forced as a choose, or it does not occur in the (first) recv event */ if (extterm == NULL) { extterm = newt; @@ -594,11 +594,11 @@ roleInstanceArachne (const System sys, const Protocol protocol, createLocals (role->declaredvars, true, false); createLocals (role->declaredconsts, false, false); - /* Now we prefix the read before rd, if extterm is not NULL. Even if + /* Now we prefix the recv before rd, if extterm is not NULL. Even if * extterm is NULL, rd is still set as the start and the index pointer of * the run. */ - run_prefix_read (sys, rid, rd, extterm); + run_prefix_recv (sys, rid, rd, extterm); /* TODO this is not what we want yet, also local knowledge. The local * knowledge (list?) also needs to be substituted on invocation. */ @@ -1131,7 +1131,7 @@ iterateLocalToOther (const System sys, const int myrun, flag = true; tlo = NULL; - // construct all others occuring in the reads + // construct all others occuring in the recvs for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next) { Term tt; @@ -1181,7 +1181,7 @@ iterateRoles (const System sys, int (*callback) (Protocol p, Role r)) return true; } -//! Get first read/send occurrence (event index) of term t in run r +//! Get first recv/send occurrence (event index) of term t in run r int firstOccurrence (const System sys, const int r, Term t, int evtype) { diff --git a/src/system.h b/src/system.h index e846687..428fedb 100644 --- a/src/system.h +++ b/src/system.h @@ -74,7 +74,7 @@ struct run Termlist substitutions; //!< The substitutions as they came from the roledef unifier int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter. - int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. + int firstNonAgentRecv; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. int firstReal; //!< 1 if a choose was inserted, otherwise 0 }; diff --git a/src/tac.c b/src/tac.c index 9752de1..a585ce2 100644 --- a/src/tac.c +++ b/src/tac.c @@ -222,8 +222,8 @@ tacPrint (Tac t) tacPrint (t->t2.tac); printf ("};\n"); break; - case TAC_READ: - printf ("read"); + case TAC_RECV: + printf ("recv"); if (t->t1.sym != NULL) { printf ("_%s", t->t1.sym->text); diff --git a/src/tac.h b/src/tac.h index e2947bf..f816b78 100644 --- a/src/tac.h +++ b/src/tac.h @@ -35,7 +35,7 @@ enum tactypes TAC_VAR, TAC_CONST, TAC_FRESH, - TAC_READ, + TAC_RECV, TAC_SEND, TAC_CLAIM, TAC_FUNC, diff --git a/src/xmlout.c b/src/xmlout.c index d3ec4ef..83ab337 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -525,7 +525,7 @@ isEventInteresting (const System sys, const Roledef rd) /** * run and index will only be output if they are nonnegative. * Also prints any bindings, if this events follows some other events - * (typically when this is a read). + * (typically when this is a recv). * * If run < 0, it is assumed to be a role event, and thus no bindings will be shown. */ @@ -542,10 +542,10 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index) eprintf ("type) { - /* Read or send types are fairly similar. + /* Recv or send types are fairly similar. * Currently, choose events are not distinguished yet. TODO */ - case READ: + case RECV: eprintf ("recv"); break; case SEND: @@ -566,7 +566,7 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index) xmlOutTerm ("label", rd->label); if (rd->type != CLAIM) { - /* read or send */ + /* recv or send */ xmlOutTerm ("from", rd->from); xmlOutTerm ("to", rd->to); xmlOutTerm ("message", rd->message); @@ -844,9 +844,9 @@ xmlOutRuns (const System sys) } else { - if (switches.extendTrivial || switches.extendNonReads) + if (switches.extendTrivial || switches.extendNonRecvs) { - if (rd->type != READ) + if (rd->type != RECV) { return true; } @@ -854,7 +854,7 @@ xmlOutRuns (const System sys) { if (switches.extendTrivial) { - /* This is a read, and we don't know whether to + /* This is a recv, and we don't know whether to * include it. Default behaviour would be to jump * out of the conditions, and return false. * Instead, we check whether it can be trivially @@ -929,7 +929,7 @@ xmlOutSemitrace (const System sys) eprintf ("