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

BUGFIX: C-minimality was tripping over claims.

Browse Source
This commit is contained in:
Cas Cremers 2008-11-09 15:11:43 +01:00
parent f21c02e772
commit d633a62f0d
1 changed files with 46 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
src/binding.c
View File

@ -543,56 +543,64 @@ bindings_c_minimal ()
for (run = 0; run < sys->maxruns; run++) for (run = 0; run < sys->maxruns; run++)
{ {
int ev; int ev;
Roledef rd;
rd = sys->runs[run].start;
//!@todo hardcoded reference to step, should be length //!@todo hardcoded reference to step, should be length
for (ev = 0; ev < sys->runs[run].step; ev++) for (ev = 0; ev < sys->runs[run].step; ev++)
{ {
if (isDependEvent (run, ev, b->run_from, b->ev_from)) if (rd->type == SEND || rd->type == READ)
{ {
// this node is *before* the from node if (isDependEvent (run, ev, b->run_from, b->ev_from))
Roledef rd;
int occursthere;
rd = roledef_shift (sys->runs[run].start, ev);
if (switches.intruder)
{ {
// intruder: interm bindings should cater for the first occurrence // this node is *before* the from node
occursthere = termInTerm (rd->message, b->term);
int occursthere;
if (switches.intruder)
{
// intruder: interm bindings should cater for the first occurrence
occursthere =
termInTerm (rd->message, b->term);
}
else
{
// no intruder, then simple test
occursthere =
isTermEqual (rd->message, b->term);
}
if (occursthere)
{
// This term already occurs in a previous node!
#ifdef DEBUG
if (DEBUGL (4))
{
// Report this
indentPrint ();
eprintf ("Binding for ");
termPrint (b->term);
eprintf
(" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ",
b->run_from, b->ev_from, run, ev);
termPrint (rd->message);
eprintf ("\n");
}
#endif
return false;
}
} }
else else
{ {
// no intruder, then simple test // If this event is not before the target, then the
occursthere = isTermEqual (rd->message, b->term); // next in the run certainly is not either (because
// that would imply that this one is before it)
// Thus, we effectively exit the loop.
break;
} }
if (occursthere)
{
// This term already occurs in a previous node!
#ifdef DEBUG
if (DEBUGL (4))
{
// Report this
indentPrint ();
eprintf ("Binding for ");
termPrint (b->term);
eprintf
(" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ",
b->run_from, b->ev_from, run, ev);
termPrint (rd->message);
eprintf ("\n");
}
#endif
return false;
}
}
else
{
// If this event is not before the target, then the
// next in the run certainly is not either (because
// that would imply that this one is before it)
// Thus, we effectively exit the loop.
break;
} }
} }
rd = rd->next;
} }
} }
bl = bl->next; bl = bl->next;