--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Jan 25 20:12:04 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Jan 25 20:44:24 2021 +0900
@@ -1,5 +1,8 @@
 #include "../../context.h"
 #include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
 #interface "TaskManager.h"
 #interface "Worker.h"
 #interface "Iterator.h"
@@ -7,6 +10,8 @@
 #interface "SingleLinkedQueue.h"
 
 static void startWorker(Worker* worker);
+extern int lengthSingleLinkedQueue(struct SingleLinkedQueue* queue);
+extern Element* getElementByIdx(struct SingleLinkedQueue* queue, int idx);
 
 Worker* createMCWorker(struct Context* context, int id, Queue* queue) {
     struct Worker* worker = new Worker();
@@ -18,6 +23,7 @@
     mcWorker->loopCounter = 0;
     worker->taskReceive = C_taskReceiveMCWorker;
     worker->shutdown = C_shutdownMCWorker;
+    srandom(time(NULL));
     pthread_create(&worker->thread, NULL, (void*)&startWorker, worker);
     return worker;
 }
@@ -36,10 +42,14 @@
     goto tasks->take(getTaskMCWorker);
 }
 
+
 __code startModelChecker(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;
     goto meta(ncontext, ncontext->next);
 }

--- a/src/parallel_execution/SingleLinkedQueue.cbc	Mon Jan 25 20:12:04 2021 +0900
+++ b/src/parallel_execution/SingleLinkedQueue.cbc	Mon Jan 25 20:44:24 2021 +0900
@@ -33,7 +33,8 @@
 }
 
 __code clearSingleLinkedQueue(struct SingleLinkedQueue* queue, __code next(...)) {
-    queue->top = NULL;
+    queue->top->next = NULL;
+    queue->last = queue->top;
     goto next(...);
 }
 
@@ -66,3 +67,28 @@
     }
 }
 
+
+int lengthSingleLinkedQueue(struct SingleLinkedQueue* queue) {
+    int length = 0;
+    struct Element* current = queue->top;
+
+    while (current->next != NULL) {
+      length++;
+      current = current->next;
+    }
+
+    return length - 1; // top is dummy
+}
+
+
+Element* getElementByIdx(struct SingleLinkedQueue* queue, int idx) {
+    struct Element* current = queue->top;
+
+    while (current->next != NULL){
+      if (idx-- == 0 ) {
+        return current->next;
+      }
+      current = current->next;
+    }
+    return queue->top;
+}