--- a/src/parallel_execution/MCWorker.h	Wed Jan 27 17:06:14 2021 +0900
+++ b/src/parallel_execution/MCWorker.h	Wed Jan 27 19:01:14 2021 +0900
@@ -1,15 +1,19 @@
 #include "ModelChecking/state_db.h"
 #include "ModelChecking/memory.h"
+#include "ModelChecking/TaskIterator.h"
 
 typedef struct MCWorker <> {
   pthread_mutex_t mutex;
   pthread_cond_t cond;
-  struct Context* context;
+  struct Context* context; //simulated task
+  struct Context* mcContext; // context for mcWorker
+  struct Context* masterContext; // context for McTaskManager (singleton)
   int id;
   int loopCounter;
-  struct Queue* mcQueue;
+  struct Queue* mcQueue; // simulated task queue par thread
   enum Code nextStep;
-  struct Context* mcContext;
-  StateDB state;
   StateNode st;
+  TaskIterator* task_iter;
+  int depth;
+  int count;
 } MCWorker;

--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Wed Jan 27 17:06:14 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Wed Jan 27 19:01:14 2021 +0900
@@ -22,8 +22,10 @@
     worker->worker = (union Data*)mcWorker;
     worker->tasks = queue;
     mcWorker->id = id;
+    mcWorker->depth = 0;
+    mcWorker->count = 0;
     mcWorker->mcContext = NULL;
-    mcWorker->state = NULL;
+    mcWorker->masterContext = context; //singleton
     mcWorker->loopCounter = 0;
     mcWorker->nextStep = C_startModelChecker;
     worker->taskReceive = C_taskReceiveMCWorker;
@@ -65,14 +67,49 @@
     goto meta(ncontext, ncontext->next);
 }
 
+extern TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev);
+extern Element* takeNextIterator(TaskIterator* iterator);
+extern void freeIterator(TaskIterator* iterator);
+
 
 __ncode mcMeta(struct Context* context, enum Code next) {
-    StateDB out;
+    context->next = next; // remember next Code Gear
     struct MCWorker* mcworker =  (struct MCWorker*) context->worker->worker;
-    if (lookup_StateDB(&mcworker->st, &mcworker->state, &out)) {
+    StateDB out = NULL;
+    struct Context* list = NULL;
+
+    mcworker->st.hash = get_memory_hash(context->mem,0);
+    if (lookup_StateDB(&mcworker->st, &mcworker->masterContext->state_db, &out)) {
+    // found in the state database
+    //printf("found %d\n",count);
+      while(!(list = (struct Context*)takeNextIterator(task_iter))) {
+          // no more branch, go back to the previous one
+          TaskIterator* prev_iter = task_iter->prev;
+          if (!prev_iter) {
+            printf("All done count %d\n",mcworker->count);
+            memory_usage();
+            exit(0);
+          }
+          //printf("no more branch %d\n",count);
+          mcworker->depth--;
+          freeIterator(task_iter);
+          mcworker->task_iter = prev_iter;
+      }
+      // return to previous state
+      //    here we assume task list is fixed, we don't have to
+      //    recover task list itself
+      restore_memory(task_iter->state->memory);
+      //printf("restore list %x next %x\n",(int)list,(int)(list->next));
+    } else {
+      // one step further
+      mcworker->depth++;
+      struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcworker->mcQueue->queue;
+      mcworker->task_iter = createQueueIterator(mcSingleQueue->top->next,out,task_iter);
     }
-    context->next = next;
-    goto meta(mcworker->context, mcworker->nextStep);
+    //printf("depth %d count %d\n", depth, count++);
+    mcworker->count++;
+    //goto list->phils->next(list->phils,list);
+    goto meta(context, next);
 }
 
 __code getTaskMCWorker(struct MCWorker* mcWorker, struct Context* task, struct Worker* worker) {

--- a/src/parallel_execution/SingleLinkedQueue.cbc	Wed Jan 27 17:06:14 2021 +0900
+++ b/src/parallel_execution/SingleLinkedQueue.cbc	Wed Jan 27 19:01:14 2021 +0900
@@ -95,25 +95,17 @@
 }
 
 
-typedef struct task_iterator {
-    Element* prev;
-    StateDB state;
-    Element* list;
-    Element* last;
-} TaskIterator, *TaskIteratorPtr;
 
-
-TaskIteratorPtr createQueueIterator(struct SingleLinkedQueue* queue, StateDB s, struct Element* prev) {
-    TaskIteratorPtr new = (TaskIteratorPtr)calloc(1, sizeof(TaskIterator));
+TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev) {
+    TaskIterator* new = (TaskIterator*)calloc(1, sizeof(TaskIterator));
     if (!new) exit(1);
     new->prev  = prev;
     new->state = s; //
-    new->list  = queue->top;
-    new->last  = queue->last;
+    new->list  = elements;
     return new;
 }
 
-Element* takeNextIterator(struct SingleLinkedQueue* queue, TaskIteratorPtr iterator) {
+Element* takeNextIterator(TaskIterator* iterator) {
   struct Element* elem = iterator->list;
   if (!elem) {
     return NULL;
@@ -124,10 +116,11 @@
     return NULL;
   }
 
-  if (next == iterator->last) {
-    return NULL;
-  }
 
   iterator->list = next;
   return next;
 }
+
+void freeIterator(TaskIterator* iterator) {
+  free(iterator);
+}

--- a/src/parallel_execution/lib/Gears/Template/Context.pm	Wed Jan 27 17:06:14 2021 +0900
+++ b/src/parallel_execution/lib/Gears/Template/Context.pm	Wed Jan 27 19:01:14 2021 +0900
@@ -109,6 +109,7 @@
 
 #include "c/enumCode.h"
 #include "ModelChecking/memory.h"
+#include "ModelChecking/state_db.h"
 
 enum Relational {
     EQ,
@@ -156,6 +157,7 @@
     int iterate;
     struct Iterator* iterator;
     MemoryPtr mem;
+    StateDB state_db;
 };
 
 typedef int Int;