diff --git a/src/arachne.c b/src/arachne.c index b931846..c81e339 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -574,6 +574,71 @@ countIntruderActions () return count; } +//! Check this variables whether it is a good agent type +/** + * Checks for leaf/etc and correct agent type + */ +int +goodAgentType (Term agent) +{ + agent = deVar (agent); + + if (!realTermLeaf (agent)) + { // not a leaf + return false; + } + else + { // real leaf + if (isTermVariable (agent)) + { + // Variable: check type consistency (should have a solution) + // Not yet: depends on matching mode also + } + else + { + // Constant: allow only exact type + if (!inTermlist (agent->stype, TERM_Agent)) + { + return false; + } + } + } + + return true; +} + +//! Check initiator roles +/** + * Returns false iff an agent type is wrong + */ +int +initiatorAgentsType () +{ + int run; + + run = 0; + while (run < sys->maxruns) + { + // Only for initiators + if (sys->runs[run].role->initiator) + { + Termlist agents; + + agents = sys->runs[run].agents; + while (agents != NULL) + { + if (!goodAgentType (agents->term)) + { + return false; + } + agents = agents->next; + } + } + run++; + } + return true; // seems to be okay +} + //------------------------------------------------------------------------ // Proof reporting //------------------------------------------------------------------------ @@ -2799,72 +2864,42 @@ prune_theorems () return 1; } - // Check if all agents are agents (!) + // Check if all actors are agents for responders (initiators come next) run = 0; while (run < sys->maxruns) { - Termlist agl; - - agl = sys->runs[run].agents; - while (agl != NULL) + if (!sys->runs[run].role->initiator) { - Term agent; + Term actor; - agent = deVar (agl->term); - if (agent == NULL) + actor = agentOfRun (sys, run); + if (!goodAgentType (actor)) { - error ("Agent of run %i is NULL", run); + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the actor "); + termPrint (actor); + eprintf (" of run %i is not of a compatible type.\n", run); + } + return 1; } - /** - * Check whether the agent of the run is of a sensible type. - * - * @TODO Note that this still needs a lemma. - */ - { - int sensibleagent; - - sensibleagent = true; - - if (!realTermLeaf (agent)) - { // not a leaf - sensibleagent = false; - } - else - { // real leaf - if (switches.match == 0 || !isTermVariable (agent)) - { // either strict matching, or not a variable, so we should check matching types - if (agent->stype == NULL) - { // Too generic - sensibleagent = false; - } - else - { // Has a type - if (!inTermlist (agent->stype, TERM_Agent)) - { // but not the right type - sensibleagent = false; - } - } - } - } - - if (!sensibleagent) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the agent "); - termPrint (agent); - eprintf (" of run %i is not of a compatible type.\n", - run); - } - return 1; - } - } - agl = agl->next; } run++; } + // Prune wrong agents type for initators + if (!initiatorAgentsType ()) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: an initiator role does not have the correct type for one of its agents.\n"); + } + return 1; + } + // Check if all agents of the main run are valid if (!isRunTrusted (sys, 0)) { diff --git a/src/compiler.c b/src/compiler.c index 7643859..43afac1 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -626,31 +626,48 @@ roleCompile (Term nameterm, Tac tc) /* parse the content of the role */ levelInit (); - while (tc != NULL) - { - switch (tc->op) - { - case TAC_READ: - commEvent (READ, tc); - break; - case TAC_SEND: - commEvent (SEND, tc); - break; - case TAC_CLAIM: - commEvent (CLAIM, tc); - break; - default: - if (!normalDeclaration (tc)) - { - printf ("ERROR: illegal command %i in role ", tc->op); - termPrint (thisRole->nameterm); - printf (" "); - errorTac (tc->lineno); - } - break; - } - tc = tc->next; - } + { + int firstEvent; + + /* initiator/responder flag not set */ + firstEvent = 1; + + while (tc != NULL) + { + switch (tc->op) + { + case TAC_READ: + if (firstEvent) + { + // First a read, thus responder + /* + * Semantics: defaults (in role.c) to initiator _unless_ the first event is a read, + * in which case we assume that the agent names are possibly received as variables + */ + thisRole->initiator = 0; + } + commEvent (READ, tc); + break; + case TAC_SEND: + commEvent (SEND, tc); + break; + case TAC_CLAIM: + commEvent (CLAIM, tc); + break; + default: + if (!normalDeclaration (tc)) + { + printf ("ERROR: illegal command %i in role ", tc->op); + termPrint (thisRole->nameterm); + printf (" "); + errorTac (tc->lineno); + } + break; + } + firstEvent = 0; + tc = tc->next; + } + } compute_role_variables (sys, thisProtocol, thisRole); levelDone (); } diff --git a/src/role.c b/src/role.c index 879e376..dc293fb 100644 --- a/src/role.c +++ b/src/role.c @@ -240,6 +240,7 @@ roleCreate (Term name) r->roledef = NULL; r->locals = NULL; r->variables = NULL; + r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c) r->next = NULL; return r; } diff --git a/src/role.h b/src/role.h index ba620c2..ecda238 100644 --- a/src/role.h +++ b/src/role.h @@ -120,6 +120,8 @@ struct role Termlist locals; //! Local variables for this role. Termlist variables; + //! Flag for initiator roles + int initiator; //! Pointer to next role definition. struct role *next; };