From 8b48aade682eec5cc75cf97e05c1dacf8a4eb753 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 31 Aug 2004 14:31:06 +0000 Subject: [PATCH] - Huge effort to make match type 2 (typeflaw generic) matching work. Problem with goals that turn into tuples, will have to be solved. --- src/arachne.c | 56 +++++++++++++++++++------------- src/binding.c | 20 +++++++++--- src/system.c | 88 +++++++++++++++++++++++++++++++++++++++------------ 3 files changed, 116 insertions(+), 48 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 473cb2c..3735806 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1022,6 +1022,7 @@ select_goal () float min_constrain; int max_level; + // Find the most constrained goal if (sys->output == PROOF) { indentPrint (); @@ -1462,6 +1463,39 @@ prune_theorems () { Termlist tl; List bl; + int run; + + // Check if all agents are agents (!) + run = 0; + while (run < sys->maxruns) + { + Termlist agl; + + agl = sys->runs[run].agents; + while (agl != NULL) + { + Term agent; + + agent = deVar(agl->term); + if (agent == NULL) + { + error ("Agent of run %i is NULL", run); + } + if (!realTermLeaf (agent) || (agent->stype != NULL && !inTermlist (agent->stype, TERM_Agent))) + { + if (sys->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++; + } // Check if all agents of the main run are valid tl = sys->runs[0].agents; @@ -1470,28 +1504,6 @@ prune_theorems () Term agent; agent = deVar (tl->term); - if (agent == NULL) - { - error ("Agent of run 0 is NULL"); - } - if (!realTermLeaf (agent)) - { - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Pruned because agent cannot be compound term.\n"); - } - return 1; - } - if (!inTermlist (agent->stype, TERM_Agent)) - { - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Pruned because agent must contain agent type.\n"); - } - return 1; - } if (!realTermVariable (agent) && inTermlist (sys->untrusted, agent)) { if (sys->output == PROOF) diff --git a/src/binding.c b/src/binding.c index 9c671bb..f8506cf 100644 --- a/src/binding.c +++ b/src/binding.c @@ -248,15 +248,25 @@ goal_graph_create () #endif done = 1; } -#ifdef DEBUG else { // It doesn't occur first in a READ, which shouldn't be happening - error - ("Term from run %i occurs in run %i before it is read?", - run2, run); + if (sys->output == PROOF) + { + eprintf ("Term "); + termPrint (t2); + eprintf (" from run %i occurs in run %i, term ", + run2, run); + termPrint (t); + eprintf (" before it is read?\n"); + } + // Thus, we create an artificial loop + if (sys->runs[0].step > 1) + { + // This forces a loop, and thus prunes + graph[graph_nodes (nodes, 0,1, 0,0)] = 1; + } } -#endif } rd = rd->next; ev++; diff --git a/src/system.c b/src/system.c index 98f6d85..d920a6a 100644 --- a/src/system.c +++ b/src/system.c @@ -326,6 +326,29 @@ runsPrint (const System sys) } } +//! Determine whether a term is sent or claimed, but not read first in a roledef +int not_read_first (const Roledef rdstart, const Term t) +{ + Roledef rd; + + rd = rdstart; + while (rd != NULL) + { + if (termSubTerm (rd->message, t)) + { + return (rd->type != READ); + } + rd = rd->next; + } + globalError++; + eprintf ("The term "); + termPrint (t); + eprintf (" is not read or sent in some roledef.\n"); + error ("Aborting."); + globalError--; + return 0; +} + //! Yield the agent name term in a role, for a run in the system. /** *@param sys The system. @@ -550,16 +573,18 @@ roleInstance (const System sys, const Protocol protocol, const Role role, /* newvar is apparently new, but it might occur * in the first event if it's a read, in which * case we forget it */ - if (sys->switchForceChoose - || !(rd->type == READ - && termSubTerm (rd->message, scanfrom->term))) + if (sys->switchForceChoose || not_read_first (rd, scanfrom->term)) { /* this term is forced as a choose, or it does not occur in the (first) read event */ - /* TODO scan might be more complex, but - * this will do for now. I.e. occurring - * first in a read will do */ - extterm = makeTermTuple (newvar, extterm); - artefacts = termlistAdd (artefacts, extterm); + if (extterm == NULL) + { + extterm = newvar; + } + else + { + extterm = makeTermTuple (newvar, extterm); + artefacts = termlistAdd (artefacts, extterm); + } } } else @@ -574,19 +599,6 @@ roleInstance (const System sys, const Protocol protocol, const Role role, /* set agent list */ runs[rid].agents = termlistDuplicate (tolist); - /* prefix a read for such reads. TODO: this should also cover any external stuff */ - if (extterm != NULL) - { - Roledef rdnew; - - rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL); - /* this is an internal action! */ - rdnew->internal = 1; - rdnew->next = rd; - rd = rdnew; - /* mark the first real action */ - runs[rid].firstReal++; - } } else { @@ -621,6 +633,26 @@ roleInstance (const System sys, const Protocol protocol, const Role role, if (inTermlist (protocol->rolenames, oldt)) { runs[rid].agents = termlistAdd (runs[rid].agents, newt); + + if (isTermVariable (newt)) + { + // It is a protocol role name, maybe add choose? + // Note that for anything but full type flaws, this is not an issue. + // In the POR reduction, force choose was the default. Here it is not. + if (not_read_first(rd, oldt) && sys->match == 2 ) + { + /* this term is forced as a choose, or it does not occur in the (first) read event */ + if (extterm == NULL) + { + extterm = newt; + } + else + { + extterm = makeTermTuple (newt, extterm); + artefacts = termlistAdd (artefacts, extterm); + } + } + } } fromlist = termlistAdd (fromlist, oldt); tolist = termlistAdd (tolist, newt); @@ -637,6 +669,20 @@ roleInstance (const System sys, const Protocol protocol, const Role role, } } + /* prefix a read for such reads. TODO: this should also cover any external stuff */ + if (extterm != NULL) + { + Roledef rdnew; + + rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL); + /* this is an internal action! */ + rdnew->internal = 1; + rdnew->next = rd; + rd = rdnew; + /* mark the first real action */ + runs[rid].firstReal++; + } + /* possibly shifted rd */ runs[rid].start = rd; runs[rid].index = rd;