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

Nearly at 20 trampolines left.

Browse Source
This commit is contained in:
Cas Cremers 2018-10-19 16:01:44 -04:00
parent 9da05f738c
commit 38d57ed91d
1 changed files with 27 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
src/system.c
View File

@ -1189,41 +1189,43 @@ iterateRoles (const System sys, int (*callback) (Protocol p, Role r))
} }
//! Get first recv/send occurrence (event index) of term t in run r //! Get first recv/send occurrence (event index) of term t in run r
/**
* ..or -1 if it does not occor
*/
int int
firstOccurrence (const System sys, const int r, Term t, int evtype) firstOccurrence (const System sys, const int r, Term t, int evtype)
{ {
int firste; int e;
Roledef rd;
int checkOccurs (Roledef rd, int e) rd = sys->runs[r].start;
{ for (e = 0; e < sys->runs[r].step; e++)
if (termSubTerm (rd->message, t) || termSubTerm (rd->from, t) {
|| termSubTerm (rd->to, t)) if (evtype == ANYEVENT || rd->type == evtype)
{ {
firste = e; if (termSubTerm (rd->message, t) || termSubTerm (rd->from, t)
return false; || termSubTerm (rd->to, t))
} {
return true; return e;
} }
}
rd = rd->next;
}
firste = -1;
iterateEventsType (sys, r, evtype, checkOccurs);
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (3)) if (DEBUGL (3))
{ {
if (firste == -1) globalError++;
{ eprintf ("Warning: Desired term ");
globalError++; termPrint (t);
eprintf ("Warning: Desired term "); eprintf (" does not occur");
termPrint (t); eprintf (" in run %i in event type %i.\n", r, evtype);
eprintf (" does not occur"); runPrint (sys->runs[r].start);
eprintf (" in run %i in event type %i.\n", r, evtype); eprintf ("\n");
runPrint (sys->runs[r].start); globalError--;
eprintf ("\n");
globalError--;
}
} }
#endif #endif
return firste; return -1;
} }
//! Get the roledef of an event //! Get the roledef of an event