--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 00:04:05 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 10:06:35 2021 +0900
@@ -57,11 +57,9 @@
     struct SingleLinkedQueue* mcQueue =  (struct SingleLinkedQueue*)worker->mcQueue->queue;
     struct Element* elem = mcQueue->top;
     elem = elem->next;
-    int length = lengthSingleLinkedQueue(mcQueue);
-    int idx = random()%(length+1); // incase of multithread use random_r
-    elem = getElementByIdx(mcQueue, idx);
     struct Context* ncontext = (struct Context*)elem->data;
     worker->mcContext = ncontext;
+    int length = lengthSingleLinkedQueue(mcQueue);
     for (int i = 0; i <= length; i++) {
         struct Element* tmpElem = getElementByIdx(mcQueue, i);
         struct Context* tmpContext = (struct Context*)tmpElem->data;
@@ -71,6 +69,18 @@
     goto meta(ncontext, ncontext->next);
 }
 
+__code startRandom(struct MCWorker* worker) {
+    struct SingleLinkedQueue* mcQueue =  (struct SingleLinkedQueue*)worker->mcQueue->queue;
+    struct Element* elem = mcQueue->top;
+    elem = elem->next;
+    int length = lengthSingleLinkedQueue(mcQueue);
+    int idx = random()%(length+1); // incase of multithread use random_r
+    elem = getElementByIdx(mcQueue, idx);
+    struct Context* ncontext = (struct Context*)elem->data;
+    worker->mcContext = ncontext;
+    goto meta(ncontext, ncontext->next);
+}
+
 extern TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev);
 extern Element* takeNextIterator(TaskIterator* iterator);
 extern void freeIterator(TaskIterator* iterator);
@@ -118,7 +128,7 @@
     // printf("depth %d count %d\n", depth, count++);
     mcworker->count++;
     //goto list->phils->next(list->phils,list);
-    goto meta(context, next);
+    goto meta(context, context->next);
 }
 
 __code getTaskMCWorker(struct MCWorker* mcWorker, struct Context* task, struct Worker* worker) {