view src/mcMeta.cbc @ 6:958c69a33b37 default tip

fix presen
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 May 2021 14:04:14 +0900
parents 67e6ca3c7e6c
children
line wrap: on
line source

    __ncode mcMeta(struct Context* context, enum Code next) {
        // 次の実行を context に覚えておく
        context->next = next; // remember next Code Gear
        // Worker (複数)と TaskManager(singleton)を context から取ってくる
        struct MCWorker* mcWorker =  (struct MCWorker*) context->worker->worker;
        StateNode st ;
        StateDB out = &st;
        struct Element* list = NULL;
        struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcWorker->taskManager->taskManager;
        out->memory = mcti->mem;
        out->hash = get_memory_hash(mcti->mem,0);
        if (dump) {
            dump_memory(mcti->mem);printf("\n");
        }
        // state を db から探す
        int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit);
        
        // モデル検査フラグの更新
        mcti->statefunc(mcti, mcWorker, mcWorker->parent, out, mcWorker->checking);
        if (found) {
          // 既に状態 db にあった場合
          // iterator を探す、終わっていたら上に戻る
          while(!(list = takeNextIterator(mcWorker->task_iter))) {
              // no more branch, go back to the previous one
              TaskIterator* prev_iter = mcWorker->task_iter->prev;
              if (!prev_iter) {
                //  もう上がないので全部探した
                printf("All done count %d repeat %d\n",mcWorker->count,mcWorker->visit);
                memory_usage();
                // flag の更新を見る
                if (! mcWorker->change && mcWorker->checking) {
                  exit(0);
                } else if (! mcWorker->change ) {
                    // flag の更新は終わったので、フラグを調べる
                    mcWorker->checking = 1;
                } 
 
                // 最初から始める
                mcWorker->change = 0;
                mcWorker->visit++;
                // start from root state and iterator
                mcWorker->depth = 0;
                struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
                mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,mcWorker->root,NULL);
              } else {
                // 一つ上に戻る
                mcWorker->depth--;
                freeIterator(mcWorker->task_iter);
                mcWorker->task_iter = prev_iter;
              }
          }
          // 戻った時にメモリを書き戻す
          restore_memory(mcWorker->task_iter->state->memory);
          context = (Context *)list->data;
          // printf("restore list %x next %x\n",(int)list,(int)(list->next));
        } else {
          // 一段、深く実行するので、新しく iterator を作る
          mcWorker->depth++;
          struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
          mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,out,mcWorker->task_iter);
        }
        // normal level に戻る
        mcWorker->parent = out;
        mcWorker->count++;
        mcWorker->mcContext = context;
        //goto list->phils->next(list->phils,list);
        goto meta(context, context->next);
    }