From 508d49efbbb13435154ca7db1a379494a7666ebe Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 14 Jul 2004 06:55:05 +0000
Subject: [PATCH] - Added local step index to runs.

---
 src/modelchecker.c | 10 +++++++---
 src/runs.c         |  1 +
 src/runs.h         | 22 ++++++++--------------
 3 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/modelchecker.c b/src/modelchecker.c
index 0270b1a..2f7786f 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -119,9 +119,9 @@ executeStep (const System sys, const int run)
       printf ("#%i\n", run);
     }
 #endif
+  sys->runs[run].step++;
   runPointerSet (sys, run, runPoint->next);
 
-
   /* store knowledge for this step */
   (sys->step)++;
   sys->traceKnow[sys->step] = sys->know;
@@ -200,8 +200,11 @@ explorify (const System sys, const int run)
 {
   Roledef rd;
   int flag;
+  int myStep;
 
   rd = runPointerGet (sys, run);
+  myStep = sys->runs[run].step;
+
   if (rd == NULL)
     {
       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.
    */
-  if (rd == sys->runs[run].start && rd->type == READ)
+  if (myStep == 0 && rd->type == READ)
     {
       int rid;
 
@@ -286,7 +289,8 @@ explorify (const System sys, const int run)
     {
       /* traverse the system after the step */
       flag = traverse (sys);
-      runPointerSet (sys, run, rd);
+      runPointerSet (sys, run, rd);	// reset rd pointer
+      sys->runs[run].step = myStep;	// reset local index
       sys->step--;
       indentSet (sys->step);
       return flag;
diff --git a/src/runs.c b/src/runs.c
index e4a8aa3..f613a18 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -249,6 +249,7 @@ ensureValidRun (System sys, int run)
       struct run myrun = sys->runs[i];
       myrun.role = NULL;
       myrun.agents = NULL;
+      myrun.step = 0;
       myrun.index = NULL;
       myrun.start = NULL;
       myrun.know = knowledgeDuplicate (sys->know);
diff --git a/src/runs.h b/src/runs.h
index b02b339..356f4d0 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -125,20 +125,14 @@ typedef struct protocol *Protocol;
 //! Run container.
 struct run
 {
-  //! Protocol of this run.
-  Protocol protocol;
-  //! Role of this run.
-  Role role;
-  //! Agents involved in this run.
-  Termlist agents;
-  //! Current execution point in the run.
-  Roledef index;
-  //! Head of the run definition.
-  Roledef start;
-  //! Current knowledge of the run.
-  Knowledge know;
-  //! Locals of the run.
-  Termlist locals;
+  Protocol protocol;	//!< Protocol of this run.
+  Role role;		//!< Role of this run.
+  Termlist agents; 	//!< Agents involved in this run.
+  int step;		//!< Current execution point in the run (integer)
+  Roledef index;	//!< Current execution point in the run (roledef pointer)
+  Roledef start;	//!< Head of the run definition.
+  Knowledge know;	//!< Current knowledge of the run.
+  Termlist locals;	//!< Locals of the run.
 };
 
 //! Shorthand for run pointer.