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

- Cleaned up -t10, removed the inclination towards chooses.

Browse Source
This commit is contained in:
ccremers 2004-07-17 20:18:55 +00:00
parent ff178f46a5
commit 6a3edd06c2
1 changed files with 3 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/modelchecker.c
View File

@ -1255,40 +1255,11 @@ traversePOR6 (const System sys)
/* The 'choose' implemented here is the following: /* The 'choose' implemented here is the following:
* *
* choose ev#rid * choose ev#rid
* where rid = min(r: ev#r in enabled(sys): (r-lastrun) mod maxruns) * where rid = min(r: ev#r in enabled(sys): r)
* and where lastrun is the runid of the previous event
* in the trace, or 0 if there was none.
*/ */
/* First pick out any choose events */ /* Try all events (implicitly we only handle enabled ones) left-to-right.
for (run = 0; run < sys->maxruns && !flag; run++) * If one was chosen, flag is set, and the loop aborts. */
{
rd = runPointerGet (sys, run);
if (rd != NULL)
{
switch (rd->type)
{
case CLAIM:
case SEND:
break;
case READ:
if (rd->internal)
{
flag = executeTry (sys, run);
}
break;
default:
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
exit (1);
}
}
}
/* Try all events (implicitly we only handle enabled ones) starting with our
* first choice. If one was chosen, flag is set, and the loop aborts. */
for (run = 0; run < sys->maxruns && !flag; run++) for (run = 0; run < sys->maxruns && !flag; run++)
{ {
rd = runPointerGet (sys, run); rd = runPointerGet (sys, run);