--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Jan 25 18:09:21 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Jan 25 20:12:04 2021 +0900
@@ -37,14 +37,17 @@
 }
 
 __code startModelChecker(struct MCWorker* worker) {
-    struct Queue* mcQueue =  worker->mcQueue;
-    goto takeSingleLinkedQueue(mcQueue, taskReceiveMCWorker);
+    struct SingleLinkedQueue* mcQueue =  (struct SingleLinkedQueue*)worker->mcQueue->queue;
+    struct Element* elem = mcQueue->top;
+    elem = elem->next;
+    struct Context* ncontext = (struct Context*)elem->data;
+    goto meta(ncontext, ncontext->next);
 }
 
 __code getTaskMCWorker(struct MCWorker* mcWorker, struct Context* task, struct Worker* worker) {
     if (!task) {
         printf("mc worker take end\n");
-        goto worker->shutdown(); // end thread
+        goto startModelChecker(); // end thread
     }
     printf("mc worker take\n");
     task->worker = worker;