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

- Added local step index to runs.

Browse Source
This commit is contained in:
ccremers 2004-07-14 06:55:05 +00:00
parent 5bb5f610fb
commit 508d49efbb
3 changed files with 16 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/modelchecker.c
View File

@ -119,9 +119,9 @@ executeStep (const System sys, const int run)
printf ("#%i\n", run); printf ("#%i\n", run);
} }
#endif #endif
sys->runs[run].step++;
runPointerSet (sys, run, runPoint->next); runPointerSet (sys, run, runPoint->next);
/* store knowledge for this step */ /* store knowledge for this step */
(sys->step)++; (sys->step)++;
sys->traceKnow[sys->step] = sys->know; sys->traceKnow[sys->step] = sys->know;
@ -200,8 +200,11 @@ explorify (const System sys, const int run)
{ {
Roledef rd; Roledef rd;
int flag; int flag;
int myStep;
rd = runPointerGet (sys, run); rd = runPointerGet (sys, run);
myStep = sys->runs[run].step;
if (rd == NULL) if (rd == NULL)
{ {
fprintf (stderr, "ERROR: trying to progress completed run!\n"); fprintf (stderr, "ERROR: trying to progress completed run!\n");
@ -213,7 +216,7 @@ explorify (const System sys, const int run)
/* /*
* Special checks after (implicit) choose events; always first in run reads. * Special checks after (implicit) choose events; always first in run reads.
*/ */
if (rd == sys->runs[run].start && rd->type == READ) if (myStep == 0 && rd->type == READ)
{ {
int rid; int rid;
@ -286,7 +289,8 @@ explorify (const System sys, const int run)
{ {
/* traverse the system after the step */ /* traverse the system after the step */
flag = traverse (sys); flag = traverse (sys);
runPointerSet (sys, run, rd); runPointerSet (sys, run, rd); // reset rd pointer
sys->runs[run].step = myStep; // reset local index
sys->step--; sys->step--;
indentSet (sys->step); indentSet (sys->step);
return flag; return flag;

1
src/runs.c
View File

@ -249,6 +249,7 @@ ensureValidRun (System sys, int run)
struct run myrun = sys->runs[i]; struct run myrun = sys->runs[i];
myrun.role = NULL; myrun.role = NULL;
myrun.agents = NULL; myrun.agents = NULL;
myrun.step = 0;
myrun.index = NULL; myrun.index = NULL;
myrun.start = NULL; myrun.start = NULL;
myrun.know = knowledgeDuplicate (sys->know); myrun.know = knowledgeDuplicate (sys->know);

22
src/runs.h
View File

@ -125,20 +125,14 @@ typedef struct protocol *Protocol;
//! Run container. //! Run container.
struct run struct run
{ {
//! Protocol of this run. Protocol protocol; //!< Protocol of this run.
Protocol protocol; Role role; //!< Role of this run.
//! Role of this run. Termlist agents; //!< Agents involved in this run.
Role role; int step; //!< Current execution point in the run (integer)
//! Agents involved in this run. Roledef index; //!< Current execution point in the run (roledef pointer)
Termlist agents; Roledef start; //!< Head of the run definition.
//! Current execution point in the run. Knowledge know; //!< Current knowledge of the run.
Roledef index; Termlist locals; //!< Locals of the run.
//! Head of the run definition.
Roledef start;
//! Current knowledge of the run.
Knowledge know;
//! Locals of the run.
Termlist locals;
}; };
//! Shorthand for run pointer. //! Shorthand for run pointer.