andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Huge effort to make match type 2 (typeflaw generic) matching work.

Browse Source 
Problem with goals that turn into tuples, will have to be solved.
This commit is contained in:
ccremers 2004-08-31 14:31:06 +00:00
parent 0e9b7dcf11
commit 8b48aade68
3 changed files with 116 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
src/arachne.c
View File

@ -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)

18
src/binding.c
View File

@ -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?",
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++;

84
src/system.c
View File

@ -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,18 +573,20 @@ 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 */
if (extterm == NULL)
{
extterm = newvar;
}
else
{
extterm = makeTermTuple (newvar, extterm);
artefacts = termlistAdd (artefacts, extterm);
}
}
}
else
{
/* not a type constant, add to list */
@ -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;